From 301a70e45eac43f034077c95bce04edbcf2ab4ad Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 11 Oct 2001 17:27:20 +0000
Subject: 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
---
 proofs/tacinterp.ml | 2 +-
 proofs/tacmach.ml   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

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
 
-- 
cgit v1.2.3