Merge PR #7819: Ho matching occ sel

Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot

5 files changed, 7 insertions, 5 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8da30bd9c9..6fd2f7c2bc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
       raise NoChange;
     end
   in
-  let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in
+  let eq_constr c1 c2 =
+    try ignore(Evarconv.unify_delay env sigma c1 c2); true
+    with Evarconv.UnableToUnify _ -> false in
   if not (noccurn sigma 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp sigma t) then nochange "not an equality";
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2d833a2cde..e78d0f93a4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -449,7 +449,7 @@ let evd_convertible env evd x y =
        unsolvable constraints remain, so we check that this unification
        does not introduce any new problem. *)
     let _, pbs = Evd.extract_all_conv_pbs evd in
-    let evd' = Evarconv.the_conv_x env x y evd in
+    let evd' = Evarconv.unify_delay env evd x y in
     let _, pbs' = Evd.extract_all_conv_pbs evd' in
     if evd' == evd || problem_inclusion pbs' pbs then Some evd'
     else None
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index a1e21aab04..543d4de0fe 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -557,7 +557,7 @@ let rec intern_atomic lf ist x =
       | _ -> false
       in
       let is_onconcl = match cl.concl_occs with
-      | AllOccurrences | NoOccurrences -> true
+      | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
       | _ -> false
       in
       TacChange (None,
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 30f716d764..eac84f0543 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1766,7 +1766,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | _ -> false
         in
         let is_onconcl = match cl.concl_occs with
-          | AllOccurrences | NoOccurrences -> true
+          | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
         let c_interp patvars env sigma =
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 552a4048b1..fb99b87108 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -213,7 +213,7 @@ let unif_EQ_args env sigma pa a =
   loop 0
 
 let unif_HO env ise p c =
-  try Evarconv.the_conv_x env p c ise
+  try Evarconv.unify_delay env ise p c
   with Evarconv.UnableToUnify(ise, err) ->
     raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err)))