aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* More invariants in Rewrite unification.Gravatar Pierre-Marie Pédrot2014-09-15
* The unifying functions of Rewrite uses the return types of strategies.Gravatar Pierre-Marie Pédrot2014-09-15
* Splitting the uses of the unification function according to the status ofGravatar Pierre-Marie Pédrot2014-09-15
* Rewrite.apply_strategy uses the same return type as strategies.Gravatar Pierre-Marie Pédrot2014-09-14
* Proper type for rewrite strategy results.Gravatar Pierre-Marie Pédrot2014-09-14
* Retroknowledge arguments are made VERNAC ARGUMENTS.Gravatar Pierre-Marie Pédrot2014-09-13
* Fixing injection bug #3616 on sigma-types.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Commit 682aa67cc80 about enforcing that apply does not create newGravatar Hugo Herbelin2014-09-12
* Oopps.. fixed the .ml not the .ml4Gravatar Matthieu Sozeau2014-09-11
* Use an AST for strategy names.Gravatar Matthieu Sozeau2014-09-11
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
* Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...Gravatar Hugo Herbelin2014-09-11
* Other bugs with "inversion as" (collision between user-provided names and gen...Gravatar Hugo Herbelin2014-09-11
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
* More small bugs in intros_replacing.Gravatar Hugo Herbelin2014-09-10
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
* Displaying genarg tag in idtac.Gravatar Pierre-Marie Pédrot2014-09-09
* Removing antiquotations in Tauto.Gravatar Pierre-Marie Pédrot2014-09-08
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:43:21 +0000