X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=54e8ebe050fb5a59cad06150b1c4238daa9da784;hb=790eccfa6b94dc82826d919691f8d4bfadb04573;hp=4d86521074122e31e6907a28c25887355809dd99;hpb=6719c0e318b312b51b089fea3d69d1b7103245ea;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 4d8652107..54e8ebe05 100644
--- 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 *****************************************************)
 
@@ -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