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