coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
*	Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35.	Arnaud Spiwack	2014-12-04
*	Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075.	Arnaud Spiwack	2014-12-04
*	Fixing bug #3682.	Pierre-Marie Pédrot	2014-11-30
*	Adding missing unsafe primitives to Proofview.	Pierre-Marie Pédrot	2014-11-30
*	Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.	Arnaud Spiwack	2014-11-28
*	Tactic primitives: missing [advance] lead to spurious dangling goals.	Arnaud Spiwack	2014-11-28
*	One more word about "simpl f": avoid "simpl f" to be printed "simpl f",	Hugo Herbelin	2014-11-23
*	Removing useless flag of the historical move tactic.	Pierre-Marie Pédrot	2014-11-22
*	Exporting a primitive allowing to run completely the tactic monad.	Pierre-Marie Pédrot	2014-11-22
*	Exporting the function handling side-effects only applied to terms.	Pierre-Marie Pédrot	2014-11-20
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	new: Optimize Proof, Optimize Heap	Enrico Tassi	2014-11-09
*	Follow up to experimental eager evar unification in bcba6d1bc9:	Hugo Herbelin	2014-11-08
*	Removing the legacy intro tactic code.	Pierre-Marie Pédrot	2014-11-07
*	Removing the old rename tactic.	Pierre-Marie Pédrot	2014-11-04
*	Plural and singular forms in error messages.	Hugo Herbelin	2014-11-02
*	Info: do not record info trace unless needed.	Arnaud Spiwack	2014-11-01
*	Info: print a name for the primitive tactics in [Proofview].	Arnaud Spiwack	2014-11-01
*	Info: dispatching-branches are declared as such in the info trace.	Arnaud Spiwack	2014-11-01
*	Add [Info] command.	Arnaud Spiwack	2014-11-01
*	An API for info traces.	Arnaud Spiwack	2014-11-01
*	Cleaning and documenting Clenv.make_evar_clause	Pierre-Marie Pédrot	2014-10-27
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25