Several bugs fixed:

[helm.git] / components / grafite_parser / grafiteParser.ml

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 2d37892217407440aac8957ee8c9029ff1bc9613..9a0cc9f438ae90941aa7f41ddf169bf626777224 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -574,6 +574,11 @@ EXTEND
         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = CicNotationParser.let_defs -> 
+         (* In case of mutual definitions here we produce just
+            the syntax tree for the first one. The others will be
+            generated from the completely specified term just before
+            insertion in the environment. We use the flavour
+            `MutualDefinition to rememer this. *)
           let name,ty = 
             match defs with
             | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
@@ -588,8 +593,14 @@ EXTEND
             | _ -> assert false 
           in
           let body = Ast.Ident (name,None) in
-          GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty,
-            Some (Ast.LetRec (ind_kind, defs, body))))
+          let flavour =
+           if List.length defs = 1 then
+            `Definition
+           else
+            `MutualDefinition
+          in
+           GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
+             Some (Ast.LetRec (ind_kind, defs, body))))
     | IDENT "inductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))