| C.Sort _ as t -> t
| C.Implicit -> assert false
| C.Meta (n, l) ->
- (try
- aux k (CicSubstitution.lift_meta l (List.assoc n subst))
- with Not_found ->
- let l' =
- let i = ref 0 in
- List.map
- (function
- | None -> None
- | Some t ->
- incr i;
- try
- Some (aux k t)
- with Occur ->
- more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
- None)
- l
- in
- 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 *)
+ let l' =
+ let i = ref 0 in
+ List.map
+ (function
+ | None -> None
+ | Some t ->
+ incr i;
+ try
+ Some (aux k t)
+ with Occur ->
+ more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
+ None)
+ l
+ in
+ C.Meta (n, l')
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
| C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)