index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
rewrite.ml
Commit message (
Expand
)
Author
Age
*
In setoid_rewrite error messages:
Hugo Herbelin
2014-11-22
*
Fix resolve_morphism to build well-scoped terms in case some arguments
Matthieu Sozeau
2014-11-22
*
Tentative rephrasing of error message for rewrite.
Hugo Herbelin
2014-11-18
*
Replugging hints in rewriting strategies.
Pierre-Marie Pédrot
2014-11-10
*
Follow up to experimental eager evar unification in bcba6d1bc9:
Hugo Herbelin
2014-11-08
*
Cleaning and documenting Clenv.make_evar_clause
Pierre-Marie Pédrot
2014-10-27
*
Preventing potential evar leak in Rewrite.
Pierre-Marie Pédrot
2014-10-26
*
Change reduction_of_red_expr to return an e_reduction_function returning
Matthieu Sozeau
2014-10-24
*
Proofview: move more functions to the Unsafe module.
Arnaud Spiwack
2014-10-22
*
Proofview: split [V82] module into [Unsafe] and [V82].
Arnaud Spiwack
2014-10-22
*
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.
Arnaud Spiwack
2014-10-22
*
Removing dead code in Rewrite.
Pierre-Marie Pédrot
2014-10-21
*
Small invariants in Rewrite code.
Pierre-Marie Pédrot
2014-10-21
*
Fixing decompose_app_rel in Rewrite.
Pierre-Marie Pédrot
2014-10-21
*
Using new clausenv in rewrite.
Pierre-Marie Pédrot
2014-10-21
*
Proofview.Refine: remove the handle type, and simplify the API.
Arnaud Spiwack
2014-10-16
*
A version of convert_concl and convert_hyp in new proof engine.
Hugo Herbelin
2014-10-09
*
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-10-07
*
Semantic fix of a refine in Rewrite.
Pierre-Marie Pédrot
2014-10-05
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
ATBR can't compile without the fix, as it uses setoid_rewrite to rewrite
Matthieu Sozeau
2014-09-23
*
Fix bug in setoid_rewrite introduced by PMP's commits, which was creating
Matthieu Sozeau
2014-09-23
*
Rewrite.apply_lemma is written in state passing style.
Pierre-Marie Pédrot
2014-09-21
*
More invariants in the code of Refine.
Pierre-Marie Pédrot
2014-09-21
*
Removing a nonsensical Errors.push.
Pierre-Marie Pédrot
2014-09-21
*
A small pass of code cleaning and clenv removing in Rewrite.
Pierre-Marie Pédrot
2014-09-15
*
Rework typeclass resolution and control of backtracking.
Matthieu Sozeau
2014-09-15
*
Removing one Evd.merge in Rewrite.
Pierre-Marie Pédrot
2014-09-15
*
More invariants in Rewrite unification.
Pierre-Marie Pédrot
2014-09-15
*
The unifying functions of Rewrite uses the return types of strategies.
Pierre-Marie Pédrot
2014-09-15
*
Splitting the uses of the unification function according to the status of
Pierre-Marie Pédrot
2014-09-15
*
Rewrite.apply_strategy uses the same return type as strategies.
Pierre-Marie Pédrot
2014-09-14
*
Proper type for rewrite strategy results.
Pierre-Marie Pédrot
2014-09-14
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Use an AST for strategy names.
Matthieu Sozeau
2014-09-11
*
A step towards better differentiating when w_unify is used for subterm
Hugo Herbelin
2014-09-10
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Fix parsing of "subterm(s)" strategy argument.
Matthieu Sozeau
2014-09-05
*
Typing.sort_of does not leak evarmaps anymore.
Pierre-Marie Pédrot
2014-09-04
*
Putting back normalized goals when entering them.
Pierre-Marie Pédrot
2014-09-03
*
Protect against "it's unifiable, if you solve some unsolvable constraints" be...
Matthieu Sozeau
2014-08-27
*
Move UnsatisfiableConstraints to a pretype error.
Matthieu Sozeau
2014-08-22
*
Removing a Goal.sensitive in Rewrite.
Pierre-Marie Pédrot
2014-08-21
*
Removing a use of tclSENSITIVE in Rewrite.
Pierre-Marie Pédrot
2014-08-21
*
Removing a use of tclSENSITIVE in Rewrite.
Pierre-Marie Pédrot
2014-08-21
*
Removing a use of tclSENSITIVE in Rewrite.
Pierre-Marie Pédrot
2014-08-21
*
Improving error message when applying rewrite to an expression which is not a...
Hugo Herbelin
2014-08-18
*
Slight simplification of naming of tactics in equality.ml (hopefully).
Hugo Herbelin
2014-08-18
*
A reorganization of the "assert" tactics (hopefully uniform naming
Hugo Herbelin
2014-08-18
[next]