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')
+ Cic.Prod(name,s,t')
| t -> ProofEngineReduction.unfold context t
let rec collapse_head_metas t =
let rec dummies_of_coercions =
function
| Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
- Cic.Meta (-1,[])
+ Cic.Meta (-1,[])
| Cic.Appl l ->
- let l' = List.map dummies_of_coercions l in Cic.Appl l'
+ let l' = List.map dummies_of_coercions l in Cic.Appl l'
| Cic.Lambda(n,s,t) ->
- let s' = dummies_of_coercions s in
- let t' = dummies_of_coercions t in
- Cic.Lambda (n,s',t')
+ let s' = dummies_of_coercions s in
+ let t' = dummies_of_coercions t in
+ Cic.Lambda (n,s',t')
| Cic.Prod(n,s,t) ->
- let s' = dummies_of_coercions s in
- let t' = dummies_of_coercions t in
- Cic.Prod (n,s',t')
+ let s' = dummies_of_coercions s in
+ let t' = dummies_of_coercions t in
+ Cic.Prod (n,s',t')
| Cic.LetIn(n,s,t) ->
- let s' = dummies_of_coercions s in
- let t' = dummies_of_coercions t in
- Cic.LetIn (n,s',t')
+ let s' = dummies_of_coercions s in
+ let t' = dummies_of_coercions t in
+ Cic.LetIn (n,s',t')
| Cic.MutCase _ -> Cic.Meta (-1,[])
| t -> t
;;
+
let rec head remove_coercions t =
let clean_up t =
if remove_coercions then dummies_of_coercions t
[head true ty; head true (unfold context ty)]
with ProofEngineTypes.Fail _ -> [head true ty]
+let key term = head false term
+
let index_term_and_unfolded_term univ context t ty =
let key = head true ty in
let univ = index univ key t in