Removing some return type compatibility layers in Termops.

7 files changed, 15 insertions, 14 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c0141f0116..01e2db08cb 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1690,7 +1690,6 @@ let abstract_tycon loc env evdref subst tycon extenv t =
 	  (named_context extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = u :: List.map mkRel vl in
-      let candidates = List.map EConstr.Unsafe.to_constr candidates in
       let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in
       lift k ev
   in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 87561868f7..3d5a5f0259 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -210,16 +210,18 @@ let computable p k =
   &&
   noccur_between 1 (k+1) ccl
 
+let pop t = Vars.lift (-1) t
+
 let lookup_name_as_displayed env t s =
   let rec lookup avoid n c = match kind_of_term c with
     | Prod (name,_,c') ->
 	(match compute_displayed_name_in RenamingForGoal avoid name c' with
            | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
-	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop (EConstr.of_constr c')))
+	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | LetIn (name,_,_,c') ->
 	(match compute_displayed_name_in RenamingForGoal avoid name c' with
            | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
-	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop (EConstr.of_constr c')))
+	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | Cast (c,_,_) -> lookup avoid n c
     | _ -> None
   in lookup (ids_of_named_context (named_context env)) 1 t
@@ -439,7 +441,7 @@ let detype_instance sigma l =
   else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
 
 let rec detype flags avoid env sigma t =
-  match kind_of_term (collapse_appl sigma (EConstr.of_constr t)) with
+  match kind_of_term (EConstr.Unsafe.to_constr (collapse_appl sigma (EConstr.of_constr t))) with
     | Rel n ->
       (try match lookup_name_of_rel n (fst env) with
 	 | Name id   -> GVar (dl, id)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9675ae2ea9..6dce8627da 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -147,7 +147,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
 	  let _, a, b = destProd sigma t2 in
           if noccurn sigma 1 b then
             lookup_canonical_conversion (proji, Prod_cs),
-	    (Stack.append_app [|a;EConstr.of_constr (pop b)|] Stack.empty)
+	    (Stack.append_app [|a;pop b|] Stack.empty)
           else raise Not_found
       | Sort s ->
 	lookup_canonical_conversion
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 27436fdd8b..3003620d7e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -189,8 +189,8 @@ let restrict_evar_key evd evk filter candidates =
       | None -> evar_filter evi
       | Some filter -> filter in
       let candidates = match candidates with
-      | NoUpdate -> evi.evar_candidates
-      | UpdateWith c -> Some (List.map EConstr.Unsafe.to_constr c) in
+      | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates
+      | UpdateWith c -> Some c in
       let sigma = Sigma.Unsafe.of_evar_map evd in
       let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in
       (Sigma.to_evar_map sigma, evk)
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
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 8ec6083f71..caa5a5c8a6 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -31,7 +31,7 @@ let init_reference dir s () = coq_reference "Program" dir s
 let papp evdref r args = 
   let open EConstr in
   let gr = delayed_force r in
-    mkApp (EConstr.of_constr (Evarutil.e_new_global evdref gr), args)
+    mkApp (Evarutil.e_new_global evdref gr, args)
 
 let sig_typ = init_reference ["Init"; "Specif"] "sig"
 let sig_intro = init_reference ["Init"; "Specif"] "exist"
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index c796a91caa..90c5b241b8 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -203,10 +203,10 @@ module Cst_stack = struct
     let reconstruct_head = List.fold_left
       (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
     List.fold_right
-      (fun (cst,params,args) t -> EConstr.of_constr (Termops.replace_term sigma
+      (fun (cst,params,args) t -> Termops.replace_term sigma
 	(reconstruct_head d args)
 	(applist (cst, List.rev params))
-	t)) cst_l c
+	t) cst_l c
 
   let pr l =
     let open Pp in
@@ -969,7 +969,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else mkApp (f,lc) in
-	      if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold ()
+	      if noccurn sigma 1 u then (pop u,Stack.empty),Cst_stack.empty else fold ()
             | _ -> fold ()
 	  else fold ()
 	| _ -> fold ())
@@ -1068,7 +1068,7 @@ let local_whd_state_gen flags sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else mkApp (f,lc) in
-	      if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s
+	      if noccurn sigma 1 u then (pop u,Stack.empty) else s
             | _ -> s
 	  else s
 	| _ -> s)