1. "by proof" now allowed as a justification in equality chains.

[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 fd1849760f986010be8a950833a5bf8eb47aca11..d4ab241cbbc64cfe8638980b81e4e051dcf9e57f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -182,8 +182,8 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.ApplyS (loc, cic, params)
     | GrafiteAst.Assumption loc ->
         metasenv,GrafiteAst.Assumption loc
-    | GrafiteAst.Auto (loc,params) ->
-        metasenv,GrafiteAst.Auto (loc,params)
+    | GrafiteAst.AutoBatch (loc,params) ->
+        metasenv,GrafiteAst.AutoBatch (loc,params)
     | GrafiteAst.Cases (loc, what, idents) ->
         let metasenv,what = disambiguate_term context metasenv what in
         metasenv,GrafiteAst.Cases (loc, what, idents)
@@ -195,6 +195,16 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Clear (loc,id)
     | GrafiteAst.ClearBody (loc,id) ->
        metasenv,GrafiteAst.ClearBody (loc,id)
+    | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
+        let metasenv,t1 = disambiguate_term context metasenv t1 in
+        let metasenv,t2 = 
+          match t2 with
+          | None -> metasenv, None
+          | Some t2 -> 
+              let m, t2 = disambiguate_term context metasenv t2 in
+              m, Some t2
+        in
+        metasenv,   GrafiteAst.Compose (loc, t1, t2, times, spec)
     | GrafiteAst.Constructor (loc,n) ->
         metasenv,GrafiteAst.Constructor (loc,n)
     | GrafiteAst.Contradiction loc ->
@@ -387,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)   
 
 
@@ -477,6 +488,7 @@ let disambiguate_macro
    | GrafiteAst.Check (loc,term) ->
       let metasenv,term = disambiguate_term context metasenv term in
        metasenv,GrafiteAst.Check (loc,term)
+   | GrafiteAst.AutoInteractive _
    | GrafiteAst.Hint _
    | GrafiteAst.WLocate _
    | GrafiteAst.Inline _ as macro ->