X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=65371bc67a85f85ee8a29f30901442ad3857f7c8;hb=36014ac060f150e7d93f607c914a0b06239715c0;hp=ae4eac52082e91e30f5ad602f230836b162438b3;hpb=a2b75ceaade20d5ef6b5174883d3ec62ab7de41d;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index ae4eac520..65371bc67 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -328,16 +328,16 @@ let disambiguate_tactic
         let metasenv,cic =
 	 match term1 with
 	    None -> metasenv,None
-	  | Some t -> 
+	  | Some (start,t) -> 
 	     let metasenv,t = disambiguate_term context metasenv t in
-	      metasenv,Some t in
+	      metasenv,Some (start,t) in
 	let metasenv,cic'= disambiguate_term context metasenv term2 in
         let metasenv,cic'' =
 	 match term3 with
-	    None -> metasenv,None
-	  | Some t -> 
+	    `Auto _ as t -> metasenv,t
+	  | `Term t -> 
 	     let metasenv,t = disambiguate_term context metasenv t in
-	      metasenv,Some t in
+	      metasenv,`Term t in
 	metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)