X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FgrafiteAst.ml;h=7d09e2d6a5933c53c59035d6be3764a219205987;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=e845e575557cf9c0a86cf13b82baf3a2d60697dc;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index e845e5755..7d09e2d6a 100644
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -109,15 +109,15 @@ type obj =
   | Inductive of (string * CicNotationPt.term) list *
       CicNotationPt.term inductive_type list
       (** parameters, list of loc * mutual inductive types *)
-  | Theorem of thm_flavour * string * CicNotationPt.term * CicNotationPt.term option
+  | Theorem of thm_flavour * string * CicNotationPt.term *
+      CicNotationPt.term option
       (** flavour, name, type, body
        * - name is absent when an unnamed theorem is being proved, tipically in
        *   interactive usage
        * - body is present when its given along with the command, otherwise it
        *   will be given in proof editing mode using the tactical language
        *)
-  | Record of
-     (string * CicNotationPt.term) list * string * CicNotationPt.term *
+  | Record of (string * CicNotationPt.term) list * string * CicNotationPt.term *
       (string * CicNotationPt.term) list
 
 type ('term,'obj) command =