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 /tactics/eqschemes.mli | |
| 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 'tactics/eqschemes.mli')
| -rw-r--r-- | tactics/eqschemes.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 8c649aecf..3d0ea4790 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -17,18 +17,17 @@ open Ind_tables val rew_l2r_dep_scheme_kind : individual scheme_kind val rew_l2r_scheme_kind : individual scheme_kind -val rew_l2r_forward_dep_scheme_kind : individual scheme_kind val rew_r2l_forward_dep_scheme_kind : individual scheme_kind +val rew_l2r_forward_dep_scheme_kind : individual scheme_kind val rew_r2l_dep_scheme_kind : individual scheme_kind val rew_r2l_scheme_kind : individual scheme_kind -val rew_asym_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> constr -val build_l2r_forward_rew_scheme : - bool -> env -> inductive -> sorts_family -> constr val build_r2l_forward_rew_scheme : bool -> env -> inductive -> sorts_family -> constr +val build_l2r_forward_rew_scheme : + bool -> env -> inductive -> sorts_family -> constr (** Builds a symmetry scheme for a symmetrical equality type *) |