From 8aea38ca9b526d1d1ed731948528b4e921b303d2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Nov 2003 12:33:06 +0000
Subject: Prise en compte des defs syntaxiques dans is_global et
 global_reference qui passent donc de Termops a Constrintern

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacmach.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 32951721b5..d6e2245306 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -87,7 +87,7 @@ let pf_interp_type gls c =
   let evc = project gls in 
   Constrintern.interp_type evc (pf_env gls) c
 
-let pf_global gls id = construct_reference (pf_hyps gls) id
+let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
-- 
cgit v1.2.3