diff options
Diffstat (limited to 'pretyping/locus.ml')
| -rw-r--r-- | pretyping/locus.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/locus.ml b/pretyping/locus.ml index 95a2e495b..37dd120c1 100644 --- a/pretyping/locus.ml +++ b/pretyping/locus.ml @@ -9,10 +9,13 @@ (************************************************************************) open Names -open Misctypes (** Locus : positions in hypotheses and goals *) +type 'a or_var = + | ArgArg of 'a + | ArgVar of lident + (** {6 Occurrences} *) type 'a occurrences_gen = |