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

1 files changed, 3 insertions, 3 deletions

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))