aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Display number of available goals in "incorrect number of goals" error message.Gravatar Arnaud Spiwack2014-09-08
* Fix [induction] wrt inductive records and non-recursive variants.Gravatar Arnaud Spiwack2014-09-08
* Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].Gravatar Arnaud Spiwack2014-09-08
* The [constr:(…)] Ltac construction now shares the same context as [uconstr:...Gravatar Arnaud Spiwack2014-09-08
* Add a tactic [revgoals] to reverse the list of focused goals.Gravatar Arnaud Spiwack2014-09-08
* A better check that an "as" clause has been given to inversion, soGravatar Hugo Herbelin2014-09-07
* Fixing a bug in intros_replacing which was causing inversion notGravatar Hugo Herbelin2014-09-07
* Fixing "simple inversion as" (bug #2164).Gravatar Hugo Herbelin2014-09-07
* Dead code in inv.ml.Gravatar Hugo Herbelin2014-09-07
* Inlining code in Tacinterp that was only used once.Gravatar Pierre-Marie Pédrot2014-09-06
* Code simplification in Tacinterp.Gravatar Pierre-Marie Pédrot2014-09-06
* Proper interpretation function for tauto.Gravatar Pierre-Marie Pédrot2014-09-06
* Adding a way to inject tactic closures in interpretation values.Gravatar Pierre-Marie Pédrot2014-09-06
* Fixing clearbody : typecheck definitions in context.Gravatar Pierre-Marie Pédrot2014-09-06
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Retype terms resulting from the feeding of a context with a term.Gravatar Pierre-Marie Pédrot2014-09-05
* Remove a redundant typing phase in the [refine] tactic.Gravatar Arnaud Spiwack2014-09-05
* Silence an ocaml warning.Gravatar Arnaud Spiwack2014-09-05
* Ltac's [uconstr] values now use the identifier context to give names to binders.Gravatar Arnaud Spiwack2014-09-05
* Adds an identifier context in pretying's Ltac context.Gravatar Arnaud Spiwack2014-09-05
* Fix parsing of "subterm(s)" strategy argument.Gravatar Matthieu Sozeau2014-09-05
* Adding a Ftactic module for potentially focussing tactics.Gravatar Pierre-Marie Pédrot2014-09-05
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Reimplementing the clearbody tactic.Gravatar Pierre-Marie Pédrot2014-09-04
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
* Typing.sort_of does not leak evarmaps anymore.Gravatar Pierre-Marie Pédrot2014-09-04
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
* Using goal-tactics to interpret arguments to idtac.Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tacinterp: [interp_message] and associate now only require an environ...Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Ltac's idtac is now implemented using the new API."Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."Gravatar Pierre-Marie Pédrot2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Putting back normalized goals when entering them.Gravatar Pierre-Marie Pédrot2014-09-03
* Yes another remaining clearing bug with 'apply in'.Gravatar Hugo Herbelin2014-09-03
* Fixing bug #2818.Gravatar Pierre-Marie Pédrot2014-09-03
* Useless hooks in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
* Code simplification in Tacenv.Gravatar Pierre-Marie Pédrot2014-09-03
* Code factorization in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
* Another fix than 19a7a5789c to avoid descend_in_conjunction to useGravatar Hugo Herbelin2014-09-02
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
* Code cleaning in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-01
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
* Moving code of tactic interpretation from Tacenv to Vernacentries.Gravatar Pierre-Marie Pédrot2014-08-31
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 10:31:44 +0000