with
Not_found ->
let params =
- (match CicEnvironment.get_cooked_obj ~trust:true uri with
+ let obj = CicEnvironment.get_obj uri in
+ (match obj with
C.Constant _ -> raise ReferenceToConstant
| C.Variable (_,_,_,params) -> params
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst') ->
let params =
- (match CicEnvironment.get_cooked_obj ~trust:true uri with
+ let obj = CicEnvironment.get_obj uri in
+ (match obj with
C.Constant (_,_,_,params) -> params
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof (_,_,_,_,params) -> params
C.Const (uri,exp_named_subst'')
| C.MutInd (uri,typeno,exp_named_subst') ->
let params =
- (match CicEnvironment.get_cooked_obj ~trust:true uri with
+ let obj = CicEnvironment.get_obj uri in
+ (match obj with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof
C.MutInd (uri,typeno,exp_named_subst'')
| C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
let params =
- (match CicEnvironment.get_cooked_obj ~trust:true uri with
+ let obj = CicEnvironment.get_obj uri in
+ (match obj with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof