]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/grafiteAst.ml
commented Record type constructor
[helm.git] / helm / ocaml / cic_notation / grafiteAst.ml
index f7e953b8cb87f71863555982db2dfcd28b1b268d..4697ab6adceca84e0d566ffb66374458a6dbc844 100644 (file)
@@ -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