sort CProp added

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 1c2a7d37fb1a83fc9e15cfc9ec989088a9af57f5..a663282207c6057ae94cf4fdf4e7360bc74ba58f 100644 (file)
--- 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