diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-29 19:00:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-29 19:00:41 +0000 |
| commit | 75afe9058afc2dca20472c1f8ed07c901b831bd3 (patch) | |
| tree | 90d6b21ea27e406ff7b0660a86dbe0c380de8b6c /toplevel/coqtop.ml | |
| parent | d02173f7f55ec5b719940a89103c39e017313f5a (diff) | |
New pass on inductive schemes
- Made "is defined" message quiet when a tactic define (via find_scheme)
a scheme for internal use (in ind_tables.ml)
- Improved documentation of eqschemes.ml (and swiched l2r/r2l terminology
when talking about rewriting in hypotheses)
- Took benefit of the new support for commutative cuts in the fixpoint guard
checker for reducing the collection of rewriting schemes needed to
implement the various kinds of rewriting (dependent or not, with
symmetrical equality or not, in hypotheses or in conclusion, from
left-to-right or from right-to-left)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13038 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/coqtop.ml')
0 files changed, 0 insertions, 0 deletions