diff options
| author | herbelin | 2010-05-29 19:00:41 +0000 |
|---|---|---|
| committer | herbelin | 2010-05-29 19:00:41 +0000 |
| commit | 75afe9058afc2dca20472c1f8ed07c901b831bd3 (patch) | |
| tree | 90d6b21ea27e406ff7b0660a86dbe0c380de8b6c /toplevel | |
| 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')
| -rw-r--r-- | toplevel/ind_tables.ml | 2 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 845a5697a0..8e3d9437f8 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -118,7 +118,7 @@ let define internal id c = const_entry_opaque = false; const_entry_boxed = Flags.boxed_definitions() }, Decl_kinds.IsDefinition Scheme) in - definition_message id; + if not internal then definition_message id; kn let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index a5d15a28ab..a02b01351f 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -245,14 +245,14 @@ let declare_rewriting_schemes ind = if Hipattern.is_inductive_equality ind then begin ignore (define_individual_scheme rew_r2l_scheme_kind true None ind); ignore (define_individual_scheme rew_r2l_dep_scheme_kind true None ind); - ignore (define_individual_scheme rew_l2r_forward_dep_scheme_kind true None ind); + ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind true None ind); (* These ones expect the equality to be symmetric; the first one also *) (* needs eq *) ignore_error (define_individual_scheme rew_l2r_scheme_kind true None) ind; ignore_error (define_individual_scheme rew_l2r_dep_scheme_kind true None) ind; ignore_error - (define_individual_scheme rew_r2l_forward_dep_scheme_kind true None) ind + (define_individual_scheme rew_l2r_forward_dep_scheme_kind true None) ind end let declare_congr_scheme ind = |