diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 2e344b2178..6ac1591bbd 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -70,8 +70,8 @@ val hnf_prod_applist : env -> types -> constr list -> types (************************************************************************) (*s Recognizing products and arities modulo reduction *) -val dest_prod : env -> types -> Sign.rel_context * types -val dest_prod_assum : env -> types -> Sign.rel_context * types +val dest_prod : env -> types -> rel_context * types +val dest_prod_assum : env -> types -> rel_context * types -val dest_arity : env -> types -> Sign.arity +val dest_arity : env -> types -> arity val is_arity : env -> types -> bool |