coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-10-04	rename test files (do not start by a digit)	Vincent Laporte

2018-03-30	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin

2018-03-04	Remove deprecated options related to typeclasses.	Théo Zimmermann

2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin

2016-11-15	Revert part of a477dc, disallow_shelved	Matthieu Sozeau
	In only_classes mode we do not try to implement a stricter semantics for shelved goals in 8.6. Leaving this for 8.7. Update the documentation as well. Remove a spurious printf call as well. Fix test-suite now that shelved goals are allowed
2016-11-03	Fix handling of only_classes at toplevel	Matthieu Sozeau

2015-03-11	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi
	- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
2015-03-03	Fix bug #3732: firstorder was using detyping to build existential	Matthieu Sozeau
	instances and forgeting about the evars and universes that could appear there... dirty hack gone, using the evar map properly and avoiding needless constructions/deconstructions of terms.