new implementation of the destruct tactic,

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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index ececcf967934f82ee5ccbbeb150b07b85e405b15..2fe6b9aaee80949f0130b972cc8bae673ace256f 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -216,9 +216,11 @@ let rec disambiguate_tactic
          metasenv,GrafiteAst.Decompose (loc, names)
     | GrafiteAst.Demodulate loc ->
         metasenv,GrafiteAst.Demodulate loc
-    | GrafiteAst.Destruct (loc,term) ->
+    | GrafiteAst.Destruct (loc, Some term) ->
         let metasenv,term = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.Destruct(loc,term)
+        metasenv,GrafiteAst.Destruct(loc, Some term)
+    | GrafiteAst.Destruct (loc, None) ->
+        metasenv,GrafiteAst.Destruct(loc,None)
     | GrafiteAst.Exact (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Exact (loc, cic)
@@ -294,8 +296,6 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Ring loc
     | GrafiteAst.Split loc ->
         metasenv,GrafiteAst.Split loc
-    | GrafiteAst.Subst loc ->
-        metasenv, GrafiteAst.Subst loc
     | GrafiteAst.Symmetry loc ->
         metasenv,GrafiteAst.Symmetry loc
     | GrafiteAst.Transitivity (loc, term) -> 
@@ -397,7 +397,8 @@ let rec disambiguate_tactic
            `Auto _ as t -> metasenv,t
          | `Term t -> 
             let metasenv,t = disambiguate_term context metasenv t in
-             metasenv,`Term t in
+             metasenv,`Term t
+          | `Proof as t -> metasenv,t in
        metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)