diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-01 02:37:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
| commit | 615290d0f9d5cad7c508d45cf4ab89aecff033b2 (patch) | |
| tree | f5db022987df54435d807017f4f647ca9e275e9c /pretyping | |
| parent | 4aaeb5d429227505adfde9fe04c3c0fb69f2d37f (diff) | |
[api] Remove Misctypes.
We move the last 3 types to more adequate places.
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. *) |