aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml
Commit message (Expand)AuthorAge
* In setoid_rewrite error messages:Gravatar Hugo Herbelin2014-11-22
* Fix resolve_morphism to build well-scoped terms in case some argumentsGravatar Matthieu Sozeau2014-11-22
* Tentative rephrasing of error message for rewrite.Gravatar Hugo Herbelin2014-11-18
* Replugging hints in rewriting strategies.Gravatar Pierre-Marie Pédrot2014-11-10
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Cleaning and documenting Clenv.make_evar_clauseGravatar Pierre-Marie Pédrot2014-10-27
* Preventing potential evar leak in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-26
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Removing dead code in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Small invariants in Rewrite code.Gravatar Pierre-Marie Pédrot2014-10-21
* Fixing decompose_app_rel in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Using new clausenv in rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Semantic fix of a refine in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-05
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* 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
* A small pass of code cleaning and clenv removing in Rewrite.Gravatar Pierre-Marie Pédrot2014-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
* 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
* Use an AST for strategy names.Gravatar Matthieu Sozeau2014-09-11
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Fix parsing of "subterm(s)" strategy argument.Gravatar Matthieu Sozeau2014-09-05
* Typing.sort_of does not leak evarmaps anymore.Gravatar Pierre-Marie Pédrot2014-09-04
* Putting back normalized goals when entering them.Gravatar Pierre-Marie Pédrot2014-09-03
* Protect against "it's unifiable, if you solve some unsolvable constraints" be...Gravatar Matthieu Sozeau2014-08-27
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Removing a Goal.sensitive in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Improving error message when applying rewrite to an expression which is not a...Gravatar Hugo Herbelin2014-08-18
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 12:17:54 +0000