diff options
author | 2017-11-13 17:13:44 +0100 | |
---|---|---|
committer | 2017-11-13 17:13:44 +0100 | |
commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /pretyping/inductiveops.ml | |
parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'pretyping/inductiveops.ml')
-rw-r--r-- | pretyping/inductiveops.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b31ee03d8..34df7d3d7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -11,6 +11,7 @@ open Util open Names open Univ open Term +open Constr open Vars open Termops open Declarations @@ -643,7 +644,7 @@ let type_of_projection_knowing_arg env sigma p c ty = syntactic conditions *) let control_only_guard env c = - let check_fix_cofix e c = match kind_of_term c with + let check_fix_cofix e c = match kind c with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix | Fix (_,(_,_,_) as fix) -> @@ -659,7 +660,7 @@ let control_only_guard env c = (* inference of subtyping condition for inductive types *) let infer_inductive_subtyping_arity_constructor - (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) = + (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) = let numchecked = ref 0 in let numparams = Context.Rel.nhyps params in let update_contexts (env, evd, csts) csts' = |