Modification pour faire compiler pretyping.ml qui maintenant compile

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

2 files changed, 26 insertions, 21 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 6746de0652..3ca214a434 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -703,24 +703,3 @@ let fconstruct_with_univ sigma sign com =
   let(_,j) = with_universes (Mach.fexecute sigma sign)
                (univ_sp, Constraintab.current_constraints(), c)
   in j
-
-
-(* Keeping universe constraints *)
-let fconstruct_type_with_univ_sp sigma sign sp c =
-  with_universes
-    (Mach.fexecute_type sigma sign) (sp,initial_universes,c) 
-
-
-let fconstruct_with_univ_sp sigma sign sp c =
-  with_universes
-    (Mach.fexecute sigma sign) (sp,initial_universes,c) 
-
-
-let infconstruct_type_with_univ_sp sigma (sign,fsign) sp c =
-  with_universes
-    (Mach.infexecute_type sigma (sign,fsign)) (sp,initial_universes,c) 
-
-
-let infconstruct_with_univ_sp sigma (sign,fsign) sp c =
-  with_universes
-    (Mach.infexecute sigma (sign,fsign)) (sp,initial_universes,c) 
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index c6fee417b0..e6029cdb72 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -41,4 +41,30 @@ val raw_constr_of_compattern :
 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 : context -> Coqast.t -> typed_type
+
+val constr_of_com_casted : 'c evar_map -> context -> Coqast.t -> constr ->
+  constr
+
+val constr_of_com1 : bool -> 'c evar_map -> context -> Coqast.t -> constr
+val constr_of_com : 'c evar_map -> context -> Coqast.t -> constr
+val constr_of_com_sort : 'c evar_map -> context -> Coqast.t -> constr
+
+val fconstr_of_com1 : bool -> 'c evar_map -> context -> Coqast.t -> constr
+val fconstr_of_com : 'c evar_map -> context -> Coqast.t -> constr
+val fconstr_of_com_sort : 'c evar_map -> context -> Coqast.t -> constr
+
+(* Typing with Trad, and re-checking with Mach *)
+
+val fconstruct :'c evar_map -> context -> Coqast.t -> unsafe_judgment
+val fconstruct_type :
+  'c evar_map -> context -> Coqast.t -> typed_type
+
+(* Typing, re-checking with universes constraints *)
+val fconstruct_with_univ :
+  'c evar_map -> context -> Coqast.t -> judgement
+
 (* $Id$ *)