diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index f7a8d88c2..35daff7b5 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -7,7 +7,6 @@ (************************************************************************) open Term -open Context open Environ (*********************************************************************** @@ -99,9 +98,9 @@ val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) -val dest_prod : env -> types -> rel_context * types -val dest_prod_assum : env -> types -> rel_context * types -val dest_lam_assum : env -> types -> rel_context * types +val dest_prod : env -> types -> Context.Rel.t * types +val dest_prod_assum : env -> types -> Context.Rel.t * types +val dest_lam_assum : env -> types -> Context.Rel.t * types exception NotArity |