coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Useless hooks in Tacintern.	Pierre-Marie Pédrot	2014-09-03
\|
*	Getting rid of atomic tactics in Tacenv.	Pierre-Marie Pédrot	2014-08-31
\| \| \| \| \| \|	ML tactics that may be used as simple identifiers are now declared as a true Ltac entry pertaining to the module that contains the Declare ML Module statement.
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
\| \| \| \|	potentially conflicting tactics names from different plugins.
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
\| \| \| \| \| \| \| \|	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
\| \| \| \| \| \|	Actually, this was wrong, as evars should not appear until interpretation. Evarmaps were only passed around uselessly, and often fed with dummy or irrelevant values.
*	Centralizing the Ltac-defining functions in Tacenv.	ppedrot	2013-11-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Replacing an association list by a map in globalizing environment.	ppedrot	2013-08-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16654 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed the distinction between generic Ltac vars and Let/Intro	ppedrot	2013-06-27
\| \| \| \| \| \| \| \| \| \| \| \|	bindings, which permits using only one environment for interning terms. Ltac semantics was sligthly changed, as it required introducing a lot of additional coercions from goal variables to other types. Ltac seemed to be quite non-uniform, as it tried to represent hypotheses with intropatterns, instead of the dedicated var type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16612 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Splitted up Genarg in four different levels:	ppedrot	2013-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \|	1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing the various glob/subst/interp registering functions for	ppedrot	2013-06-18
\| \| \| \| \| \|	extra argument types and putting them into Genarg. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16586 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Now glob_sign and interp_sign only depend on structures defined	ppedrot	2013-06-18
\| \| \| \| \| \| \|	upto Genarg, so moved them there. This will allow defining the new genarg interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16584 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Make ist (interp_sign) available to TACTIC EXTEND code	gareuselesinge	2013-05-29
\| \| \| \| \| \| \|	In order to do so I had to move the data base of tactics to tacinterp (from tacintern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16540 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of identifier	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7