if b1||b2 then true,Cic.Cast (te, ty)
else
not_found
- | Cic.Prod (name, s, t) ->
+ | Cic.Prod (_, s, t) ->
let b1,s = aux s in
let b2,t = aux t in
if b1||b2 then
- true, Cic.Prod (name, s, t)
+ true, Cic.Prod (Cic.Anonymous, s, t)
else
not_found
- | Cic.Lambda (name, s, t) ->
+ | Cic.Lambda (_, s, t) ->
let b1,s = aux s in
let b2,t = aux t in
if b1||b2 then
- true, Cic.Lambda (name, s, t)
+ true, Cic.Lambda (Cic.Anonymous, s, t)
else
not_found
- | Cic.LetIn (name, s, t) ->
+ | Cic.LetIn (_, s, t) ->
let b1,s = aux s in
let b2,t = aux t in
if b1||b2 then
- true, Cic.LetIn (name, s, t)
+ true, Cic.LetIn (Cic.Anonymous, s, t)
else
not_found
| Cic.Appl terms ->
let sort_metasenv (m : Cic.metasenv) =
(MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
;;
-