| None -> raise RelToHiddenHypothesis
)
| C.Var (uri,exp_named_subst) as t ->
- (match CicEnvironment.get_cooked_obj uri with
+ (match CicEnvironment.get_cooked_obj ~trust:false uri with
C.Constant _ -> raise ReferenceToConstant
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
| C.Appl (he::tl) -> whdaux (tl@l) he
| C.Appl [] -> raise (Impossible 1)
| C.Const (uri,exp_named_subst) as t ->
- (match CicEnvironment.get_cooked_obj uri with
+ (match CicEnvironment.get_cooked_obj ~trust:false uri with
C.Constant (_,Some body,_,_) ->
whdaux l (CicSubstitution.subst_vars exp_named_subst body)
| C.Constant _ -> if l = [] then t else C.Appl (t::l)