sort CProp added

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index ac5850ca285c07a19f9d6e07e27ffbf442488e44..79304211deb0e8a69f3f1072a8657dc2a33510fa 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -36,6 +36,7 @@ let mk_fresh_name context name ~typ =
        (try
          (match CicTypeChecker.type_of_aux' [] context typ with
              C.Sort C.Prop -> "H"
+          | C.Sort C.CProp -> "H"
            | C.Sort C.Set -> "x"
            | _ -> "H"
          )