in
C.Meta (i,l'))
| C.Sort _ as t -> t
- | C.Implicit -> assert false
+ | C.Implicit _ -> assert false
| C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
| C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
| C.Rel _
| C.Sort _ as t -> t
- | C.Implicit -> assert false
+ | C.Implicit _ -> assert false
| C.Meta (n, l) ->
(* we do not retrieve the term associated to ?n in subst since *)
(* in this way we can restrict if something goes wrong *)
(*CSC: first order unification. Does it help or does it harm? *)
deliftaux k (S.lift m t)
| Some (_,C.Decl t) ->
- (*CSC: The following check seems to be wrong! *)
- (*CSC: B:Set |- ?2 : Set *)
- (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x *)
- (*CSC: Why should I restrict ?2 over B? The instantiation *)
- (*CSC: ?1 := A is perfectly reasonable and well-typed. *)
- (*CSC: Thus I comment out the following two lines that *)
- (*CSC: are the incriminated ones. *)
- (*(* It may augment to_be_restricted *)
- ignore (deliftaux k (S.lift m t)) ;*)
- (*CSC: end of bug commented out *)
C.Rel ((position (m-k) l) + k)
| None -> raise (MetaSubstFailure "RelToHiddenHypothesis"))
| C.Var (uri,exp_named_subst) ->
let l' = deliftl 1 l1 in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)