coq - The formal proof system

Age	Commit message (Expand)	Author
2017-04-13	update XML protocol doc to 8.6	Paul Steckler
2017-04-13	add XML protocol doc for 8.5	Paul Steckler
2017-04-13	Reinstate fixpoint refolding in [cbn], deactivated by mistake.	Matthieu Sozeau
2017-04-13	[toplevel] Don't print goals if there is no pending proof.	Emilio Jesus Gallego Arias
2017-04-13	Using fold_glob_constr_with_binders to code bound_glob_vars.	Hugo Herbelin
2017-04-13	Adding a fold_glob_constr_with_binders combinator.	Hugo Herbelin
2017-04-13	Silence a few OCaml warnings.	Guillaume Melquiond
2017-04-12	Merge PR#510: Correctly identify [Time Defined.] as a defined	Maxime Dénès
2017-04-12	Merge PR#441: Port Toplevel to the Stm API	Maxime Dénès
2017-04-12	[toplevel] [stm] cleanup in module open	Emilio Jesus Gallego Arias
2017-04-12	[stm] [nit] Centralize compile-time debug flag.	Emilio Jesus Gallego Arias
2017-04-12	[stm] Improve error messages on add/parse.	Emilio Jesus Gallego Arias
2017-04-12	[flags] Documentation and a minor tweak.	Emilio Jesus Gallego Arias
2017-04-12	[vernac] vernacentries.mli cleanup	Emilio Jesus Gallego Arias
2017-04-12	[stm] Port the toplevel to the STM.	Emilio Jesus Gallego Arias
2017-04-12	[stm] Move main parsing entry point to the STM.	Emilio Jesus Gallego Arias
2017-04-12	[stm] Remove edit_id.	Emilio Jesus Gallego Arias
2017-04-12	Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...	Maxime Dénès
2017-04-12	Missing optimization when Kernel Term Sharing is disabled.	Pierre-Marie Pédrot
2017-04-11	Merge PR#549: Fast path in weak head reduction of applied atoms.	Maxime Dénès
2017-04-11	Update INSTALL now that -debug is the default.	Théo Zimmermann
2017-04-11	Merge PR#543: Sanitize instance interpretation	Maxime Dénès
2017-04-11	Update RefMan-pre to mention template polymorphism.	Gaetan Gilbert
2017-04-11	Update various comments to use "template polymorphism"	Gaetan Gilbert
2017-04-11	Use "template polymorphism" in the documentation.	Gaetan Gilbert
2017-04-11	Mention template polymorphism in the documentation.	Gaetan Gilbert
2017-04-11	Merge PR#532: Clean Nsatz implementation.	Maxime Dénès
2017-04-11	Merge PR#537: Efficient side-effect abstraction	Maxime Dénès
2017-04-11	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès
2017-04-10	Adding a test for 'rewrite in *' when an evar is solved by side-effect.	Pierre-Marie Pédrot
2017-04-10	Adding a test for the correctness of normalization in legacy typeclasses.	Pierre-Marie Pédrot
2017-04-10	Documenting the changes introduced by the EConstr branch.	Pierre-Marie Pédrot
2017-04-10	Revert "refactoring: Reductionops.contextual_reduction_function type"	Matej Košík
2017-04-10	Revert "comment: typo"	Matej Košík
2017-04-10	Revert "refactoring: Names.DirPath.equal"	Matej Košík
2017-04-10	Revert "refactoring: Names.DirPath.compare"	Matej Košík
2017-04-10	Revert "refactoring: Names.DirPath.is_empty"	Matej Košík
2017-04-10	Revert "simplify: Environ.push_named"	Matej Košík
2017-04-10	Revert "trivial"	Matej Košík
2017-04-10	Revert "trivial"	Matej Košík
2017-04-10	Revert "comments: corrected in the Context module"	Matej Košík
2017-04-10	comments: corrected in the Context module	Matej Kosik
2017-04-10	trivial	Matej Kosik
2017-04-10	trivial	Matej Kosik
2017-04-10	simplify: Environ.push_named	Matej Kosik
2017-04-10	refactoring: Names.DirPath.is_empty	Matej Kosik
2017-04-10	refactoring: Names.DirPath.compare	Matej Kosik
2017-04-10	refactoring: Names.DirPath.equal	Matej Kosik
2017-04-10	comment: typo	Matej Kosik
2017-04-10	refactoring: Reductionops.contextual_reduction_function type	Matej Kosik