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, 4 insertions, 3 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 772eae76b8..cff9b1acf0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -19,6 +19,7 @@ open Typing
 open Classops
 open Recordops 
 open Evarutil
+open Libnames
 
 type flexible_term = FConst of constant | FRel of int | FVar of identifier 
 type flex_kind_of_term =
@@ -70,8 +71,8 @@ let evar_apprec env isevars stack c =
 
 let check_conv_record (t1,l1) (t2,l2) =
   try
-    let proji = Declare.reference_of_constr t1 in
-    let cstr = Declare.reference_of_constr t2 in
+    let proji = reference_of_constr t1 in
+    let cstr = reference_of_constr t2 in
     let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = 
       objdef_info (proji, cstr) in
     let params1, c1, extra_args1 =
@@ -327,7 +328,7 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
   let ks =
     List.fold_left
       (fun ks b ->
-	 let dloc = (Rawterm.dummy_loc,Rawterm.InternalHole) in
+	 let dloc = (dummy_loc,Rawterm.InternalHole) in
 	 (new_isevar isevars env dloc (substl ks b)) :: ks)
       [] bs
   in