Make the clenv type private and provide a creation function.

5 files changed, 28 insertions, 19 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f47ed0fc4b..23ae9d04c4 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -39,6 +39,13 @@ type clausenv = {
   templval : constr freelisted;
   templtyp : constr freelisted }
 
+let mk_clausenv env evd templval templtyp = {
+  env; evd; templval; templtyp;
+}
+
+let update_clenv_evd clenv evd =
+  mk_clausenv clenv.env evd clenv.templval clenv.templtyp
+
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index a72c8c5e1f..bfdc5cdd8c 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -22,7 +22,7 @@ open Tactypes
 
 (** {6 The Type of Constructions clausale environments.} *)
 
-type clausenv = {
+type clausenv = private {
   env      : env; (** the typing context *)
   evd      : evar_map; (** the mapping from metavar and evar numbers to their
                            types and values *)
@@ -30,6 +30,8 @@ type clausenv = {
                                     out *)
   templtyp : constr freelisted (** its type *)}
 
+val mk_clausenv : env -> evar_map -> constr freelisted -> types freelisted -> clausenv
+val update_clenv_evd : clausenv -> evar_map -> clausenv
 
 (** subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fcdd23a9c1..633b9da053 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -154,7 +154,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let c1 = args.(arglen - 2) in
   let c2 = args.(arglen - 1) in
   let try_occ (evd', c') =
-    Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
+    let clenv = Clenv.update_clenv_evd eqclause evd' in
+    Clenv.clenv_pose_dependent_evars ~with_evars:true clenv
   in
   let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
   let occs =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 6fab111e6f..ace51c40d4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -340,10 +340,8 @@ let instantiate_hint env sigma p =
   let mk_clenv (c, cty, ctx) =
     let sigma = merge_context_set_opt sigma ctx in
     let cl = mk_clenv_from_env env sigma None (c,cty) in
-    let cl = {cl with templval =
-          { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
-        env = empty_env}
-    in
+    let templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus } in
+    let cl = mk_clausenv empty_env cl.evd templval cl.templtyp in
     { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
   in
   let code = match p.code.obj with
@@ -1649,14 +1647,17 @@ let connect_hint_clenv h gl =
     let emap c = Vars.subst_univs_level_constr subst c in
     let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
     (* Only metas are mentioning the old universes. *)
-    {
-      templval = Evd.map_fl emap clenv.templval;
-      templtyp = Evd.map_fl emap clenv.templtyp;
-      evd = Evd.map_metas emap evd;
-      env = Proofview.Goal.env gl;
-    }
+    Clenv.mk_clausenv
+      (Proofview.Goal.env gl)
+      (Evd.map_metas emap evd)
+      (Evd.map_fl emap clenv.templval)
+      (Evd.map_fl emap clenv.templtyp)
   | None ->
-    { clenv with evd = evd ; env = Proofview.Goal.env gl }
+    Clenv.mk_clausenv
+      (Proofview.Goal.env gl)
+      evd
+      clenv.templval
+      clenv.templtyp
 
 let fresh_hint env sigma h =
   let { hint_term = c; hint_uctx = ctx } = h in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 528fa65d5a..4a86d8d690 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1362,20 +1362,18 @@ let do_replace id = function
 
 let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
   let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in
-  let clenv =
-      { clenv with evd = Typeclasses.resolve_typeclasses
-          ~fail:(not with_evars) clenv.env clenv.evd }
-  in
+  let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in
+  let clenv = Clenv.update_clenv_evd clenv evd in
   let new_hyp_typ = clenv_type clenv in
   if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
-  if not with_evars && occur_meta clenv.evd new_hyp_typ then
+  if not with_evars && occur_meta evd new_hyp_typ then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
   let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
   let naming = NamingMustBe (CAst.make targetid) in
   let with_clear = do_replace (Some id) naming in
   Tacticals.New.tclTHEN
-    (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
+    (Proofview.Unsafe.tclEVARS (clear_metas evd))
     (Tacticals.New.tclTHENLAST
       (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac)