diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index a77fb84a03..0013fc32f4 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -122,7 +122,7 @@ let constr_of_id id = function if mem_named_context id hyps then mkVar id else - let csr = Declare.global_reference CCI id in + let csr = global_qualified_reference (make_qualid [] id) in (match kind_of_term csr with | IsVar _ -> raise Not_found | _ -> csr) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 8a05e0989b..d429b40691 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -82,7 +82,7 @@ let pf_interp_type gls c = let evc = project gls in Astterm.interp_type evc (pf_env gls) c -let pf_global gls id = Declare.construct_reference (pf_env gls) CCI id +let pf_global gls id = Declare.construct_reference (pf_env gls) id let pf_parse_const gls = compose (pf_global gls) id_of_string |