Collapse file tree

Files

 trunk

Search this repository

/

pretyping

/

Copy path

Directory actions

More options

More options

Directory actions

More options

More options

Latest commit

ppedrot

Merge branch 'v8.5'

Apr 15, 2015

148cf78 · Apr 15, 2015

History

History

Open commit details

This branch is 28692 commits behind rocq-prover/rocq:master.

/

pretyping

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
arguments_renaming.ml		arguments_renaming.ml	Update headers.	Jan 12, 2015
arguments_renaming.mli		arguments_renaming.mli	Update headers.	Jan 12, 2015
cases.ml		cases.ml	Fixing first part of bug rocq-prover#3210 (inference of pattern-match…	Feb 27, 2015
cases.mli		cases.mli	Update headers.	Jan 12, 2015
cbv.ml		cbv.ml	Update headers.	Jan 12, 2015
cbv.mli		cbv.mli	Update headers.	Jan 12, 2015
classops.ml		classops.ml	Use kernel names instead of user names when looking for coercions. (F…	Mar 25, 2015
classops.mli		classops.mli	Update headers.	Jan 12, 2015
coercion.ml		coercion.ml	Update headers.	Jan 12, 2015
coercion.mli		coercion.mli	Update headers.	Jan 12, 2015
constr_matching.ml		constr_matching.ml	Ensuring more invariants in Constr_matching.	Mar 29, 2015
constr_matching.mli		constr_matching.mli	Update headers.	Jan 12, 2015
detyping.ml		detyping.ml	Continuing experimentation on what part of the instance of an evar	Feb 21, 2015
detyping.mli		detyping.mli	Univs: proper printing of global and local universe names (only	Jan 17, 2015
doc.tex		doc.tex	ocamlweb	Nov 30, 1999
evarconv.ml		evarconv.ml	Fix bug rocq-prover#3532, providing universe inconsistency informatio…	Mar 3, 2015
evarconv.mli		evarconv.mli	Update headers.	Jan 12, 2015
evarsolve.ml		evarsolve.ml	Fix bug rocq-prover#4101, noccur_evar's expand_projection can legitim…	Mar 3, 2015
evarsolve.mli		evarsolve.mli	Update headers.	Jan 12, 2015
evarutil.ml		evarutil.ml	STM: proof state also includes meta counters	Feb 25, 2015
evarutil.mli		evarutil.mli	STM: proof state also includes meta counters	Feb 25, 2015
find_subterm.ml		find_subterm.ml	Removing dead code.	Feb 2, 2015
find_subterm.mli		find_subterm.mli	Removing dead code.	Feb 2, 2015
glob_ops.ml		glob_ops.ml	Update headers.	Jan 12, 2015
glob_ops.mli		glob_ops.mli	Fixing equality of notation_constrs. Fixes bug rocq-prover#4136.	Mar 24, 2015
indrec.ml		indrec.ml	Update headers.	Jan 12, 2015
indrec.mli		indrec.mli	Update headers.	Jan 12, 2015
inductiveops.ml		inductiveops.ml	Fully fixing bug rocq-prover#3491 (anomaly when building _rect scheme…	Mar 25, 2015
inductiveops.mli		inductiveops.mli	Fully fixing bug rocq-prover#3491 (anomaly when building _rect scheme…	Mar 25, 2015
locusops.ml		locusops.ml	Update headers.	Jan 12, 2015
locusops.mli		locusops.mli	Update headers.	Jan 12, 2015
miscops.ml		miscops.ml	Update headers.	Jan 12, 2015
miscops.mli		miscops.mli	Update headers.	Jan 12, 2015
nativenorm.ml		nativenorm.ml	Make native compiler handle universe polymorphic definitions.	Jan 17, 2015
nativenorm.mli		nativenorm.mli	Update headers.	Jan 12, 2015
patternops.ml		patternops.ml	Really fix constr_of_pattern and bugs rocq-prover#3590 and rocq-prove…	Apr 9, 2015
patternops.mli		patternops.mli	Fix bug rocq-prover#3590, keeping evars that are not turned into name…	Mar 3, 2015
pretype_errors.ml		pretype_errors.ml	Update headers.	Jan 12, 2015
pretype_errors.mli		pretype_errors.mli	Update headers.	Jan 12, 2015
pretyping.ml		pretyping.ml	Fix some typos in comments.	Feb 23, 2015
pretyping.mli		pretyping.mli	Fix some typos in comments.	Feb 23, 2015
pretyping.mllib		pretyping.mllib	Adding a new folder corresponding to the low-level part of the pretyper	Feb 26, 2015
program.ml		program.ml	Update headers.	Jan 12, 2015
program.mli		program.mli	Update headers.	Jan 12, 2015
recordops.ml		recordops.ml	Update headers.	Jan 12, 2015
recordops.mli		recordops.mli	Update headers.	Jan 12, 2015
redops.ml		redops.ml	Update headers.	Jan 12, 2015
redops.mli		redops.mli	Update headers.	Jan 12, 2015
reductionops.ml		reductionops.ml	Fix bug rocq-prover#3532, providing universe inconsistency informatio…	Mar 3, 2015
reductionops.mli		reductionops.mli	Fix bug rocq-prover#3532, providing universe inconsistency informatio…	Mar 3, 2015
retyping.ml		retyping.ml	Taking current env and not global env in b286c9f (4 commits ago,	Feb 27, 2015
retyping.mli		retyping.mli	Update headers.	Jan 12, 2015
tacred.ml		tacred.ml	Fix 'don't expose cases' in cbn	Feb 15, 2015
tacred.mli		tacred.mli	Update headers.	Jan 12, 2015
typeclasses.ml		typeclasses.ml	Fix bug rocq-prover#3960: potential evar instance categorized as an u…	Feb 16, 2015
typeclasses.mli		typeclasses.mli	Fix bug rocq-prover#3960: potential evar instance categorized as an u…	Feb 16, 2015
typeclasses_errors.ml		typeclasses_errors.ml	Removing dead code.	Feb 2, 2015
typeclasses_errors.mli		typeclasses_errors.mli	Removing dead code.	Feb 2, 2015
typing.ml		typing.ml	Update headers.	Jan 12, 2015
typing.mli		typing.mli	Removing dead code.	Feb 2, 2015
unification.ml		unification.ml	Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.	Feb 23, 2015
unification.mli		unification.mli	Update headers.	Jan 12, 2015
vnorm.ml		vnorm.ml	use a more compact representation of non-constant constructors	Mar 27, 2015
vnorm.mli		vnorm.mli	Update headers.	Jan 12, 2015
View all files