diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 15:21:38 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:58:05 +0100 |
| commit | 7a373e3853256b518d8ccb69fa6282211d500e0c (patch) | |
| tree | 7693643e544555da655279151cf89f2f4212a1b9 | |
| parent | 722d369d1bd5a0f65b401f24d6500d5496b8e8ab (diff) | |
COMMENTS: added to some variants of "Glob_term.glob_constr" type.
| -rw-r--r-- | intf/glob_term.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 32cf9eaf1..dfcd4a67d 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -29,9 +29,14 @@ type cases_pattern = | PatCstr of Loc.t * constructor * cases_pattern list * Name.t (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) +(** Representation of an internalized (or in other words globalized) term. *) type glob_constr = | GRef of (Loc.t * global_reference * glob_level list option) + (** An identifier that represents a reference to an object defined + either in the (global) environment or in the (local) context. *) | GVar of (Loc.t * Id.t) + (** An identifier that cannot be regarded as "GRef". + Bound variables are typically represented this way. *) | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list @@ -39,8 +44,7 @@ type glob_constr = | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GLetIn of Loc.t * Name.t * glob_constr * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses - (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in - [MatchStyle]) *) + (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr |