From ec86d39f8d1c462a42d13b347f6e309b3d3936e7 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 29 Oct 2008 15:16:55 +0000
Subject: [PATCH] Added a in_universe function

---
 helm/software/components/tactics/universe.ml  | 15 +++++++++++++++
 helm/software/components/tactics/universe.mli |  2 ++
 2 files changed, 17 insertions(+)

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index a7418461e..def2279ca 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -38,6 +38,21 @@ let get_candidates univ ty =
   S.elements (TI.retrieve_unifiables univ ty)
 ;;
 
+let in_universe univ ty =
+  let candidates = get_candidates univ ty in
+    List.fold_left 
+      (fun res cand ->
+	 match res with
+	   | Some found -> Some found
+	   | None -> 
+	       let candty,_ = 
+		 CicTypeChecker.type_of_aux' [] [] cand CicUniv.oblivion_ugraph in
+	       let same ,_ = 
+		 CicReduction.are_convertible [] candty ty CicUniv.oblivion_ugraph in
+	       if same then Some cand else None
+      ) None candidates
+;;
+
 let rec unfold context = function
   | Cic.Prod(name,s,t) -> 
       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli
index de7c20871..d74895114 100644
--- a/helm/software/components/tactics/universe.mli
+++ b/helm/software/components/tactics/universe.mli
@@ -40,6 +40,8 @@ val keys: Cic.context -> Cic.term -> Cic.term list
 (* collapse non-indexable terms, not removing coercions *)
 val key: Cic.term -> Cic.term 
 
+val in_universe: universe -> Cic.term -> Cic.term option
+
 (* indexes the term and its unfolded both without coercions *)
 val index_term_and_unfolded_term: 
   universe -> Cic.context -> Cic.term -> Cic.term -> universe
-- 
2.39.2