coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack	2013-12-04
*	Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.	Guillaume Melquiond	2013-12-03
*	Silence compilation warning by avoiding some deprecated constructs.	Guillaume Melquiond	2013-12-03
*	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot	2013-12-02
*	Getting rid of goal-dependency in declarative mode argument evaluation.	Pierre-Marie Pédrot	2013-11-27
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Do not use ugly Dyn features in the Quote plugin. Use instead the	Pierre-Marie Pédrot	2013-11-26
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Field_theory: nicer notations for constants 0 1 ...	Pierre Letouzey	2013-11-21
*	Add Acc_intro_generator on top of all wf function proof (much much faster exe...	Julien Forest	2013-11-21
*	bugfix micromega: solved an ambiguous symbol resolution	fbesson	2013-11-15
*	Porting Tactics.assumption to the new engine.	ppedrot	2013-11-08
*	Fix congruence: normalise hypotheses with respect to evars.	aspiwack	2013-11-02
*	Made Proofview.Goal.hyps a named_context.	aspiwack	2013-11-02
*	Less use of the list-based interface for goal-bound tactics.	aspiwack	2013-11-02
*	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack	2013-11-02
*	More Proofview.Goal.enter.	aspiwack	2013-11-02
*	Small syntax fix to be compatible with Ocaml 3.11.	aspiwack	2013-11-02
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Cleanup of comments.	aspiwack	2013-11-02
*	Plug back the declarative mode.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Rtree : cleanup of the comparing code	letouzey	2013-10-24
*	Oups, repair the compilation (micromega + Morphism_prop)	letouzey	2013-10-24
*	Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml".	xclerc	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	Reintroduce "or" instead of "\|\|" as the latter is redifined in "sos_lib.ml" w...	xclerc	2013-10-16
*	Avoid polymorphic comparison (plugins/rtauto).	xclerc	2013-10-14
*	Avoid polymorphic comparison (plugins/cc).	xclerc	2013-10-14
*	Remove some uses of local modules (some were unused, some were costly).	xclerc	2013-10-14
*	Getting rid of the use of deprecated elements (from the OCaml standard library).	xclerc	2013-10-14
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	STM: better handle proof modes	gareuselesinge	2013-09-30
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Removing more association lists in Constrintern.	ppedrot	2013-09-02
*	add "Print Ring" and "Print Field" vernacular commands	gareuselesinge	2013-08-30
*	Fixing the code of field_simplify_eq.	amahboub	2013-08-30
*	recdef: restore old semantics (pre STM)	gareuselesinge	2013-08-30
*	Fix typo in error message	gareuselesinge	2013-08-30