coq - The formal proof system

Age	Commit message (Collapse)	Author
2012-03-14	Final part of moving Program code inside the main code. Adapted ↵	msozeau
	add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14	Second step of integration of Program:	msozeau
	- Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
	There was a discrepancy of the notions "raw" and "globalized" between constrs and tactics, and some confusion of the notions in e.g. genarg.mli (see all globwit_* there). This commit is a first step towards unification of terminology between constrs and tactics. Changes in module names will be done separately. In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even affected by this change, has not been touched and highlights another confusion in "ARGUMENT EXTEND" in general that will be addressed later. The funind plugin doesn't respect the same naming conventions as the rest, so leave some "raw" there for now... they will be addressed later. This big commit has been generated with the following command (wrapped here, but should be on a single line): perl -pi -e 's/(\W(?:\|pp\|pr_l)\|_)raw((?:constrs?\|type\|vars\|_binder\| _context\|decl\|_decompose\|_compose\|_make)(?:\W\|_))/\1glob_\2/g;s/glo b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref\|Var\|Evar\|PatVar\|App\|Lam bda\|Prod\|LetIn\|Cases\|LetTuple\|If\|Rec\|Sort\|Hole\|Cast\|Dynamic)\W)/\1G \2/g' `git ls-files\|grep -v dev/doc/changes.txt` git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-27	Minor fixes:	msozeau
	- Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-16	Support for definition hooks in subtac.	msozeau
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12126 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey
	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7