From e88e0b2140bdd2d194a52bc09f8338b5667d0f92 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Nov 2002 18:37:54 +0000
Subject: Réforme de l'interprétation des termes : - Le parsing se fait
 maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour
 l'instant pour le pretty-printing. Un deuxième   pretty-printer dans
 ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui
 hérite de la partie interprétation qui   se trouvait avant dans "parsing"
 (constrintern.ml remplace astterm.ml;   constrextern.ml est l'équivalent de
 termast.ml pour le nouveau   printer; topconstr.ml; contient la définition de
 "constr_expr";   modintern.ml remplace astmod.ml) - Libnames.reference tend à
 remplacer Libnames.qualid

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/cc/cctac.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'contrib/cc')

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index f7a9e723fa..ca4a249685 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo" i*)
+(*i camlp4deps: "parsing/grammar.cma" i*)
 
 (* $Id$ *)
 
@@ -33,7 +33,7 @@ exception Not_an_eq
 let fail()=raise Not_an_eq
     
 let constr_of_string s () =
-  Declare.constr_of_reference (Nametab.locate (qualid_of_string s))
+  constr_of_reference (Nametab.locate (qualid_of_string s))
 
 let eq2eqT_theo = constr_of_string "Coq.Logic.Eqdep_dec.eq2eqT"
 let eqT2eq_theo = constr_of_string "Coq.Logic.Eqdep_dec.eqT2eq"
@@ -58,7 +58,7 @@ let eq_type_of_term term=
   match kind_of_term term with
       App (f,args)->
 	(try 
-	   let ref = Declare.reference_of_constr f in
+	   let ref = reference_of_constr f in
 	     if (ref=Coqlib.glob_eq || ref=Coqlib.glob_eqT) && 
 	       (Array.length args)=3 
 	     then (args.(0),args.(1),args.(2)) 
-- 
cgit v1.2.3