index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tacinterp.mli
Commit message (
Expand
)
Author
Age
*
Tacinterp: spurious enterl.
Arnaud Spiwack
2014-02-27
*
Dead code: eval_ltac_constr.
Arnaud Spiwack
2014-02-27
*
Do not use ugly Dyn features in the Quote plugin. Use instead the
Pierre-Marie Pédrot
2013-11-26
*
Tacinterp: fewer use of old-style goals.
Arnaud Spiwack
2013-11-25
*
Centralizing the Ltac-defining functions in Tacenv.
ppedrot
2013-11-10
*
Made multiple-goal tactic work after all: .
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-11-02
*
Cleaning up the type of Tacinterp.extract_ltac_constr_values.
ppedrot
2013-06-24
*
Now, idtac closures use maps instead of association list.
ppedrot
2013-06-22
*
Generalizing the use of maps instead of lists in the interpretation
ppedrot
2013-06-22
*
Splitted up Genarg in four different levels:
ppedrot
2013-06-21
*
Removing the various glob/subst/interp registering functions for
ppedrot
2013-06-18
*
Now glob_sign and interp_sign only depend on structures defined
ppedrot
2013-06-18
*
Exporting field f_debug (needed for Ssreflect).
ppedrot
2013-06-14
*
Using an "extra" Store.t field in interp_sign instead of dedicated
ppedrot
2013-06-14
*
Moving coercion functions out of Tacinterp.
ppedrot
2013-06-12
*
Hiding tactic value representations.
ppedrot
2013-06-10
*
Replacing lists by maps in matching interpretation.
ppedrot
2013-06-05
*
Make ist (interp_sign) available to TACTIC EXTEND code
gareuselesinge
2013-05-29
*
Modulification of identifier
ppedrot
2012-12-14
*
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
letouzey
2012-10-16
*
Updating headers.
herbelin
2012-08-08
*
Dump references in reduction tactics
pboutill
2012-08-05
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Corrects a (very) longstanding bug of tactics. As is were, tactic expecting
aspiwack
2012-04-18
*
Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic
herbelin
2012-03-20
*
Noise for nothing
pboutill
2012-03-02
*
Fixing bug #2640 and variants of it (inconsistency between when and
herbelin
2011-11-17
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
Moving implicit tactic support from Tacinterp to Pfedit and final evar
herbelin
2011-09-26
*
Rename subst_raw_with_bindings to subst_glob_with_bindings and export
msozeau
2011-02-10
*
One more fix for setoid_rewrite: completely reinterpret the given lemmas
msozeau
2011-02-09
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Fixed commit 13125 (stricter check of induction args): an interpretation
herbelin
2010-06-14
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Make usage of Dyn explicit
glondu
2009-10-28
*
New cleaning phase of the Local/Global option management
herbelin
2009-10-26
[next]