diff options
-rw-r--r-- | library/declare.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/library/declare.ml b/library/declare.ml index 2ccd77cf0..f186aa18c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -239,20 +239,20 @@ let construct_operator env sp id = let global_operator sp id = construct_operator (Global.env()) sp id let construct_sp_reference env sp id = + let (oper,hyps) = construct_operator env sp id in + let hyps' = Global.var_context () in + if not (hyps_inclusion env Evd.empty hyps hyps') then + error_reference_variables CCI env id; + let ids = ids_of_sign hyps in + DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) + +let construct_reference env kind id = try - let (oper,hyps) = construct_operator env sp id in - let hyps' = Global.var_context () in - if not (hyps_inclusion env Evd.empty hyps hyps') then - error_reference_variables CCI env id; - let ids = ids_of_sign hyps in - DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) + let sp = Nametab.sp_of_id kind id in + construct_sp_reference env sp id with Not_found -> VAR (let _ = Environ.lookup_var id env in id) -let construct_reference env kind id = - let sp = Nametab.sp_of_id kind id in - construct_sp_reference env sp id - let global_sp_reference sp id = construct_sp_reference (Global.env()) sp id |