diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-24 13:39:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-24 13:39:23 +0000 |
| commit | 3afaf3dde673d77cacaabc354f008dfbe49a7cee (patch) | |
| tree | 4264164faf763ab8d18274cd5aeffe5a1de21728 /kernel/reduction.mli | |
| parent | 83f038e61a4424fcf71aada9f97c91165b73aef8 (diff) | |
Passage à des contextes de vars et de rels pouvant contenir des déclarations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index fb623595a..bab5f446f 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -97,7 +97,7 @@ val splay_prod : env -> 'a evar_map -> constr -> (name * constr) list * constr val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts val sort_of_arity : env -> constr -> sorts val decomp_n_prod : - env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr + env -> 'a evar_map -> int -> constr -> Sign.rel_context * constr type 'a miota_args = { mP : constr; (* the result type *) @@ -130,7 +130,7 @@ val fold_commands : constr list -> 'a reduction_function val pattern_occs : (int list * constr * constr) list -> 'a reduction_function val compute : 'a reduction_function -val fix_recarg : constr -> 'a list -> (int * 'a) option +val fix_recarg : fixpoint -> 'a list -> (int * 'a) option val reduce_fix : (constr -> 'a list -> constr * constr list) -> constr -> constr list -> bool * (constr * constr list) |