[econstr] Switch constrintern API to non-imperative style.

We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.

2 files changed, 39 insertions, 45 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c2157bb2e..909eab27e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2094,39 +2094,36 @@ let interp_open_constr env sigma c =
 
 (* Not all evars expected to be resolved and computation of implicit args *)
 
-let interp_constr_evars_gen_impls env evdref
+let interp_constr_evars_gen_impls env sigma
     ?(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
-  let evd, c = understand_tcc env !evdref ~expected_type c in
-  evdref := evd;
-  c, imps
+  let sigma, c = understand_tcc env sigma ~expected_type c in
+  sigma, (c, imps)
 
-let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c
+let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c
 
 let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ =
   interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c
 
-let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls env evdref ~impls IsType c
+let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls env sigma ~impls IsType c
 
 (* Not all evars expected to be resolved, with side-effect on evars *)
 
-let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c =
+let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env c in
-  let evd, c = understand_tcc env !evdref ~expected_type c in
-  evdref := evd;
-  c
+  understand_tcc env sigma ~expected_type c
 
 let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
 
-let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen env evdref ~impls (OfType typ) c
+let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen env sigma ~impls (OfType typ) c
 
-let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen env evdref IsType ~impls c
+let interp_type_evars env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen env sigma IsType ~impls c
 
 (* Miscellaneous *)
 
@@ -2181,17 +2178,16 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
-let interp_glob_context_evars env evdref k bl =
+let interp_glob_context_evars env sigma k bl =
   let open EConstr in
-  let (env, par, _, impls) =
+  let env, sigma, par, _, impls =
     List.fold_left
-      (fun (env,params,n,impls) (na, k, b, t) ->
+      (fun (env,sigma,params,n,impls) (na, k, b, t) ->
        let t' =
 	 if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
 	 else t
        in
-       let (evd,t) = understand_tcc env !evdref ~expected_type:IsType t' in
-       evdref := evd;
+       let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in
 	match b with
 	    None ->
 	      let d = LocalAssum (na,t) in
@@ -2201,16 +2197,15 @@ let interp_glob_context_evars env evdref k bl =
 		    (ExplByPos (n, na), (true, true, true)) :: impls
 		else impls
 	      in
-		(push_rel d env, d::params, succ n, impls)
+                (push_rel d env, sigma, d::params, succ n, impls)
 	  | Some b ->
-	      let (evd,c) = understand_tcc env !evdref ~expected_type:(OfType t) b in
-              evdref := evd;
+              let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in
 	      let d = LocalDef (na, c, t) in
-		(push_rel d env, d::params, n, impls))
-      (env,[],k+1,[]) (List.rev bl)
-  in (env, par), impls
+                (push_rel d env, sigma, d::params, n, impls))
+      (env,sigma,[],k+1,[]) (List.rev bl)
+  in sigma, ((env, par), impls)
 
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let x = interp_glob_context_evars env evdref shift bl in
-  int_env, x
+  let sigma, x = interp_glob_context_evars env sigma shift bl in
+  sigma, (int_env, x)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index af4e4a9c5..632b423b0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -112,29 +112,28 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.co
 
 (** Accepting unresolved evars *)
 
-val interp_constr_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> EConstr.constr
+val interp_constr_evars : env -> evar_map ->
+  ?impls:internalization_env -> constr_expr -> evar_map * EConstr.constr
 
+val interp_casted_constr_evars : env -> evar_map ->
+  ?impls:internalization_env -> constr_expr -> EConstr.types -> evar_map * EConstr.constr
 
-val interp_casted_constr_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> EConstr.types -> EConstr.constr
-
-val interp_type_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> EConstr.types
+val interp_type_evars : env -> evar_map ->
+  ?impls:internalization_env -> constr_expr -> evar_map * EConstr.types
 
 (** Accepting unresolved evars and giving back the manual implicit arguments *)
 
-val interp_constr_evars_impls : env -> evar_map ref ->
+val interp_constr_evars_impls : env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
-  EConstr.constr * Impargs.manual_implicits
+  evar_map * (EConstr.constr * Impargs.manual_implicits)
 
-val interp_casted_constr_evars_impls : env -> evar_map ref ->
+val interp_casted_constr_evars_impls : env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> EConstr.types ->
-  EConstr.constr * Impargs.manual_implicits
+  evar_map * (EConstr.constr * Impargs.manual_implicits)
 
-val interp_type_evars_impls : env -> evar_map ref ->
+val interp_type_evars_impls : env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
-  EConstr.types * Impargs.manual_implicits
+  evar_map * (EConstr.types * Impargs.manual_implicits)
 
 (** Interprets constr patterns *)
 
@@ -159,8 +158,8 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst
 
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
-  env -> evar_map ref -> local_binder_expr list ->
-  internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)
+  env -> evar_map -> local_binder_expr list ->
+  evar_map * (internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits))
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)