+;;
+
+let find_in_context id context =
+ let rec find_in_context_aux c n =
+ match c with
+ [] -> failwith (id^" not found in context")
+ | a::next -> (match a with
+ Some (Cic.Name(name),Cic.Decl(t)) when name = id -> n
+ | _ -> find_in_context_aux next (n+1))
+ in find_in_context_aux context 1 (*?? bisogna invertire il contesto? ??*)
+;;
+
+(* mi sembra quadratico *)
+let rec filter_real_hyp context =
+ match context with
+ [] -> []
+ | Some(Cic.Name(h),Cic.Def(t))::next -> [(Cic.Rel(find_in_context h next),t)] @
+ filter_real_hyp next
+ | a::next -> filter_real_hyp next
+;;
+
+