-let cache_empty = (TI.empty,[]);;
-let get_candidates (univ,_) ty =
- S.elements (TI.retrieve_unifiables univ ty)
-;;
-
-let rec unfold context = function
- | Cic.Prod(name,s,t) ->
- let t' = unfold ((Some (name,Cic.Decl s))::context) t in
- Cic.Prod(name,s,t')
- | t -> ProofEngineReduction.unfold context t