X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=d4ab241cbbc64cfe8638980b81e4e051dcf9e57f;hb=6e01bb1ae52fe45ce77a7f950efb5feb295e82b1;hp=ececcf967934f82ee5ccbbeb150b07b85e405b15;hpb=c2a02fcbcaaef7358acebcb27014db4a601ad026;p=helm.git

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index ececcf967..d4ab241cb 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -397,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)