summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
bea50d8)
can now be considered convertible.
(fun b t1 t2 ->
b &&
match t1,t2 with
(fun b t1 t2 ->
b &&
match t1,t2 with
+ None,_
+ | _,None -> true
| Some t1',Some t2' -> aux context t1' t2'
| Some t1',Some t2' -> aux context t1' t2'
) 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)) ->
) 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)) ->