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).
---
 pretyping/locus.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/locus.ml')

diff --git a/pretyping/locus.ml b/pretyping/locus.ml
index 37dd120c1a..087a6b9174 100644
--- a/pretyping/locus.ml
+++ b/pretyping/locus.ml
@@ -20,6 +20,7 @@ type 'a or_var =
 
 type 'a occurrences_gen =
   | AllOccurrences
+  | AtLeastOneOccurrence
   | AllOccurrencesBut of 'a list (** non-empty *)
   | NoOccurrences
   | OnlyOccurrences of 'a list (** non-empty *)
-- 
cgit v1.2.3