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, 81 deletions

diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
deleted file mode 100644
index cb1be3ebb8..0000000000
--- a/pretyping/syntax_def.ml
+++ /dev/null
@@ -1,81 +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 Util
-open Pp
-open Names
-open Libnames
-open Rawterm
-open Libobject
-open Lib
-open Nameops
-
-(* Syntactic definitions. *)
-
-let syntax_table = ref (KNmap.empty : rawconstr KNmap.t)
-
-let _ = Summary.declare_summary
-	  "SYNTAXCONSTANT"
-	  { Summary.freeze_function = (fun () -> !syntax_table);
-	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
-	    Summary.init_function = (fun () -> syntax_table := KNmap.empty);
-	    Summary.survive_section = false }
-
-let add_syntax_constant kn c =
-  syntax_table := KNmap.add kn c !syntax_table
-
-let cache_syntax_constant ((sp,kn),c) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_syntax_constant"
-      (pr_id (basename sp) ++ str " already exists");
-  add_syntax_constant kn c;
-  Nametab.push_syntactic_definition (Nametab.Until 1) sp kn
-
-let load_syntax_constant i ((sp,kn),c) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_syntax_constant"
-      (pr_id (basename sp) ++ str " already exists");
-  add_syntax_constant kn c;
-  Nametab.push_syntactic_definition (Nametab.Until i) sp kn
-
-let open_syntax_constant i ((sp,kn),c) =
-  Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
-
-let subst_syntax_constant ((sp,kn),subst,c) =
-  subst_raw subst c
-
-let classify_syntax_constant (_,c) = Substitute c
-
-let (in_syntax_constant, out_syntax_constant) =
-  declare_object {(default_object "SYNTAXCONSTANT") with
-    cache_function = cache_syntax_constant;
-    load_function = load_syntax_constant;
-    open_function = open_syntax_constant;
-    subst_function = subst_syntax_constant;
-    classify_function = classify_syntax_constant;
-    export_function = (fun x -> Some x) } 
-
-let declare_syntactic_definition id c =
-  let _ = add_leaf id (in_syntax_constant c) in ()
-
-let rec set_loc loc = function
-  | RRef (_,a)      -> RRef (loc,a)
-  | RVar (_,a)      -> RVar (loc,a)
-  | RApp (_,a,b)    -> RApp (loc,set_loc loc a,List.map (set_loc loc) b)
-  | RSort (_,a)      -> RSort (loc,a) 
-  | RHole (_,a)      -> RHole (loc,a)
-  | RLambda (_,na,ty,c) -> RLambda (loc,na,set_loc loc ty,set_loc loc c)
-  | RProd (_,na,ty,c) -> RProd (loc,na,set_loc loc ty,set_loc loc c)
-  | RLetIn (_,na,b,c) -> RLetIn (loc,na,set_loc loc b,set_loc loc c)
-  | RCast (_,a,b) -> RCast (loc,set_loc loc a,set_loc loc b)
-  | a -> warning "Unrelocatated syntactic definition"; a
-
-let search_syntactic_definition loc kn =
-  set_loc loc (KNmap.find kn !syntax_table)