commented Record type constructor

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index f7e953b8cb87f71863555982db2dfcd28b1b268d..4697ab6adceca84e0d566ffb66374458a6dbc844 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -134,6 +134,7 @@ type obj =
        *)
   | Record of (string * Ast.term) list * string * Ast.term *
       (string * Ast.term) list
+      (** left parameters, name, type, fields *)
 
 type ('term,'obj) command =
   | Default of loc * string * UriManager.uri list