coq - The formal proof system

Age	Commit message (Expand)	Author
2017-11-07	[api] Remove 8.7 ML-deprecated functions.	Emilio Jesus Gallego Arias
2017-11-06	Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ...	Maxime Dénès
2017-11-02	Setting a system to register printers for Ltac values.	Hugo Herbelin
2017-11-02	Using a specific function to register vernac printers.	Hugo Herbelin
2017-11-01	provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules	Matej Košík
2017-10-27	Merge PR #6015: [general] Remove Econstr dependency from `intf`	Maxime Dénès
2017-10-26	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin
2017-10-25	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias
2017-10-17	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias
2017-10-17	[stm] Move interpretation state to Vernacentries	Emilio Jesus Gallego Arias
2017-10-17	[stm] Remove VtBack from public classification.	Emilio Jesus Gallego Arias
2017-10-17	[stm] First step to move interpretation of Undo commands out of the classifier.	Emilio Jesus Gallego Arias
2017-10-10	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias
2017-10-10	Merge PR #768: Omega and romega know about context definitions (fix old bug 148)	Maxime Dénès
2017-10-09	Merge PR #1087: [stm] Switch to a functional API	Maxime Dénès
2017-10-06	[stm] Switch to a functional API	Emilio Jesus Gallego Arias
2017-10-05	romega: takes advantage of context variables with body	Pierre Letouzey
2017-10-03	Ltac uses the new generic locatable API.	Pierre-Marie Pédrot
2017-10-03	Moving the Ltac-specific part of the nametab to the Ltac plugin.	Pierre-Marie Pédrot
2017-10-03	Merge PR #1040: Efficient fresh name generation	Maxime Dénès
2017-09-29	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias
2017-09-28	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot
2017-09-26	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès
2017-09-19	Remove STM vernaculars.	Maxime Dénès
2017-09-19	Don't lose names in UState.universe_context.	Gaëtan Gilbert
2017-09-19	Allow declaring universe constraints at definition level.	Matthieu Sozeau
2017-09-15	Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...	Maxime Dénès
2017-09-15	Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...	Maxime Dénès
2017-09-15	Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.	Maxime Dénès
2017-09-14	Using an algebraic type for distinguishing toplevel input from location in file.	Hugo Herbelin
2017-09-12	Port is_Set and is_Type to EConstr, as was is_Prop already.	Guillaume Melquiond
2017-09-08	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert
2017-09-07	Merge PR #931: Parametrize module body	Maxime Dénès
2017-09-07	Merge PR #914: Making the detyper lazy	Maxime Dénès
2017-09-07	Merge PR #904: Add build_coq_or to API.Coqlib	Maxime Dénès
2017-09-04	Making detyping potentially lazy.	Pierre-Marie Pédrot
2017-08-29	[general] Merge parsing with highparsing, put toplevel at the top of the link...	Emilio Jesus Gallego Arias
2017-08-29	[vernac] Store Infix Modifier in Vernac Notation.	Pierre-Marie Pédrot
2017-08-29	Statically enforcing that module types have no retroknowledge.	Pierre-Marie Pédrot
2017-08-29	Separating the module_type and module_body types by using a type parameter.	Pierre-Marie Pédrot
2017-08-29	Post-merge API fix.	Maxime Dénès
2017-08-29	Merge PR #946: Functional pretyping interface	Maxime Dénès
2017-08-29	Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...	Maxime Dénès
2017-08-29	Merge PR #805: Functional tactics	Maxime Dénès
2017-08-29	A new step of restructuration of notations.	Hugo Herbelin
2017-08-16	Merge PR #912: Detyping functions are now operating on EConstr.t.	Maxime Dénès
2017-08-16	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès
2017-08-07	Add build_coq_or to API	Sigurd Schneider
2017-08-01	Move type_uconstr to Tacinterp.	Maxime Dénès
2017-08-01	Remove pure_open_constr (now open_constr)	Maxime Dénès