- synced notation pretty printing with parsing syntax

[helm.git] / helm / ocaml / cic_notation / grafiteAst.ml

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index e845e575557cf9c0a86cf13b82baf3a2d60697dc..7d09e2d6a5933c53c59035d6be3764a219205987 100644 (file)
--- 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 =