X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=9eb1e53fa68494ef25c32ef05f4f4adca64d4ed4;hb=eaaf765efc197fa503f05d530e86347d07d138e9;hp=4c2a631761679fb8a01fa808d93af4212cba4bf6;hpb=b10df1955682f76d37bd302ee43987546ec86691;p=helm.git

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 4c2a63176..9eb1e53fa 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -157,7 +157,7 @@ let disambiguate_tactic
                     metasenv,(GrafiteAst.Type (uri, tyno) :: types)
                 | _ ->
                   raise (GrafiteDisambiguator.DisambiguationError
-                   (0,[[[],[],None,lazy "Decompose works only on inductive types"]])))
+                   (0,[[[],[],None,lazy "Decompose works only on inductive types",true]])))
         in
         let metasenv,types =
          List.fold_left disambiguate (metasenv,[]) types
@@ -328,9 +328,9 @@ 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