From 7a373e3853256b518d8ccb69fa6282211d500e0c Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 16 Dec 2015 15:21:38 +0100
Subject: COMMENTS: added to some variants of "Glob_term.glob_constr" type.

---
 intf/glob_term.mli | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 32cf9eaf13..dfcd4a67d3 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
-- 
cgit v1.2.3