coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	msg_info now puts infomsg tag in emacs mode.	Pierre Courtieu	2014-12-16
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Make sure the goals on the shelve are identified as goal and unresolvable for...	Arnaud Spiwack	2014-12-12
*	An option SimplIsCbn	Pierre Boutillier	2014-12-12
*	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack	2014-12-12
*	Exporting store of goals so that new_evar in convert, intro, etc. can	Hugo Herbelin	2014-12-07
*	Occur-check in refine.	Arnaud Spiwack	2014-12-04
*	Refine primitive: [unsafe] is now true by default.	Arnaud Spiwack	2014-12-04
*	Some refactoring following previous commit.	Arnaud Spiwack	2014-12-04