diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 15:50:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | b36adb2124d3ba8a5547605e7f89bb0835d0ab10 (patch) | |
| tree | 4ab6481d8d182f6bb3dd241b7112a3027aa26b2a /pretyping/inductiveops.ml | |
| parent | ffb59901f568351401f2f3d1f3334031658b8880 (diff) | |
Removing some return type compatibility layers in Termops.
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 120adb9fe..1dcd6399e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -443,7 +443,7 @@ let build_branch_type env dep p cs = (applist (base,[build_dependent_constructor cs])) cs.cs_args else - it_mkProd_or_LetIn base cs.cs_args + Term.it_mkProd_or_LetIn base cs.cs_args (**************************************************) @@ -575,7 +575,7 @@ let arity_of_case_predicate env (ind,params) dep k = let arsign,_ = get_arity env (ind,params) in let mind = build_dependent_inductive env (ind,params) in let concl = if dep then mkArrow mind (mkSort k) else mkSort k in - it_mkProd_or_LetIn concl arsign + Term.it_mkProd_or_LetIn concl arsign (***********************************************) (* Inferring the sort of parameters of a polymorphic inductive type |