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, 16 insertions, 2 deletions

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index bb660ddb4..60f7306ac 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -12,10 +12,11 @@
 
 open Pp
 open Util
-open Coqast
 open Names
 open Nameops
 open Term
+open Libnames
+open Topconstr
 
 (* debug *)
 
@@ -122,6 +123,7 @@ let subst_in_constr alist =
   let alist' = List.map (fun (id,id') -> (id, mkVar id')) alist in
   replace_vars alist'
 
+(*
 let subst_in_ast alist ast =
   let rec subst = function
       Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s)
@@ -130,7 +132,8 @@ let subst_in_ast alist ast =
     | x -> x
   in
     subst ast
-
+*)
+(*
 let subst_ast_in_ast alist ast =
   let rec subst = function
       Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x)
@@ -139,6 +142,17 @@ let subst_ast_in_ast alist ast =
     | x -> x
   in
     subst ast
+*)
+
+let rec subst_in_ast alist = function
+  | CRef (Ident (loc,id)) ->
+      CRef (Ident (loc,(try List.assoc id alist with Not_found -> id)))
+  | x -> map_constr_expr_with_binders subst_in_ast List.remove_assoc alist x
+
+let rec subst_ast_in_ast alist = function
+  | CRef (Ident (_,id)) as x -> (try List.assoc id alist with Not_found -> x)
+  | x ->
+      map_constr_expr_with_binders subst_ast_in_ast List.remove_assoc alist x
 
 (* subst. of variables by constr *)
 let real_subst_in_constr = replace_vars