Collapse file tree

Files

 master

Search this repository

/

pretyping

/

Copy path

Directory actions

More options

More options

Directory actions

More options

More options

Latest commit

herbelin

Fixes rocq-prover#7811 (uncaught Not_found in notation printer relate…

Open commit details

Jun 17, 2018

abd89e3 · Jun 17, 2018

History

History

Open commit details

This branch is 21358 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	[api] Rename global_reference to GlobRef.t to follow kernel style.	May 4, 2018
arguments_renaming.mli		arguments_renaming.mli	[api] Rename global_reference to GlobRef.t to follow kernel style.	May 4, 2018
cases.ml		cases.ml	Fix deprecation warning introduced by PR 664 merge	Jun 14, 2018
cases.mli		cases.mli	Update headers following rocq-prover#6543.	Feb 27, 2018
cbv.ml		cbv.ml	[api] Deprecate a couple of aliases that we missed.	Mar 28, 2018
cbv.mli		cbv.mli	[api] Deprecate a couple of aliases that we missed.	Mar 28, 2018
classops.ml		classops.ml	Split off Universes functions dealing with generating new universes.	May 17, 2018
classops.mli		classops.mli	[api] Rename global_reference to GlobRef.t to follow kernel style.	May 4, 2018
coercion.ml		coercion.ml	[api] Remove deprecated object from Term	May 30, 2018
coercion.mli		coercion.mli	Update headers following rocq-prover#6543.	Feb 27, 2018
constr_matching.ml		constr_matching.ml	Merge PR rocq-prover#7199: Fixes rocq-prover#7195: missing freshness …	Jun 4, 2018
constr_matching.mli		constr_matching.mli	Do not compute constr matching context if not used.	Apr 10, 2018
detyping.ml		detyping.ml	[api] Misctypes removal: several moves:	Jun 12, 2018
detyping.mli		detyping.mli	[api] Move universe syntax to Glob_term	May 7, 2018
doc.tex		doc.tex	ocamlweb	Nov 30, 1999
evarconv.ml		evarconv.ml	Stronger invariants in unification signature.	Jun 4, 2018
evarconv.mli		evarconv.mli	set_solve_evars doesn't use an evar_map ref	May 11, 2018
evardefine.ml		evardefine.ml	Evar maps contain econstrs.	Apr 13, 2018
evardefine.mli		evardefine.mli	Update headers following rocq-prover#6543.	Feb 27, 2018
evarsolve.ml		evarsolve.ml	Fixes rocq-prover#7780 (missing lift in expanding alias under a binde…	Jun 12, 2018
evarsolve.mli		evarsolve.mli	[api] Deprecate a couple of aliases that we missed.	Mar 28, 2018
find_subterm.ml		find_subterm.ml	Update headers following rocq-prover#6543.	Feb 27, 2018
find_subterm.mli		find_subterm.mli	Update headers following rocq-prover#6543.	Feb 27, 2018
geninterp.ml		geninterp.ml	Update headers following rocq-prover#6543.	Feb 27, 2018
geninterp.mli		geninterp.mli	Update headers following rocq-prover#6543.	Feb 27, 2018
glob_ops.ml		glob_ops.ml	Fixes rocq-prover#7811 (uncaught Not_found in notation printer relate…	Jun 17, 2018
glob_ops.mli		glob_ops.mli	[api] Misctypes removal: several moves:	Jun 12, 2018
glob_term.ml		glob_term.ml	[api] Misctypes removal: several moves:	Jun 12, 2018
indrec.ml		indrec.ml	Remove some occurrences of Evd.empty	May 25, 2018
indrec.mli		indrec.mli	[api] Rename global_reference to GlobRef.t to follow kernel style.	May 4, 2018
inductiveops.ml		inductiveops.ml	Reduce circular dependency constants <-> projections	May 31, 2018
inductiveops.mli		inductiveops.mli	[api] Deprecate a couple of aliases that we missed.	Mar 28, 2018
inferCumulativity.ml		inferCumulativity.ml	Merge PR rocq-prover#6769: Split closure cache and remove whd_both	Mar 9, 2018
inferCumulativity.mli		inferCumulativity.mli	Update headers following rocq-prover#6543.	Feb 27, 2018
locus.ml		locus.ml	[api] Remove Misctypes.	Jun 12, 2018
locusops.ml		locusops.ml	[api] Remove Misctypes.	Jun 12, 2018
locusops.mli		locusops.mli	Update headers following rocq-prover#6543.	Feb 27, 2018
ltac_pretype.ml		ltac_pretype.ml	[general] Remove Econstr dependency from intf	Oct 25, 2017
nativenorm.ml		nativenorm.ml	Merge PR rocq-prover#7679: Clean native compilation of primitive proj…	Jun 5, 2018
nativenorm.mli		nativenorm.mli	Stronger invariants in unification signature.	Jun 4, 2018
pattern.ml		pattern.ml	[api] Misctypes removal: remove dummy alias.	Jun 12, 2018
patternops.ml		patternops.ml	[api] Misctypes removal: several moves:	Jun 12, 2018
patternops.mli		patternops.mli	[api] Misctypes removal: miscellaneous aliases.	Jun 12, 2018
pretype_errors.ml		pretype_errors.ml	Remove some occurrences of Evd.empty	May 25, 2018
pretype_errors.mli		pretype_errors.mli	Update headers following rocq-prover#6543.	Feb 27, 2018
pretyping.ml		pretyping.ml	[api] Misctypes removal: several moves:	Jun 12, 2018
pretyping.mli		pretyping.mli	[api] Move universe syntax to Glob_term	May 7, 2018
pretyping.mllib		pretyping.mllib	[api] Move Constrexpr to the interp module.	May 31, 2018
program.ml		program.ml	Deprecate most evarutil evdref functions	May 11, 2018
program.mli		program.mli	[api] Rename global_reference to GlobRef.t to follow kernel style.	May 4, 2018
recordops.ml		recordops.ml	Remove some occurrences of Evd.empty	May 25, 2018
recordops.mli		recordops.mli	[api] Rename global_reference to GlobRef.t to follow kernel style.	May 4, 2018
reductionops.ml		reductionops.ml	Stronger invariants in unification signature.	Jun 4, 2018
reductionops.mli		reductionops.mli	Stronger invariants in unification signature.	Jun 4, 2018
retyping.ml		retyping.ml	Evar maps contain econstrs.	Apr 13, 2018
retyping.mli		retyping.mli	[api] Deprecate a couple of aliases that we missed.	Mar 28, 2018
tacred.ml		tacred.ml	[api] Remove deprecated object from Term	May 30, 2018
tacred.mli		tacred.mli	[api] Rename global_reference to GlobRef.t to follow kernel style.	May 4, 2018
typeclasses.ml		typeclasses.ml	[api] Misctypes removal: miscellaneous aliases.	Jun 12, 2018
typeclasses.mli		typeclasses.mli	[api] Misctypes removal: miscellaneous aliases.	Jun 12, 2018
typeclasses_errors.ml		typeclasses_errors.ml	[api] Misctypes removal: miscellaneous aliases.	Jun 12, 2018
typeclasses_errors.mli		typeclasses_errors.mli	[api] Misctypes removal: miscellaneous aliases.	Jun 12, 2018
typing.ml		typing.ml	Merge PR rocq-prover#664: Fixing rocq-prover#5500 (missing test in re…	Jun 14, 2018
typing.mli		typing.mli	Deprecate Typing.e_* functions	May 14, 2018
unification.ml		unification.ml	Merge PR rocq-prover#7004: Make simple apply obey Opaque directive.	Jun 5, 2018
unification.mli		unification.mli	Make direct invocations of simple apply obey Opaque directive.	Jun 5, 2018
vnorm.ml		vnorm.ml	Preserving "canonical" form of return predicate in vm_compute.	Jun 4, 2018
vnorm.mli		vnorm.mli	Update headers following rocq-prover#6543.	Feb 27, 2018
View all files