diff options
| author | herbelin | 2001-10-11 17:27:20 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-11 17:27:20 +0000 |
| commit | 301a70e45eac43f034077c95bce04edbcf2ab4ad (patch) | |
| tree | d61c92f0d7a46203618a4610301c64d65c9c03ad /proofs | |
| parent | 1d5b3f16e202af2874181671abd86a47fca37cd7 (diff) | |
Suppression option immediate_discharge; nettoyage de Declare et conséquences
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |