coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix previous merge.	Maxime Dénès	2015-09-17
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\
\| *	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
* \|	Opacifying the proof_terminator type.	Pierre-Marie Pédrot	2015-09-08
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Removing the generalization of the body of inductive schemes from	Hugo Herbelin	2015-08-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-29
\|\\|
\| *	Fixing what seems to be a typo.	Hugo Herbelin	2015-07-29
\| *	Slightly improving line break formatting in Info command.	Hugo Herbelin	2015-07-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-24
\|\\|
\| *	Fix `Pp` function used by the `Info` command.	Arnaud Spiwack	2015-06-23
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	STM: states coming from workers have no proof terminators (Close #4246)	Enrico Tassi	2015-06-09
\| *	Admitted does not drop poly-univ constraints (Fix #4244)	Enrico Tassi	2015-06-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|\\|
\| *	STM/Univ: save initial univs (the ones in the statement) in Proof.proof	Enrico Tassi	2015-05-29
\| *	Fix bug #4159	Matthieu Sozeau	2015-05-27
\| *	Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...	Pierre-Marie Pédrot	2015-05-18
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Disable precompilation for native_compute by default.	Guillaume Melquiond	2015-05-14
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
* \|	Exposing the minimal amount of internal of the Logic monad in order to	Pierre-Marie Pédrot	2015-05-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| *	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22
\| *	Slightly more efficient implementation of the logic monad.	Pierre-Marie Pédrot	2015-04-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	typo	Enrico Tassi	2015-03-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
* \|	Moving Proofview_monad to the engine/ folder.	Pierre-Marie Pédrot	2015-02-28
* \|	Adding a new folder corresponding to the low-level part of the pretyper	Pierre-Marie Pédrot	2015-02-27
\|/
*	[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...	Arnaud Spiwack	2015-02-24
*	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
*	Granting wish #4008.	Pierre-Marie Pédrot	2015-02-10
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Tentative workaround for bug #3798.	Pierre-Marie Pédrot	2015-01-24
*	Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it was	Maxime Dénès	2015-01-18
*	Update headers.	Maxime Dénès	2015-01-12
*	Avoiding introducing yet another convention in naming files.	Hugo Herbelin	2015-01-08
*	Fixed and extend bullet related info/error messages. + doc.	Pierre Courtieu	2015-01-08
*	Added more informative messages about bullets.	Pierre Courtieu	2015-01-05
*	Call nf_constraints also when compiling directly to vo	Enrico Tassi	2014-12-28
*	Proof using: call "clear" to remove from sight the vars not selected	Enrico Tassi	2014-12-28
*	remove debug prints (leftover)	Enrico Tassi	2014-12-28
*	proof_global: make it possible to call close_proof in a worker	Enrico Tassi	2014-12-27
*	Call Evd.nf_constraints only on Univ Poly constants	Enrico Tassi	2014-12-26
*	Vi2vo: fix handling of univ constraints coming from the body	Enrico Tassi	2014-12-23
*	Better doc and a few fixes for Proof using.	Enrico Tassi	2014-12-19
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18