aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml
Commit message (Expand)AuthorAge
...
* 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
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Refine patch for behavior of unify_to_subterm to allow backtracking onGravatar Matthieu Sozeau2014-08-18
* Remove confusing behavior of unify_with_subterm that could fail withGravatar Matthieu Sozeau2014-08-14
* Redo PMP's patch to rewriting to make it purely functional using state passing.Gravatar Matthieu Sozeau2014-07-14
* check_for_interrupt: better (but slower) in threading modeGravatar Enrico Tassi2014-07-10
* In setoid_rewrite, force resolution of the contraints generated by rewriting ...Gravatar Matthieu Sozeau2014-07-02
* Add an init_setoid check in rewrite to avoid trying to get undefined references.Gravatar Matthieu Sozeau2014-06-27
* In rewrite, wrong computation of the sort of the term to be rewritten inGravatar Matthieu Sozeau2014-06-25
* Fix semantics of change p with c to typecheck c at each specific occurrence o...Gravatar Matthieu Sozeau2014-06-23
* Allow more relaxed conversion between the types of the two terms of a rewriteGravatar Matthieu Sozeau2014-06-20
* - Fix bug in unification, not only named metas are turned into evars (e.g. in...Gravatar Matthieu Sozeau2014-06-19
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Fix bug #3291, stack overflow in rewrite.Gravatar Matthieu Sozeau2014-06-11
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* In generalized rewrite, avoid retyping completely and constantly the conclusi...Gravatar Matthieu Sozeau2014-06-11
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Gravatar Hugo Herbelin2014-05-31
* Removing a tclSENSITIVE from rewrite.Gravatar Pierre-Marie Pédrot2014-05-27
* Update and start testing rewrite-in-type code.Gravatar Matthieu Sozeau2014-05-09
* Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Gravatar Hugo Herbelin2014-05-08
* Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Gravatar Hugo Herbelin2014-05-08
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06