| C.Rel _
| C.Meta _
| C.Sort _
- | C.Implicit -> true
+ | C.Implicit _ -> true
| C.Cast (te,ty) ->
does_not_occur n te && does_not_occur n ty
| C.Prod (name,so,dest) ->
(function None -> None | Some t -> Some (head_beta_reduce t)) l
)
| C.Sort _ as t -> t
- | C.Implicit -> assert false
+ | C.Implicit _ -> assert false
| C.Cast (te,ty) ->
C.Cast (head_beta_reduce te, head_beta_reduce ty)
| C.Prod (n,s,t) ->
(* Checks suppressed *)
CicSubstitution.lift_meta l ty
| C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
- | C.Implicit -> raise (Impossible 21)
+ | C.Implicit _ -> raise (Impossible 21)
| C.Cast (te,ty) ->
(* Let's visit all the subterms that will not be visited later *)
let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
if does_not_occur 1 t_typ then
(* since [Rel 1] does not occur in typ, substituting any term *)
(* in place of [Rel 1] is equivalent to delifting once *)
- CicSubstitution.subst C.Implicit t_typ
+ CicSubstitution.subst (C.Implicit None) t_typ
else
C.LetIn (n,s,t_typ)
| C.Appl (he::tl) when List.length tl > 0 ->