X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=3653c46069adc15ff3a2be2aa7edc7ca9693ea1f;hb=c0a733b932a64804f67ac93f9ab9f52bd0614fc6;hp=2d37892217407440aac8957ee8c9029ff1bc9613;hpb=77d56df4d446307199a9d4e03478260c6c63baf8;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 2d3789221..3653c4606 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -157,12 +157,9 @@ EXTEND
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
-        idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
-        let types = match types with None -> [] | Some types -> types in
+    | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
 	let idents = match idents with None -> [] | Some idents -> idents in
-	let to_spec id = GrafiteAst.Ident id in
-	GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
+	GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
     | IDENT "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)
@@ -256,12 +253,12 @@ EXTEND
 	 | BYC_weproved (ty,id,t1) ->
 	    GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
 	 | BYC_letsuchthat (id1,t1,id2,t2) ->
-	    (match t with
+	   (* (match t with
 	        LNone floc ->
                  raise (HExtlib.Localized
 		  (floc,CicNotationParser.Parse_error
 		    "tactic_term expected here"))
-              | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
+              | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
 	 | BYC_wehaveand (id1,t1,id2,t2) ->
 	    (match t with
 	        LNone floc ->
@@ -574,6 +571,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 +590,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))
@@ -663,7 +671,7 @@ EXTEND
             (loc,GrafiteAst.Include (iloc,buri))))
     | scom = lexicon_command ; SYMBOL "." ->
        fun ~include_paths status ->
-        let status = LexiconEngine.eval_command status scom in
+	let status = LexiconEngine.eval_command status scom in
          status,LNone loc
     | EOI -> raise End_of_file
     ]