[pretyper] Less imperative passing of the evar_map, part I.

This builds on the work on #8545.

2 files changed, 45 insertions, 49 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1b7f32bcae..04bfb5acaf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -231,24 +231,26 @@ let frozen_and_pending_holes (sigma, sigma') =
     end in
     FrozenProgress data
 
-let apply_typeclasses env evdref frozen fail_evar =
+let apply_typeclasses env sigma frozen fail_evar =
   let filter_frozen = match frozen with
-  | FrozenId map -> fun evk -> Evar.Map.mem evk map
-  | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
+    | FrozenId map -> fun evk -> Evar.Map.mem evk map
+    | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
   in
-  evdref := Typeclasses.resolve_typeclasses
-     ~filter:(if Flags.is_program_mode () 
-	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
-              else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk)))
-     ~split:true ~fail:fail_evar env !evdref;
-  if Flags.is_program_mode () then (* Try optionally solving the obligations *)
-    evdref := Typeclasses.resolve_typeclasses
-      ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref
-
-let apply_inference_hook hook evdref frozen = match frozen with
-| FrozenId _ -> ()
+  let sigma = Typeclasses.resolve_typeclasses
+      ~filter:(if Flags.is_program_mode ()
+               then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
+               else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk)))
+      ~split:true ~fail:fail_evar env sigma in
+  let sigma = if Flags.is_program_mode () then (* Try optionally solving the obligations *)
+      Typeclasses.resolve_typeclasses
+        ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env sigma
+    else sigma in
+  sigma
+
+let apply_inference_hook hook sigma frozen = match frozen with
+| FrozenId _ -> sigma
 | FrozenProgress (lazy (_, pending)) ->
-  evdref := Evar.Set.fold (fun evk sigma ->
+  Evar.Set.fold (fun evk sigma ->
     if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
       try
@@ -257,18 +259,19 @@ let apply_inference_hook hook evdref frozen = match frozen with
       with Exit ->
         sigma
     else
-      sigma) pending !evdref
+      sigma) pending sigma
 
-let apply_heuristics env evdref fail_evar =
+let apply_heuristics env sigma fail_evar =
   (* Resolve eagerly, potentially making wrong choices *)
-  try evdref := solve_unif_constraints_with_heuristics
-	~ts:(Typeclasses.classes_transparent_state ()) env !evdref
+  try solve_unif_constraints_with_heuristics
+        ~ts:(Typeclasses.classes_transparent_state ()) env sigma
   with e when CErrors.noncritical e ->
-    let e = CErrors.push e in if fail_evar then iraise e
+    let e = CErrors.push e in
+    if fail_evar then iraise e else sigma
 
 let check_typeclasses_instances_are_solved env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
-  apply_typeclasses env (ref current_sigma) frozen true
+  apply_typeclasses env current_sigma frozen true
 
 let check_extra_evars_are_solved env current_sigma frozen = match frozen with
 | FrozenId _ -> ()
@@ -297,22 +300,30 @@ let check_evars env initial_sigma sigma c =
     | _ -> EConstr.iter sigma proc_rec c
   in proc_rec c
 
-let check_evars_are_solved env current_sigma frozen =
-  check_typeclasses_instances_are_solved env current_sigma frozen;
-  check_problems_are_solved env current_sigma;
-  check_extra_evars_are_solved env current_sigma frozen
+let check_evars_are_solved env sigma frozen =
+  let sigma = check_typeclasses_instances_are_solved env sigma frozen in
+  check_problems_are_solved env sigma;
+  check_extra_evars_are_solved env sigma frozen
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
-let solve_remaining_evars flags env current_sigma init_sigma =
-  let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
-  let evdref = ref current_sigma in
-  if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
-  if Option.has_some flags.use_hook then
-    apply_inference_hook (Option.get flags.use_hook env) evdref frozen;
-  if flags.solve_unification_constraints then apply_heuristics env evdref false;
-  if flags.fail_evar then check_evars_are_solved env !evdref frozen;
-  !evdref
+let solve_remaining_evars flags env sigma init_sigma =
+  let frozen = frozen_and_pending_holes (init_sigma, sigma) in
+  let sigma =
+    if flags.use_typeclasses
+    then apply_typeclasses env sigma frozen false
+    else sigma
+  in
+  let sigma = if Option.has_some flags.use_hook
+    then apply_inference_hook (Option.get flags.use_hook env) sigma frozen
+    else sigma
+  in
+  let sigma = if flags.solve_unification_constraints
+    then apply_heuristics env sigma false
+    else sigma
+  in
+  if flags.fail_evar then check_evars_are_solved env sigma frozen;
+  sigma
 
 let check_evars_are_solved env current_sigma init_sigma =
   let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
@@ -1113,9 +1124,3 @@ let understand_tcc ?flags env sigma ?expected_type 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)
-
-let pretype k0 resolve_tc typcon env evdref lvar t =
-  pretype k0 resolve_tc typcon (GlobEnv.make env !evdref lvar) evdref t
-
-let pretype_type k0 resolve_tc valcon env evdref lvar t =
-  pretype_type k0 resolve_tc valcon (GlobEnv.make env !evdref lvar) evdref t
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index fcc361b16b..0f95d27528 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -19,7 +19,6 @@ open Evd
 open EConstr
 open Glob_term
 open Ltac_pretype
-open Evardefine
 
 val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
   glob_level -> Univ.Level.t
@@ -111,14 +110,6 @@ val check_evars : env -> evar_map -> evar_map -> constr -> unit
 
 (**/**)
 (** Internal of Pretyping... *)
-val pretype :
-  int -> bool -> type_constraint -> env -> evar_map ref ->
-  ltac_var_map -> glob_constr -> unsafe_judgment
-
-val pretype_type :
-  int -> bool -> val_constraint -> env -> evar_map ref ->
-  ltac_var_map -> glob_constr -> unsafe_type_judgment
-
 val ise_pretype_gen :
   inference_flags -> env -> evar_map ->
   ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types