aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
Commit message (Expand)AuthorAge
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
* [info_auto] & [info_trivial]: warning message to help users find [Info].Gravatar Arnaud Spiwack2015-02-24
* [info] tactical warning: do not suggest [info_auto] and [info_trivial].Gravatar Arnaud Spiwack2015-02-24
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Revert "Removing spurious tclWITHHOLES."Gravatar Pierre-Marie Pédrot2015-02-10
* Tentative workaround for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* A global [gfail] tactic which works like [fail] except that it fails even if ...Gravatar Arnaud Spiwack2014-12-23
* Remove compatibility layer from Ltac's [fail].Gravatar Arnaud Spiwack2014-12-23
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Writing Tactics.keep in the new monad.Gravatar Pierre-Marie Pédrot2014-11-21
* Fixing the previous commit. We had to normalize evars first.Gravatar Pierre-Marie Pédrot2014-11-20
* Somehow fixing a side-effect bug in tactics-in-terms.Gravatar Pierre-Marie Pédrot2014-11-20
* Print [uconstr]-s in [idtac] messages.Gravatar Arnaud Spiwack2014-11-19
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).Gravatar Pierre-Marie Pédrot2014-11-10
* Fixing bug #3803.Gravatar Pierre-Marie Pédrot2014-11-09
* Removing the unused boolean flag from the move tactic implementation.Gravatar Pierre-Marie Pédrot2014-11-09
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* Print [rename] tactic properly in info trace.Gravatar Arnaud Spiwack2014-11-07
* Writing rename_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-11-03
* Info: the warning message of the defunct [info] tactic now points to the [Inf...Gravatar Arnaud Spiwack2014-11-01
* Info: print name of calls to Ltac constants ([TacCall]).Gravatar Arnaud Spiwack2014-11-01
* Info: tactic notations (TacAlias) print their names.Gravatar Arnaud Spiwack2014-11-01
* Info: Tactics coming from [TACTIC EXTEND] print their names.Gravatar Arnaud Spiwack2014-11-01
* Info: print the name of atomic tactics.Gravatar Arnaud Spiwack2014-11-01
* Info: Ltac's idtac logs its message in the info trace.Gravatar Arnaud Spiwack2014-11-01
* Making destruct on idents with maximal implicit arguments working, byGravatar Hugo Herbelin2014-10-27
* Fixing evars lost in interpretation of eliminator of destruct.Gravatar Hugo Herbelin2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Specializing tclBREAK so that it can choose the return exception in caseGravatar Pierre-Marie Pédrot2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Goal: remove some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-10-16
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
* Added support for interpreting hyp lists in tactic notations.Gravatar Hugo Herbelin2014-09-24
* Fix bug #3633 properly, by delaying the interpetation of constrs inGravatar Matthieu Sozeau2014-09-17
* Ltac names in binders: some Ltac values can be seen both as terms and identif...Gravatar Arnaud Spiwack2014-09-15
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 07:23:55 +0000