aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
AgeCommit message (Expand)Author
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-11-21Writing Tactics.keep in the new monad.Pierre-Marie Pédrot
2014-11-20Fixing the previous commit. We had to normalize evars first.Pierre-Marie Pédrot
2014-11-20Somehow fixing a side-effect bug in tactics-in-terms.Pierre-Marie Pédrot
2014-11-19Print [uconstr]-s in [idtac] messages.Arnaud Spiwack
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-10Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).Pierre-Marie Pédrot
2014-11-09Fixing bug #3803.Pierre-Marie Pédrot
2014-11-09Removing the unused boolean flag from the move tactic implementation.Pierre-Marie Pédrot
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-07Print [rename] tactic properly in info trace.Arnaud Spiwack
2014-11-03Writing rename_hyps in the new monad.Pierre-Marie Pédrot
2014-11-01Info: the warning message of the defunct [info] tactic now points to the [Inf...Arnaud Spiwack
2014-11-01Info: print name of calls to Ltac constants ([TacCall]).Arnaud Spiwack
2014-11-01Info: tactic notations (TacAlias) print their names.Arnaud Spiwack
2014-11-01Info: Tactics coming from [TACTIC EXTEND] print their names.Arnaud Spiwack
2014-11-01Info: print the name of atomic tactics.Arnaud Spiwack
2014-11-01Info: Ltac's idtac logs its message in the info trace.Arnaud Spiwack
2014-10-27Making destruct on idents with maximal implicit arguments working, byHugo Herbelin
2014-10-27Fixing evars lost in interpretation of eliminator of destruct.Hugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-22Specializing tclBREAK so that it can choose the return exception in casePierre-Marie Pédrot
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-10-22Make names in [Proofview_monad] more uniform.Arnaud Spiwack
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-16Goal: remove some functions from the compatibility layer.Arnaud Spiwack
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-24Using an or_var rather than the hack with loc for coding a pure identHugo Herbelin
2014-09-24Added support for interpreting hyp lists in tactic notations.Hugo Herbelin
2014-09-17Fix bug #3633 properly, by delaying the interpetation of constrs inMatthieu Sozeau
2014-09-15Ltac names in binders: some Ltac values can be seen both as terms and identif...Arnaud Spiwack
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-10Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Hugo Herbelin
2014-09-09Displaying genarg tag in idtac.Pierre-Marie Pédrot
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-09-08Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].Arnaud Spiwack
2014-09-08The [constr:(…)] Ltac construction now shares the same context as [uconstr:...Arnaud Spiwack
2014-09-06Inlining code in Tacinterp that was only used once.Pierre-Marie Pédrot
2014-09-06Code simplification in Tacinterp.Pierre-Marie Pédrot
2014-09-06Adding a way to inject tactic closures in interpretation values.Pierre-Marie Pédrot
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-09-05Retype terms resulting from the feeding of a context with a term.Pierre-Marie Pédrot
2014-09-05Ltac's [uconstr] values now use the identifier context to give names to binders.Arnaud Spiwack
2014-09-05Adds an identifier context in pretying's Ltac context.Arnaud Spiwack
2014-09-05Adding a Ftactic module for potentially focussing tactics.Pierre-Marie Pédrot
2014-09-05At last a working clearbody!Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 05:48:55 +0000