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, 0 insertions, 133 deletions

diff --git a/parsing/astmod.ml b/parsing/astmod.ml
deleted file mode 100644
index cbb19fa0bf..0000000000
--- a/parsing/astmod.ml
+++ /dev/null
@@ -1,133 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Entries
-open Libnames
-open Coqast
-open Astterm
- 
-let rec make_mp mp = function
-    [] -> mp
-  | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
-
-(*
-(* Since module components are not put in the nametab we try to locate
-the module prefix *)
-exception BadRef
-
-let lookup_qualid (modtype:bool) qid = 
-  let rec make_mp mp = function
-      [] -> mp
-    | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
-  in
-  let rec find_module_prefix dir n =
-    if n<0 then raise Not_found;
-    let dir',dir'' = list_chop n dir in
-    let id',dir''' = 
-      match dir'' with 
-	| hd::tl -> hd,tl 
-	| _ -> anomaly "This list should not be empty!"
-    in
-    let qid' = make_qualid dir' id' in
-      try 
-	match Nametab.locate qid' with
-	  | ModRef mp -> mp,dir'''
-	  | _ -> raise BadRef
-      with
-	  Not_found -> find_module_prefix dir (pred n)
-  in
-    try Nametab.locate qid
-    with Not_found -> 
-      let (dir,id) = repr_qualid qid in
-      let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in
-      let mp = 
-	List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir' 
-      in
-	if modtype then
-	  ModTypeRef (make_ln mp (label_of_id id))
-	else
-	  ModRef (MPdot (mp,label_of_id id))
-
-*)
-
-(* Search for the head of [qid] in [binders]. 
-   If found, returns the module_path/kernel_name created from the dirpath
-   and the basename. Searches Nametab otherwise.
-*)
-
-let lookup_module qid =
-  Nametab.locate_module qid
-	
-let lookup_modtype qid =
-  Nametab.locate_modtype qid
-
-let transl_with_decl env = function 
-  | Node(loc,"WITHMODULE",[id_ast;qid_ast]) ->
-      let id = match id_ast with
-	  Nvar(_,id) -> id
-	| _ -> anomaly "Identifier AST expected"
-      in
-      let qid = match qid_ast with
-	| Node (loc, "QUALID", astl) -> 
-  	    interp_qualid astl
-	| _ -> anomaly "QUALID expected"
-      in
-	With_Module (id,lookup_module qid)
-  | Node(loc,"WITHDEFINITION",[id_ast;cast]) ->
-      let id = match id_ast with
-	  Nvar(_,id) -> id
-	| _ -> anomaly "Identifier AST expected"
-      in
-      let c = interp_constr Evd.empty env cast in
-	With_Definition (id,c)
-  | _ -> anomaly "Unexpected AST"
-
-let rec interp_modtype env = function 
-  | Node(loc,"MODTYPEQID",qid_ast) -> begin match qid_ast with 
-      | [Node (loc, "QUALID", astl)] -> 
-  	  let qid = interp_qualid astl in begin
-	      try 
-	        MTEident (lookup_modtype qid)
-	      with
-	        | Not_found -> 
-		    Modops.error_not_a_modtype (*loc*) (string_of_qualid qid)
-	    end
-      | _ -> anomaly "QUALID expected"
-    end
-  | Node(loc,"MODTYPEWITH",[mty_ast;decl_ast]) ->
-      let mty = interp_modtype env mty_ast in
-      let decl = transl_with_decl env decl_ast in
-	MTEwith(mty,decl)
-  | _ -> anomaly "TODO: transl_modtype: I can handle qualid module types only"
- 
-
-let rec interp_modexpr env = function 
-  | Node(loc,"MODEXPRQID",qid_ast) -> begin match qid_ast with 
-      | [Node (loc, "QUALID", astl)] -> 
-	  let qid = interp_qualid astl in begin
-	    try 
-	      MEident (lookup_module qid)
-	    with
-	      | Not_found -> 
-		 Modops.error_not_a_module (*loc*) (string_of_qualid qid)
-	  end
-      | _ -> anomaly "QUALID expected"
-    end
-  | Node(_,"MODEXPRAPP",[ast1;ast2]) ->
-      let me1 = interp_modexpr env ast1 in
-      let me2 = interp_modexpr env ast2 in
-	MEapply(me1,me2)
-  | Node(_,"MODEXPRAPP",_) -> 
-      anomaly "transl_modexpr: MODEXPRAPP must have two arguments"
-  | _ -> anomaly "transl_modexpr: I can handle MODEXPRQID or MODEXPRAPP only..."
-