| C.CurrentProof (_,_,body,_) -> whdaux l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
- | C.Abst _ as t -> t (*CSC l should be empty ????? *)
| C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutCase (mutind,cookingsno,i,_,term,pl) as t->
eat_first (num_to_eat,tl)
in
whdaux (ts@l) (List.nth pl (j-1))
- | C.Abst _| C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ -> if l = [] then t else C.Appl (t::l)
)
(fun (_,ty1,bo1) (_,ty2,bo2) b ->
b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
fl1 fl2 true
- | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
+ | (C.Cast _, _) | (_, C.Cast _)
| (C.Implicit, _) | (_, C.Implicit) ->
raise (Impossible 3) (* we don't trust our whd ;-) *)
| (_,_) -> false