Merge PR #7827: [engine] safe [add_unification_pb] interface

5 files changed, 31 insertions, 3 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 82be4791f..1625f6fc8 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -514,6 +514,21 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami
   evdref := evd';
   ev
 
+(* Safe interface to unification problems *)
+type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr
+
+let eq_unification_pb evd (pbty,env,t1,t2) (pbty',env',t1',t2') =
+  pbty == pbty' && env == env' &&
+    EConstr.eq_constr evd t1 t1' &&
+    EConstr.eq_constr evd t2 t2'
+
+let add_unification_pb ?(tail=false) pb evd =
+  let conv_pbs = Evd.conv_pbs evd in
+  if not (List.exists (eq_unification_pb evd pb) conv_pbs) then
+    let (pbty,env,t1,t2) = pb in
+    Evd.add_conv_pb ~tail (pbty,env,t1,t2) evd
+  else evd
+
 (* This assumes an evar with identity instance and generalizes it over only
    the de Bruijn part of the context *)
 let generalize_evar_over_rels sigma (ev,args) =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c17f3d168..db638be9e 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -217,6 +217,14 @@ val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array ->
 val compare_constructor_instances : evar_map ->
   Univ.Instance.t -> Univ.Instance.t -> evar_map
 
+(** {6 Unification problems} *)
+type unification_pb = conv_pb * env * constr * constr
+
+(** [add_unification_pb ?tail pb sigma]
+    Add a unification problem [pb] to [sigma], if not already present.
+    Put it at the end of the list if [tail] is true, by default it is false. *)
+val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map
+
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
diff --git a/engine/evd.ml b/engine/evd.ml
index f56f9662d..714a0b645 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -621,10 +621,11 @@ let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
 let add_conv_pb ?(tail=false) pb d =
-  (** MS: we have duplicates here, why? *)
   if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
   else {d with conv_pbs = pb::d.conv_pbs}
 
+let conv_pbs d = d.conv_pbs
+
 let evar_source evk d = (find d evk).evar_source
 
 let evar_ident evk evd = EvNames.ident evk evd.evar_names
diff --git a/engine/evd.mli b/engine/evd.mli
index 405fcc403..d166fd804 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -439,7 +439,11 @@ type clbinding =
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * econstr * econstr
+
+(** The following two functions are for internal use only,
+    see [Evarutil.add_unification_pb] for a safe interface. *)
 val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
+val conv_pbs : evar_map -> evar_constraint list
 
 val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 88a91af88..a71ef6508 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -510,7 +510,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
         let tM = Stack.zip evd apprM in
 	  miller_pfenning on_left
 	    (fun () -> if not_only_app then (* Postpone the use of an heuristic *)
-	      switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
+              switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
 	    else quick_fail i)
 	  ev lF tM i
     and consume (termF,skF as apprF) (termM,skM as apprM) i = 
@@ -578,7 +578,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                          i,mkEvar ev
                        else
                          i,Stack.zip evd apprF in
-		     switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
+                     switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i))
 	               tF tR
 		   else
                      UnifFailure (evd,OccurCheck (fst ev,tR)))])