]> matita.cs.unibo.it Git - helm.git/blobdiff - components/acic_content/cicNotationPt.ml
BIG FAT COMMIT REGARDING COERCIONS:
[helm.git] / components / acic_content / cicNotationPt.ml
index 609fb9d2f24a08f362c2276afa16f8fa2f673737..6ea1ec9175449da004407a76ce43f6265cbf1be9 100644 (file)
@@ -174,7 +174,7 @@ type obj =
        *   will be given in proof editing mode using the tactical language,
        *   unless the flavour is an Axiom
        *)
-  | Record of (string * term) list * string * term * (string * term * bool) list
+  | Record of (string * term) list * string * term * (string * term * bool * int) list
       (** left parameters, name, type, fields *)
 
 (** {2 Standard precedences} *)