X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=151d8cebdb008d4ab83a22159b391f2ee1944d30;hb=9e18c7f8aa6c5b905598521c769c1a2f58c13262;hp=2e7f1224f795a99b46729613cb5ca816a78161cc;hpb=2135f4eb98004c55f67ae3fa52ca60d53a86d9f2;p=helm.git

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 2e7f1224f..151d8cebd 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -246,6 +246,8 @@ let disambiguate_tactic
         metasenv,GrafiteAst.Ring loc
     | GrafiteAst.Split loc ->
         metasenv,GrafiteAst.Split loc
+    | GrafiteAst.Subst (loc, hyp) ->
+        metasenv, GrafiteAst.Subst (loc, hyp)
     | GrafiteAst.Symmetry loc ->
         metasenv,GrafiteAst.Symmetry loc
     | GrafiteAst.Transitivity (loc, term) -> 
@@ -306,20 +308,16 @@ let disambiguate_tactic
    | GrafiteAst.Thesisbecomes (loc, term) ->
         let metasenv,cic = disambiguate_term context metasenv term in
 	metasenv,GrafiteAst.Thesisbecomes (loc, cic)
-   | GrafiteAst.Let1 (loc, id, term, term1) ->
+   | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
         let metasenv,cic = disambiguate_term context metasenv term in
-	let metasenv,cic'= disambiguate_term context metasenv term1 in
-	metasenv,GrafiteAst.Let1(loc, id, cic, cic')
-   | GrafiteAst.Bywehave (loc, term, term1, id, term2, id1) ->
-        let metasenv,cic = 
-	    match term with 
-	     None -> metasenv,None
-	   | Some t ->
-	         let metasenv,t = disambiguate_term context metasenv t in
-		   metasenv,Some t in
+        let metasenv,cic' = disambiguate_term context metasenv term1 in
+	let metasenv,cic''= disambiguate_term context metasenv term2 in
+	metasenv,GrafiteAst.ExistsElim(loc, cic, id1, cic', id2, cic'')
+   | GrafiteAst.AndElim (loc, term, id, term1, id1, term2) ->
+	let metasenv,cic = disambiguate_term context metasenv term in
 	let metasenv,cic'= disambiguate_term context metasenv term1 in
 	let metasenv,cic''= disambiguate_term context metasenv term2 in
-	metasenv,GrafiteAst.Bywehave(loc, cic, cic', id, cic'', id1)   
+	metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'')   
    | GrafiteAst.Case (loc, id, params) ->
         let metasenv,params' =
 	 List.fold_right
@@ -329,7 +327,7 @@ let disambiguate_tactic
 	  ) params (metasenv,[])
 	in
 	metasenv,GrafiteAst.Case(loc, id, params')   
-   | GrafiteAst.RewritingStep (loc, term1, term2, term3) ->
+   | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
         let metasenv,cic =
 	 match term1 with
 	    None -> metasenv,None
@@ -343,7 +341,7 @@ let disambiguate_tactic
 	  | Some t -> 
 	     let metasenv,t = disambiguate_term context metasenv t in
 	      metasenv,Some t in
-	metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'')   
+	metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)   
 
 
 let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =