X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=53142e252bfe90a135405bfe32dd00c008d7b91d;hb=42f2dc48b4fef5b404f406bf512d6a0cde35c067;hp=2fe6b9aaee80949f0130b972cc8bae673ace256f;hpb=55891f80b4f14251dfd5c9111f22f5edcbde2e11;p=helm.git

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 2fe6b9aae..53142e252 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -216,9 +216,13 @@ let rec disambiguate_tactic
          metasenv,GrafiteAst.Decompose (loc, names)
     | GrafiteAst.Demodulate loc ->
         metasenv,GrafiteAst.Demodulate loc
-    | GrafiteAst.Destruct (loc, Some term) ->
-        let metasenv,term = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.Destruct(loc, Some term)
+    | GrafiteAst.Destruct (loc, Some terms) ->
+        let map term (metasenv, terms) =
+           let metasenv, term = disambiguate_term context metasenv term in
+           metasenv, term :: terms
+        in
+        let metasenv, terms = List.fold_right map terms (metasenv, []) in 
+	metasenv, GrafiteAst.Destruct(loc, Some terms)
     | GrafiteAst.Destruct (loc, None) ->
         metasenv,GrafiteAst.Destruct(loc,None)
     | GrafiteAst.Exact (loc, term) -> 
@@ -264,12 +268,12 @@ let rec disambiguate_tactic
        let metasenv,term = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Inversion (loc, term)
     | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
-       let f term to_what =
-          let metasenv,term = disambiguate_term context metasenv term in
-          term :: to_what
+       let f term (metasenv, to_what) =
+          let metasenv, term = disambiguate_term context metasenv term in
+          metasenv, term :: to_what
        in
-       let to_what = List.fold_right f to_what [] in 
-       let metasenv,what = disambiguate_term context metasenv what in
+       let metasenv, to_what = List.fold_right f to_what (metasenv, []) in 
+       let metasenv, what = disambiguate_term context metasenv what in
        metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
     | GrafiteAst.Left loc ->
        metasenv,GrafiteAst.Left loc