X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=4d86521074122e31e6907a28c25887355809dd99;hb=1bbc2dd649df75e33f2cd7fb3e5ecb15f526a442;hp=d599bdeb2b8420c11ce83573535d11603e3e2b38;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index d599bdeb2..4d8652107 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -133,7 +133,7 @@ let get_default_eliminator context uri tyno ty =
    let ext = match get_tail context (get_type context ty) with
       | C.Sort C.Prop     -> "_ind"
       | C.Sort C.Set      -> "_rec"
-      | C.Sort C.CProp    -> "_rec"
+      | C.Sort (C.CProp _)   -> "_rect"
       | C.Sort (C.Type _) -> "_rect"
       | t                 -> 
          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);