coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-11	Modify Strings/String.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Strings/Ascii.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Vectors/VectorEq.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Vectors/VectorSpec.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Vectors/VectorDef.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Vectors/Fin.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify micromega/OrderedRing.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Arith/Euclid.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Arith/Div2.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Arith/Even.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify setoid_ring/Ring.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify setoid_ring/InitialRing.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Similarly remove the explicit graph argument in the ~evar conversion API.	Pierre-Marie Pédrot
2020-10-11	Pick the universe graph out of the environment in conversion API.	Pierre-Marie Pédrot
2020-10-11	Remove the compare_graph field from the conversion API.	Pierre-Marie Pédrot
2020-10-11	Fix #13169: vm_compute has existential crisis.	Pierre-Marie Pédrot
2020-10-10	Adding change log for #12950.	Hugo Herbelin
2020-10-10	Documenting the new only-parsing only-printing model.	Hugo Herbelin
2020-10-10	New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.	Hugo Herbelin
2020-10-10	Adding a warning in case a notation is used neither for parsing nor printing.	Hugo Herbelin
2020-10-10	Notations: reworking the treatment of only-parsing and only-printing notations.	Hugo Herbelin
2020-10-10	Splitting ssrbool's multi-printing notations into parsing and printing.	Hugo Herbelin
2020-10-10	Notation.ml: Move interpretation_eq earlier for future use.	Hugo Herbelin
2020-10-10	Print Scope & cie: Add parentheses around notation interpretation.	Hugo Herbelin
2020-10-10	Prim.pattern_ident takes a location and its synonymous pattern_identref is de...	Hugo Herbelin
2020-10-10	Add location in existential variable names (CEvar/GEvar).	Hugo Herbelin
2020-10-10	Adding and using locations on identifiers in constr_expr where they were miss...	Hugo Herbelin
2020-10-10	Closes #13142 (more standardized pretty-printing of records).	Hugo Herbelin
2020-10-10	Merge PR #13164: [bench] Dump the vo size difference.	coqbot-app[bot]
2020-10-09	Add an XML message for "Show Proof Diffs"	Jim Fehrle
2020-10-09	Modify ZArith/ZArith_dec.v to compile with -mangle-names	Jasper Hugunin
2020-10-09	Modify Bool/Sumbool.v to compile with -mangle-names	Jasper Hugunin
2020-10-09	Update pretyping/detyping.ml	Enrico Tassi
2020-10-09	Merge PR #13088: [stm] move par: to comTactic	coqbot-app[bot]
2020-10-09	overlay for mtac2	Enrico Tassi
2020-10-09	[stm] move par: implementation to vernac/comTactic and stm/partac	Enrico Tassi
2020-10-09	Merge PR #13143: Drop misleading argument of Pp.h box	coqbot-app[bot]
2020-10-09	improve comment	Enrico Tassi
2020-10-09	[bench] Dump the vo size difference.	Pierre-Marie Pédrot
2020-10-09	overlay for minim-prop-toset	Gaëtan Gilbert
2020-10-09	No bidirectionality when expected type for lambda is an evar.	Gaëtan Gilbert
2020-10-09	Minimize Prop <= i to i := Set	Gaëtan Gilbert
2020-10-09	Merge PR #13087: Put type-in-type flag in ugraph.	Pierre-Marie Pédrot
2020-10-09	Store the resolver of required modules as functor parameters in safe_env.	Pierre-Marie Pédrot
2020-10-09	[printing] make detyping resilient to "let x : _ := t in"	Enrico Tassi
2020-10-08	Modify ZArith/Zorder.v to compile with -mangle-names	Jasper Hugunin
2020-10-08	Modify setoid_ring/Ring_polynom.v to compile with -mangle-names	Jasper Hugunin
2020-10-08	Modify ZArith/BinInt.v to compile with -mangle-names	Jasper Hugunin
2020-10-08	Modify Numbers/Integer/Abstract/ZBits.v to compile with -mangle-names	Jasper Hugunin
2020-10-08	Modify Numbers/Integer/Abstract/ZLcm.v to compile with -mangle-names	Jasper Hugunin