coq - The formal proof system

Age	Commit message (Expand)	Author
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-25	Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...	Maxime Dénès
2017-09-25	Merge PR #1057: Reporting locations in error messages about notation formats.	Maxime Dénès
2017-09-23	Discharge.ml: cosmetic renaming of some variables.	Hugo Herbelin
2017-09-23	Fixing #5755 (discharging of inductive types not correct with let-ins).	Hugo Herbelin
2017-09-22	Merge PR #1055: Remove STM vernaculars	Maxime Dénès
2017-09-20	[flags] Flag `open Flags`	Emilio Jesus Gallego Arias
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	proof_global: cleanup and comment close_proof	Matthieu Sozeau
2017-09-19	Allow declaring universe constraints at definition level.	Matthieu Sozeau
2017-09-18	Reporting locations in error messages about notation formats.	Hugo Herbelin
2017-09-18	Fixing two anomalies in corner cases of the syntax of notation formats.	Hugo Herbelin
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-15	Merge PR #1037: Parse directly to Sorts.family when appropriate.	Maxime Dénès
2017-09-15	Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...	Maxime Dénès
2017-09-14	Using an algebraic type for distinguishing toplevel input from location in file.	Hugo Herbelin
2017-09-12	Fixing bug #5693 (treating empty notation format as any format).	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-04	Making detyping potentially lazy.	Pierre-Marie Pédrot
2017-08-31	Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name	Maxime Dénès
2017-08-30	Fixing a capitalization in the middle of the sentence of an error message.	Hugo Herbelin
2017-08-29	[vernac] Store Infix Modifier in Vernac Notation.	Pierre-Marie Pédrot
2017-08-29	Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170	Maxime Dénès
2017-08-29	Merge PR #946: Functional pretyping interface	Maxime Dénès
2017-08-29	Quoting notations in incompatible-level error message.	Hugo Herbelin
2017-08-29	A new step of restructuration of notations.	Hugo Herbelin
2017-08-29	Dropping former fix to bug #5469 (notation format not recognizing curly braces).	Hugo Herbelin
2017-08-29	A little reorganization of notations + a fix to #5608.	Hugo Herbelin
2017-08-29	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin
2017-08-17	Add native compute profiling, BZ#5170	Paul Steckler
2017-08-16	Merge PR #912: Detyping functions are now operating on EConstr.t.	Maxime Dénès
2017-08-16	Merge PR #841: Timorous fix of bug #5598 on global existing class in sections	Maxime Dénès
2017-08-16	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès
2017-08-01	Remove understand_tcc_evars.	Maxime Dénès
2017-08-01	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot
2017-08-01	Merge PR #919: Remove a few useless evar-normalizations in printing code.	Maxime Dénès
2017-08-01	Merge PR #834: Adding support for recursive notations of the form "x , .. , y...	Maxime Dénès
2017-07-31	Improve errors for cumulativity when monomorphic	Amin Timany
2017-07-31	Change the option for cumulativity	Amin Timany
2017-07-31	Issue error on monomorphic cumulative inductives	Amin Timany
2017-07-31	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík
2017-07-26	Remove a few useless evar-normalizations in printing code.	Pierre-Marie Pédrot