aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.Gravatar Matthieu Sozeau2014-09-27
* Make pattern_of_constr typed so that we can infer the proper patternsGravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Changed semantics of induction !id when a clause is given: don'tGravatar Hugo Herbelin2014-09-27
* Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Gravatar Pierre-Marie Pédrot2014-09-27
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
* Make eq_pattern_test/eq_test work up to the equivalence of primitiveGravatar Matthieu Sozeau2014-09-24
* 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
* ATBR can't compile without the fix, as it uses setoid_rewrite to rewriteGravatar Matthieu Sozeau2014-09-23
* Fix bug in setoid_rewrite introduced by PMP's commits, which was creatingGravatar Matthieu Sozeau2014-09-23
* Rewrite.apply_lemma is written in state passing style.Gravatar Pierre-Marie Pédrot2014-09-21
* More invariants in the code of Refine.Gravatar Pierre-Marie Pédrot2014-09-21
* Removing a nonsensical Errors.push.Gravatar Pierre-Marie Pédrot2014-09-21
* Fixing strange evarmap leak in goals.Gravatar Pierre-Marie Pédrot2014-09-18
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Fix bug #3633 properly, by delaying the interpetation of constrs inGravatar Matthieu Sozeau2014-09-17
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Gravatar Arnaud Spiwack2014-09-15
* Ltac names in binders: some Ltac values can be seen both as terms and identif...Gravatar Arnaud Spiwack2014-09-15
* A small pass of code cleaning and clenv removing in Rewrite.Gravatar Pierre-Marie Pédrot2014-09-15
* Avoid backtracking in typeclass search if a solution for a closedGravatar Matthieu Sozeau2014-09-15
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* Removing one Evd.merge in Rewrite.Gravatar Pierre-Marie Pédrot2014-09-15
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 02:45:45 +0000