Use evd_combX in Cases.

3 files changed, 37 insertions, 41 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 52610f6f3..2b202ef3e 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -436,7 +436,7 @@ let new_pure_evar_full evd evi =
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ =
   let default_naming = Misctypes.IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
@@ -463,14 +463,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
   in
   (evd, newevk)
 
-let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
+let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance =
   let open EConstr in
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
   let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
-let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
   let instance =
     match filter with
@@ -480,7 +480,7 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ =
+let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ =
   let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
   let map c = csubst_subst subst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
@@ -490,7 +490,7 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnami
     | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
 
-let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid =
+let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
   let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in
   evd', (e, s)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c24660f5b..7dd98bac9 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -25,10 +25,11 @@ val mk_new_meta : unit -> constr
 (** {6 Creating a fresh evar given their type and context} *)
 
 val new_evar_from_context :
-  named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * EConstr.t
+  ?principal:bool ->
+  named_context_val -> evar_map  -> types -> evar_map * EConstr.t
 
 type naming_mode =
   | KeepUserNameAndRenameExistingButSectionNames
@@ -37,25 +38,28 @@ type naming_mode =
   | FailIfConflict
 
 val new_evar :
-  env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> ?hypnaming:naming_mode -> types -> evar_map * EConstr.t
+  ?principal:bool -> ?hypnaming:naming_mode ->
+  env -> evar_map -> types -> evar_map * EConstr.t
 
 val new_pure_evar :
-  named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * Evar.t
+  ?principal:bool ->
+  named_context_val -> evar_map -> types -> evar_map * Evar.t
 
 val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> ?hypnaming:naming_mode -> rigid ->
+  ?principal:bool -> ?hypnaming:naming_mode ->
+  env -> evar_map -> rigid ->
   evar_map * (constr * Sorts.t)
 
 val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
@@ -74,10 +78,10 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> 
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
+ named_context_val -> evar_map -> types ->
   constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 84f0aba8c..ee7c39982 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -295,9 +295,11 @@ let inductive_template evdref env tmloc ind =
         | LocalAssum (na,ty) ->
             let ty = EConstr.of_constr ty in
 	    let ty' = substl subst ty in
-            let evd, e = Evarutil.new_evar env !evdref ~src:(hole_source n) ty' in
-            evdref := evd;
-	    (e::subst,e::evarl,n+1)
+            let e = evd_comb1
+                (Evarutil.new_evar env ~src:(hole_source n))
+                evdref ty'
+            in
+            (e::subst,e::evarl,n+1)
 	| LocalDef (na,b,ty) ->
             let b = EConstr.of_constr b in
 	    (substl subst b::subst,evarl,n+1))
@@ -375,8 +377,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) =
   let loc = loc_of_glob_constr tomatch in
   let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
   let j = typing_fun tycon env evdref !lvar tomatch in
-  let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in
-  evdref := evd;
+  let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in
   let typ = nf_evar !evdref j.uj_type in
   lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar;
   let t =
@@ -399,15 +400,9 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl =
 (* Utils *)
 
 let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref =
-  let evd, (e, u) = new_type_evar env !evdref univ_flexible_alg ~src:src in
-  evdref := evd;
+  let (e, u) = evd_comb1 (new_type_evar env  ~src:src) evdref univ_flexible_alg in
   e
 
-let evd_comb2 f evdref x y =
-  let (evd',y) = f !evdref x y in
-  evdref := evd';
-  y
-
 let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
   (* Ideally, we could find a common inductive type to which both the
      term to match and the patterns coerce *)
@@ -1019,8 +1014,8 @@ let adjust_impossible_cases pb pred tomatch submat =
     begin match Constr.kind pred with
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase ->
         if not (Evd.is_defined !(pb.evdref) evk) then begin
-	  let evd, default = use_unit_judge !(pb.evdref) in
-          pb.evdref := Evd.define evk default.uj_type evd
+          let default = evd_comb0 use_unit_judge pb.evdref in
+          pb.evdref := Evd.define evk default.uj_type !(pb.evdref)
         end;
         add_assert_false_case pb tomatch
     | _ ->
@@ -1686,8 +1681,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
-        let evd, ev' = Evarutil.new_evar env !evdref ~src ty in
-        evdref := evd;
+        let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in
         begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
@@ -1718,8 +1712,7 @@ 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 evd, ev = Evarutil.new_evar extenv !evdref ~src ~filter ~candidates ty in
-      evdref := evd;
+      let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in
       lift k ev
   in
   aux (0,extenv,subst0) t0
@@ -1731,14 +1724,15 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
            we are in an impossible branch *)
 	let n = Context.Rel.length (rel_context env) in
 	let n' = Context.Rel.length (rel_context tycon_env) in
-        let evd, (impossible_case_type, u) =
-          new_type_evar (reset_context env) !evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in
-        evdref := evd;
-	(lift (n'-n) impossible_case_type, mkSort u)
+        let impossible_case_type, u =
+          evd_comb1
+            (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase))
+            evdref univ_flexible_alg
+        in
+        (lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in
-        let evd,tt = Typing.type_of extenv !evdref t in
-        evdref := evd;
+        let tt = evd_comb1 (Typing.type_of extenv) evdref t in
         (t,tt) in
   match cumul env !evdref tt (mkSort s) with
   | None -> anomaly (Pp.str "Build_tycon: should be a type.");
@@ -1932,9 +1926,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
 let inh_conv_coerce_to_tycon ?loc env evdref j tycon =
   match tycon with
     | Some p ->
-	let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in
-          evdref := evd';
-          j
+      evd_comb2 (Coercion.inh_conv_coerce_to ?loc true env) evdref j p
     | None -> j
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)