Procedural: bug fix in the procedural rendering of the abstraction

[helm.git] / helm / software / components / acic_procedural / proceduralHelpers.ml

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index d599bdeb2b8420c11ce83573535d11603e3e2b38..54e8ebe050fb5a59cad06150b1c4238daa9da784 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -32,6 +32,8 @@ module PEH  = ProofEngineHelpers
 module E    = CicEnvironment
 module UM   = UriManager
 module D    = Deannotate
+module PER  = ProofEngineReduction
+module Ut   = CicUtil
 
 (* fresh name generator *****************************************************)
 
@@ -133,7 +135,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);
@@ -159,6 +161,16 @@ let get_ind_parameters c t =
 
 let cic = D.deannotate_term
 
+let occurs c ~what ~where =
+   let result = ref false in
+   let equality c t1 t2 =
+      let r = Ut.alpha_equivalence t1 t2 in
+      result := !result || r; r
+   in
+   let context, what, with_what = c, [what], [C.Rel 0] in
+   let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
+   !result
+
 (* Ensuring Barendregt convenction ******************************************)
 
 let rec add_entries map c = function