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