diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/locus.ml | 5 | ||||
| -rw-r--r-- | pretyping/locusops.ml | 4 | ||||
| -rw-r--r-- | pretyping/misctypes.ml | 28 |
3 files changed, 6 insertions, 31 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 = diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 1664e68f2..6b6a3f8a9 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -86,8 +86,8 @@ let concrete_clause_of enum_hyps cl = (** Miscellaneous functions *) let out_arg = function - | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.") - | Misctypes.ArgArg x -> x + | ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.") + | ArgArg x -> x let occurrences_of_hyp id cls = let rec hyp_occ = function diff --git a/pretyping/misctypes.ml b/pretyping/misctypes.ml deleted file mode 100644 index 332a90182..000000000 --- a/pretyping/misctypes.ml +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names - -(** Some utility types for parsing *) - -type 'a or_var = - | ArgArg of 'a - | ArgVar of lident - -type 'a and_short_name = 'a * lident option - -type 'a or_by_notation_r = - | AN of 'a - | ByNotation of (string * string option) - -type 'a or_by_notation = 'a or_by_notation_r CAst.t - -(* NB: the last string in [ByNotation] is actually a [Notation.delimiters], - but this formulation avoids a useless dependency. *) |