coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-02	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-10-24	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-23	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-18	declaration_hooks use Ephemeron	gareuselesinge
2013-10-16	Reintroduce "or" instead of "\|\|" as the latter is redifined in "sos_lib.ml" w...	xclerc
2013-10-14	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-05	Moving side effects into evar_map. There was no reason to keep another	ppedrot
2013-09-30	STM: better handle proof modes	gareuselesinge
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-02	Removing more association lists in Constrintern.	ppedrot
2013-08-30	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-25	Added a more efficient way to recover the domain of a map.	ppedrot
2013-08-23	Fixing an incompleteness of the ring/field tactics	amahboub
2013-08-22	Correcting misplaced Proof command.	amahboub
2013-08-22	Fixing a significant efficiency leak in the code of the field tactic.	amahboub
2013-08-22	Nicer code concerning dirpaths and modpath around Lib	letouzey
2013-08-22	Misc changes around coqtop.ml :	letouzey
2013-08-22	Less "Coq" strings everywhere	letouzey
2013-08-22	micromega: remove empty file CheckerMaker	letouzey
2013-08-22	Field_theory : faster and nicer proofs + nice notations.	letouzey
2013-08-22	Ring_polynom : shorter proof for Psub_ok	letouzey
2013-08-20	Declarations.mli: reorganization of modular structures	letouzey
2013-08-08	calling interp by hand is forbidden	gareuselesinge