diff options
| author | ppedrot | 2012-06-22 15:14:30 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-22 15:14:30 +0000 |
| commit | 6b45f2d36929162cf92272bb60c2c245d9a0ead3 (patch) | |
| tree | 93aa975697b7de73563c84773d99b4c65b92173b /intf/misctypes.mli | |
| parent | fea214f82954197d23fda9a0e4e7d93e0cbf9b4c (diff) | |
Added an indirection with respect to Loc in Compat. As many [open Compat]
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf/misctypes.mli')
| -rw-r--r-- | intf/misctypes.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index a511458129..b9f5a6dbe2 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -25,7 +25,7 @@ type intro_pattern_expr = | IntroFresh of identifier | IntroForthcoming of bool | IntroAnonymous -and or_and_intro_pattern_expr = (Pp.loc * intro_pattern_expr) list list +and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list (** Move destination for hypothesis *) @@ -52,7 +52,7 @@ type 'a cast_type = type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier -type 'a explicit_bindings = (Pp.loc * quantified_hypothesis * 'a) list +type 'a explicit_bindings = (Loc.t * quantified_hypothesis * 'a) list type 'a bindings = | ImplicitBindings of 'a list @@ -66,13 +66,13 @@ type 'a with_bindings = 'a * 'a bindings type 'a or_var = | ArgArg of 'a - | ArgVar of Names.identifier Pp.located + | ArgVar of Names.identifier Loc.located -type 'a and_short_name = 'a * identifier Pp.located option +type 'a and_short_name = 'a * identifier Loc.located option type 'a or_by_notation = | AN of 'a - | ByNotation of (Pp.loc * string * string option) + | ByNotation of (Loc.t * string * string option) (* NB: the last string in [ByNotation] is actually a [Notation.delimiters], but this formulation avoids a useless dependency. *) |