aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacintern.mli
AgeCommit message (Collapse)Author
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2015-02-27Removing the unused field ltacrecvars of tactic internalization.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-09-03Useless hooks in Tacintern.Pierre-Marie Pédrot
2014-08-31Getting rid of atomic tactics in Tacenv.Pierre-Marie Pédrot
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.
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
potentially conflicting tactics names from different plugins.
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
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.
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
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.
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-03Replacing an association list by a map in globalizing environment.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16654 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Removed the distinction between generic Ltac vars and Let/Introppedrot
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
2013-06-21Splitted up Genarg in four different levels:ppedrot
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
2013-06-18Removing the various glob/subst/interp registering functions forppedrot
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
2013-06-18Now glob_sign and interp_sign only depend on structures definedppedrot
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
2013-05-29Make ist (interp_sign) available to TACTIC EXTEND codegareuselesinge
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
2012-12-14Modulification of identifierppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:07:50 +0000