sort CProp added

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 8dfdd66c494cb2659ce11294dfeb4490928d8442..b060e009e067f012d8e4dd7e1ee469e7fdfb93c9 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -420,6 +420,7 @@ let elim_tac ~term ~status:(proof, goal) =
       match T.type_of_aux' metasenv context ty with
          C.Sort C.Prop -> "_ind"
        | C.Sort C.Set  -> "_rec"
+       | C.Sort C.CProp -> "_rec"
        | C.Sort C.Type -> "_rect"
        | _ -> assert false
      in