aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2014-09-08Removing antiquotations in Tauto.Pierre-Marie Pédrot
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-09-08Display number of available goals in "incorrect number of goals" error message.Arnaud Spiwack
2014-09-08Fix [induction] wrt inductive records and non-recursive variants.Arnaud Spiwack
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-08Add a tactic [revgoals] to reverse the list of focused goals.Arnaud Spiwack
2014-09-07A better check that an "as" clause has been given to inversion, soHugo Herbelin
2014-09-07Fixing a bug in intros_replacing which was causing inversion notHugo Herbelin
2014-09-07Fixing "simple inversion as" (bug #2164).Hugo Herbelin
2014-09-07Dead code in inv.ml.Hugo Herbelin
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-06Proper interpretation function for tauto.Pierre-Marie Pédrot
2014-09-06Adding a way to inject tactic closures in interpretation values.Pierre-Marie Pédrot
2014-09-06Fixing clearbody : typecheck definitions in context.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-05Remove a redundant typing phase in the [refine] tactic.Arnaud Spiwack
2014-09-05Silence an ocaml warning.Arnaud Spiwack
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-05Fix parsing of "subterm(s)" strategy argument.Matthieu Sozeau
2014-09-05Adding a Ftactic module for potentially focussing tactics.Pierre-Marie Pédrot
2014-09-05Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-05At last a working clearbody!Pierre-Marie Pédrot
2014-09-04Revert the two previous commits. I was testing in the wrong branch.Pierre-Marie Pédrot
2014-09-04Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-04Reimplementing the clearbody tactic.Pierre-Marie Pédrot
2014-09-04Proofview refiner is now type-safe by default.Pierre-Marie Pédrot
2014-09-04Typing.sort_of does not leak evarmaps anymore.Pierre-Marie Pédrot
2014-09-04Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Pierre-Marie Pédrot
2014-09-04Using goal-tactics to interpret arguments to idtac.Pierre-Marie Pédrot
2014-09-04Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Pierre-Marie Pédrot
2014-09-04Revert "Tacinterp: [interp_message] and associate now only require an environ...Pierre-Marie Pédrot
2014-09-04Revert "Ltac's idtac is now implemented using the new API."Pierre-Marie Pédrot
2014-09-04Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."Pierre-Marie Pédrot
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-09-03Putting back normalized goals when entering them.Pierre-Marie Pédrot
2014-09-03Yes another remaining clearing bug with 'apply in'.Hugo Herbelin
2014-09-03Fixing bug #2818.Pierre-Marie Pédrot
2014-09-03Useless hooks in Tacintern.Pierre-Marie Pédrot
2014-09-03Code simplification in Tacenv.Pierre-Marie Pédrot
2014-09-03Code factorization in Tacintern.Pierre-Marie Pédrot
2014-09-02Another fix than 19a7a5789c to avoid descend_in_conjunction to useHugo Herbelin
2014-09-02Removing [revert] tactic from the AST.Pierre-Marie Pédrot
2014-09-01Moving the decompose tactic out of the AST.Pierre-Marie Pédrot
2014-09-01Code cleaning in Tacintern.Pierre-Marie Pédrot
2014-08-31Getting rid of atomic tactics in Tacenv.Pierre-Marie Pédrot
2014-08-31Moving code of tactic interpretation from Tacenv to Vernacentries.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 11:58:28 +0000