Remove understand_tcc_evars.

Use the functional interface understand_tcc instead.

4 files changed, 16 insertions, 15 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c9fc3aa4f..e465677cd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2038,7 +2038,9 @@ let interp_constr_evars_gen_impls env evdref
     ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
-    understand_tcc_evars env evdref ~expected_type c, imps
+  let evd, c = understand_tcc env !evdref ~expected_type c in
+  evdref := evd;
+  c, imps
 
 let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c
@@ -2053,7 +2055,9 @@ let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c =
 
 let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env c in
-  understand_tcc_evars env evdref ~expected_type c
+  let evd, c = understand_tcc env !evdref ~expected_type c in
+  evdref := evd;
+  c
 
 let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
@@ -2098,7 +2102,9 @@ let interp_binder env sigma na t =
 let interp_binder_evars env evdref na t =
   let t = intern_gen IsType env t in
   let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in
-  understand_tcc_evars env evdref ~expected_type:IsType t'
+  let evd, c = understand_tcc env !evdref ~expected_type:IsType t' in
+  evdref := evd;
+  c
 
 let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
@@ -2125,7 +2131,8 @@ let interp_glob_context_evars env evdref k bl =
 	 if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
 	 else t
        in
-       let t = understand_tcc_evars env evdref ~expected_type:IsType t' in
+       let (evd,t) = understand_tcc env !evdref ~expected_type:IsType t' in
+       evdref := evd;
 	match b with
 	    None ->
 	      let d = LocalAssum (na,t) in
@@ -2137,7 +2144,8 @@ let interp_glob_context_evars env evdref k bl =
 	      in
 		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
-	      let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in
+	      let (evd,c) = understand_tcc env !evdref ~expected_type:(OfType t) b in
+              evdref := evd;
 	      let d = LocalDef (na, c, t) in
 		(push_rel d env, d::params, n, impls))
       (env,[],k+1,[]) (List.rev bl)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7362b57fe..40b8bcad9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1194,11 +1194,6 @@ let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutT
   let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in
   (sigma, c)
 
-let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c =
-  let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in
-  evdref := sigma;
-  c
-
 let understand_ltac flags env sigma lvar kind c =
   let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index aa25e3604..7395e94a0 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -55,9 +55,6 @@ val all_and_fail_flags : inference_flags
 val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
   ?expected_type:typing_constraint -> glob_constr -> evar_map * constr
 
-val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
-  ?expected_type:typing_constraint -> glob_constr -> constr
-
 (** More general entry point with evars from ltac *)
 
 (** Generic call to the interpreter from glob_constr to constr
diff --git a/vernac/command.ml b/vernac/command.ml
index e04bebe33..a315ac14e 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -393,8 +393,9 @@ let is_impredicative env u =
 
 let interp_ind_arity env evdref ind =
   let c = intern_gen IsType env ind.ind_arity in
-  let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
-  let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in
+  let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
+  let (evd,t) = understand_tcc env !evdref ~expected_type:IsType c in
+  evdref := evd;
   let pseudo_poly = check_anonymous_type c in
   let () = if not (Reductionops.is_arity env !evdref t) then
     user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")