X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=a663282207c6057ae94cf4fdf4e7360bc74ba58f;hb=124f4cc530827721444de874e1a04ee5012586b1;hp=1c2a7d37fb1a83fc9e15cfc9ec989088a9af57f5;hpb=0583c44e19ee683efab796bf21904bbfc64fbf1e;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 1c2a7d37f..a66328220 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -164,6 +164,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
          match CicTypeChecker.type_of_aux' metasenv context wty with
             C.Sort C.Set -> "cic:/Coq/Init/Logic/eq.ind"
           | C.Sort C.Type
+	  | C.Sort C.CProp
           | C.Sort C.Prop -> "cic:/Coq/Init/Logic_Type/eqT.ind"
           | _ -> assert false
         in