Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en interp_constr etc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@356 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 27 insertions, 33 deletions

diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index d762faba10..54c1ce5c20 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -12,52 +12,48 @@ open Rawterm
 
 (* Translation from AST to terms. *)
 
-(*
+val interp_rawconstr     : 'a evar_map -> env -> Coqast.t -> rawconstr
+val interp_constr        : 'a evar_map -> env -> Coqast.t -> constr
+val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
+val interp_type          : 'a evar_map -> env -> Coqast.t -> constr
+val typed_type_of_com    : 'a evar_map -> env -> Coqast.t -> typed_type
+val judgment_of_com      : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
+
+val constr_of_com_pattern : 'a evar_map -> env -> Coqast.t -> constr
+val redexp_of_ast : 
+  'a evar_map -> env -> string * Coqast.t list -> Tacred.red_expr
+
+(* Translation rules from V6 to V7:
+
+constr_of_com_casted -> interp_casted_constr
+constr_of_com_sort   -> interp_type
+constr_of_com        -> interp_constr
+rawconstr_of_com     -> interp_rawconstr  [+ env instead of sign]
+type_of_com          -> typed_type_of_com Evd.empty
+constr_of_com1 true  -> interp_type
+*)
+
+(*i For debug (or obsolete)
 val dbize_op : CoqAst.loc -> string -> CoqAst.t list -> constr list -> constr
 val dbize    : unit assumptions -> CoqAst.t -> constr
 
-val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr
-*)
 val dbize_cci      : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
+val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr
 
-(*
-val absolutize_fw  : 'c evar_map -> unit assumptions -> constr -> constr
-*)
 val dbize_fw       : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
-
-val raw_constr_of_com :
-  'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
+val absolutize_fw  : 'c evar_map -> unit assumptions -> constr -> constr
 val raw_fconstr_of_com :
   'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
+val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr
+val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
+
 val raw_constr_of_compattern :
   'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
 
 val globalize_command : Coqast.t -> Coqast.t
 val globalize_ast     : Coqast.t -> Coqast.t
 
-(*i Ceci était avant dans Trad
-    Maintenant elles sont là car relève des ast i*)
-
-val type_of_com : env -> Coqast.t -> typed_type
-
-val constr_of_com_casted : 'a evar_map -> env -> Coqast.t -> constr ->
-  constr
-
-val constr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
-val constr_of_com : 'a evar_map -> env -> Coqast.t -> constr
-val constr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
-val constr_of_com_pattern : 'a evar_map -> env -> Coqast.t -> constr
-
-val fconstr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
-val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr
-val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
-
-val judgment_of_com1 : 
-  bool -> 'a evar_map -> env -> Coqast.t -> unsafe_judgment
-val judgment_of_com : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
-
 (* Typing with Trad, and re-checking with Mach *)
-(*i
 val fconstruct :'c evar_map -> context -> Coqast.t -> unsafe_judgment
 val fconstruct_type : 'c evar_map -> context -> Coqast.t -> typed_type
 
@@ -67,5 +63,3 @@ val fconstruct_with_univ :
 
 i*)
 
-val redexp_of_ast : 
-  'a evar_map -> env -> string * Coqast.t list -> Tacred.red_expr