From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 15:50:17 +0100
Subject: Removing some return type compatibility layers in Termops.

---
 pretyping/inductiveops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 120adb9fef..1dcd6399e7 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
-- 
cgit v1.2.3