diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
| commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
| tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /intf/misctypes.mli | |
| parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) | |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'intf/misctypes.mli')
| -rw-r--r-- | intf/misctypes.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index a20093bc..1452bbc3 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -31,7 +31,8 @@ and 'constr intro_pattern_action_expr = | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr) | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = - (Loc.t * 'constr intro_pattern_expr) list list + | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list + | IntroAndPattern of (Loc.t * 'constr intro_pattern_expr) list (** Move destination for hypothesis *) @@ -43,7 +44,10 @@ type 'id move_location = (** Sorts *) -type 'a glob_sort_gen = GProp | GSet | GType of 'a +type 'a glob_sort_gen = + | GProp (** representation of [Prop] literal *) + | GSet (** representation of [Set] literal *) + | GType of 'a (** representation of [Type] literal *) type sort_info = string Loc.located list type level_info = string Loc.located option |