let module S = CicSubstitution in
function
C.Rel n as t ->
- (try
- match List.nth context (n-1) with
- Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_,C.Def (bo,_)) ->
- try_delta_expansion context l t (S.lift n bo)
- | None -> raise RelToHiddenHypothesis
- with
- Failure _ -> assert false)
+ (* we never perform delta expansion automatically *)
+ if l = [] then t else C.Appl (t::l)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
| C.Sort _ as t -> t (* l should be empty *)
| C.Implicit _ as t -> t
| C.Cast (te,ty) ->
- C.Cast (reduceaux context l te, reduceaux context l ty)
+ C.Cast (reduceaux context l te, reduceaux context [] ty)
| C.Prod (name,s,t) ->
assert (l = []) ;
C.Prod (name,