| 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 b t1 t2 ->
b &&
match t1,t2 with
- None,None -> true
+ None,_
+ | _,None -> true
| Some t1',Some t2' -> aux context t1' t2'
- | _,_ -> false
) true l1 l2
| (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
(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