X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=79304211deb0e8a69f3f1072a8657dc2a33510fa;hb=0de1b960f42ac368414b7405a79e7933445ee8af;hp=ac5850ca285c07a19f9d6e07e27ffbf442488e44;hpb=265cf771fbfe217b5f274b999fc3ad887683a09a;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index ac5850ca2..79304211d 100644
--- 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"
          )