coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Revised the Ltac trace mechanism so that trace breaking due to	herbelin	2013-02-17
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (proof)	ppedrot	2012-11-25
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	remove Refiner.abstract_tactic and similar	letouzey	2012-10-06
*	Clean-up : removal of Proof_type.tactic_expr	letouzey	2012-10-06
*	Proof_type: rule now degenerates to prim_rule	letouzey	2012-10-06
*	Clean-up : no more Proof_type.proof_tree	letouzey	2012-10-06
*	Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box	letouzey	2012-10-06
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Use the library function List.substract in prev commit	letouzey	2012-10-02
*	Added a new tactical infoH tac, that displays the names of hypothesis created...	courtieu	2012-10-01
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey	2012-03-30
*	Noise for nothing	pboutill	2012-03-02
*	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey	2011-03-18
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fix comment	glondu	2010-06-07
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Improved the efficiency of evars traverals thanks to a split of	herbelin	2010-05-13
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Attached evar source to the evar_info and add location to tclWITHHOLES errors	herbelin	2009-12-22
*	In "progress", extending the set of evars w/o solving an existing one is	herbelin	2009-12-21
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Use a lazy value for the message in FailError, so that it won't be	msozeau	2009-06-11
*	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin	2009-05-20
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
*	pushed evar reduction in kernel	barras	2009-02-06
*	Really compare evar maps in progress, due to merging in apply and other	msozeau	2009-01-23
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	- Rebranchement backtrack du langage déclaratif dans Coqide	herbelin	2008-07-18
*	fixed catch_failerror + improved progress check + fixed repeat (repeat simpl ...	barras	2008-05-29
*	Move exception-handling code for catching tactics failure	msozeau	2008-05-01
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Adding the tactic "instantiate" (without argument), to force the	glondu	2007-12-07
*	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov	2007-04-02
*	Correction du bug #1315:	notin	2007-01-22
*	bug #1194: normalisation evars a la sortie de focus	barras	2006-10-23
*	affichage des ... dans les scripts	barras	2006-10-16
*	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey	2006-10-05
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26