From c039d78bd098a499a34038e64bd1e5fbe280d7f3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 28 Jul 2017 15:31:28 +0200
Subject: locus: Add an AtLeastOneOccurrence constructor.

The semantics is obviously that it is an error if not at least one
occurrence is found (natural semantics for rewriting for
example).
---
 plugins/ltac/tacintern.ml | 2 +-
 plugins/ltac/tacinterp.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac')

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 525ff7fd0f..d17a8e3cc8 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1746,7 +1746,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 =
-- 
cgit v1.2.3


From 78b51f541d0107f06c21fc1260aae2ab9f7229c5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Oct 2018 18:04:35 +0200
Subject: Change interfaces of evarconv as suggested by Enrico.

Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).

Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).
---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2055b25ff4..ea54973fdc 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
-- 
cgit v1.2.3