- Procedural: moved in a directory on its own

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

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 9eb1e53fa68494ef25c32ef05f4f4adca64d4ed4..7d110e2df6a5e4844d894d4ab96f2afb5ee92691 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -130,6 +130,9 @@ let disambiguate_tactic
         metasenv,GrafiteAst.Assumption loc
     | GrafiteAst.Auto (loc,params) ->
         metasenv,GrafiteAst.Auto (loc,params)
+    | GrafiteAst.Cases (loc, what, idents) ->
+        let metasenv,what = disambiguate_term context metasenv what in
+        metasenv,GrafiteAst.Cases (loc, what, idents)
     | GrafiteAst.Change (loc, pattern, with_what) -> 
         let with_what = disambiguate_lazy_term with_what in
         let pattern = disambiguate_pattern pattern in
@@ -233,10 +236,10 @@ let disambiguate_tactic
         let pattern = disambiguate_pattern pattern in
         let with_what = disambiguate_lazy_term with_what in
         metasenv,GrafiteAst.Replace (loc, pattern, with_what)
-    | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
+    | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
         let metasenv,term = disambiguate_term context metasenv t in
         let pattern = disambiguate_pattern pattern in
-        metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern)
+        metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
     | GrafiteAst.Right loc ->
         metasenv,GrafiteAst.Right loc
     | GrafiteAst.Ring loc ->
@@ -295,6 +298,10 @@ let disambiguate_tactic
                    let metasenv,t = disambiguate_term context metasenv t in
                     metasenv,Some t in
        metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'')
+    | GrafiteAst.We_proceed_by_cases_on (loc, term, term') ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+       let metasenv,cic' = disambiguate_term context metasenv term' in
+       metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic')
     | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
         let metasenv,cic = disambiguate_term context metasenv term in
        let metasenv,cic' = disambiguate_term context metasenv term' in