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 ececcf967934f82ee5ccbbeb150b07b85e405b15..d4ab241cbbc64cfe8638980b81e4e051dcf9e57f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/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)