coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Removing Convert_concl and Convert_hyp from Logic.	Hugo Herbelin	2014-10-09
*	A version of convert_concl and convert_hyp in new proof engine.	Hugo Herbelin	2014-10-09
*	A few Global.env removed.	Hugo Herbelin	2014-10-04
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Removing the old implementation of clear_body.	Pierre-Marie Pédrot	2014-09-05
*	Revert the two previous commits. I was testing in the wrong branch.	Pierre-Marie Pédrot	2014-09-04
*	Removing the old implementation of clear_body.	Pierre-Marie Pédrot	2014-09-04
*	Move UnsatisfiableConstraints to a pretype error.	Matthieu Sozeau	2014-08-22
*	Reorganization of tactics:	Hugo Herbelin	2014-08-18
*	A new step in the new "standard" naming policy for propositional hypotheses	Hugo Herbelin	2014-08-05
*	Fixing "clear" in internal_cut_replace: forbid dependencies in the	Hugo Herbelin	2014-06-13
*	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin	2014-06-04
*	Use of "H"-based names for propositional hypotheses obtained by	Hugo Herbelin	2014-06-01
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Fix interface for template polymorphism, cleaning up code in all typing algor...	Matthieu Sozeau	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Removing the Change_evar refiner rule.	Pierre-Marie Pédrot	2014-03-31
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	More sharing in Logic, together with some code cleaning.	Pierre-Marie Pédrot	2014-02-21
*	Tracking memory misallocation by trying to improve sharing.	Pierre-Marie Pédrot	2014-02-03
*	Algebraized "No such hypothesis" errors	Pierre-Marie Pédrot	2014-01-06
*	Useless array to list conversions in proof/logic.ml.	ppedrot	2013-10-28
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Replacing lists by sets in clear tactic.	ppedrot	2013-08-25
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Getting rid of LtacLocated exception transformer.	ppedrot	2013-05-28
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Fixing #2968. This is quite brittle though, because we are messing	ppedrot	2013-04-16
*	Allow catching of WrongAbstractionType, fixing a regression from 8.4	msozeau	2013-04-05
*	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
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Revised the Ltac trace mechanism so that trace breaking due to	herbelin	2013-02-17
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot	2012-12-13
*	Monomorphization (proof)	ppedrot	2012-11-25
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14