amelioration de la structure des univers

elimination des compteurs globaux de metas et d'evars du noyau
nettoyage de safe_typing.ml (plus de flags)


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

7 files changed, 28 insertions, 20 deletions

diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 6f7d400fe..744e75fa5 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -27,9 +27,10 @@ val interp_type          : 'a evar_map -> env -> Coqast.t -> types
 val interp_sort          : Coqast.t -> sorts
 
 val interp_openconstr    :
-  'a evar_map -> env -> Coqast.t -> (int * constr) list * constr
+  'a evar_map -> env -> Coqast.t -> (existential * constr) list * constr
 val interp_casted_openconstr    :
-  'a evar_map -> env -> Coqast.t -> constr -> (int * constr) list * constr
+  'a evar_map -> env -> Coqast.t -> constr ->
+    (existential * constr) list * constr
 
 (* [interp_type_with_implicits] extends [interp_type] by allowing
    implicits arguments in the ``rel'' part of [env]; the extra
@@ -54,7 +55,7 @@ val interp_constr_gen     :
 val interp_openconstr_gen     :
   'a evar_map -> env -> (identifier * constr) list ->
     (int * constr) list -> Coqast.t -> constr option
-      -> (int * constr) list * constr
+      -> (existential * constr) list * constr
 
 (*Interprets constr patterns according to a list of instantiations
   (variables)*)
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index ba6e8614e..250000b74 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -154,10 +154,11 @@ let print_syntax_entry whatfor sub_pr env se =
     | PH(e,externpr,reln) ->
         let printer =
           match externpr with (* May branch to an other printer *)
-            | Some (c,entry_prec) ->
+            | Some c ->
                 (try (* Test for a primitive printer *)
 		   (Ppprim.map c) (sub_pr whatfor (Some(rule_prec,reln)))
-                 with Not_found -> token_printer (sub_pr c entry_prec))
+                 with Not_found ->
+                   token_printer (sub_pr c (Some(rule_prec,reln))))
             | None -> token_printer (sub_pr whatfor (Some(rule_prec,reln)))
         in 
 	printer (Ast.pat_sub Ast.dummy_loc env e)
diff --git a/parsing/extend.ml4 b/parsing/extend.ml4
index f5969f4b2..d3c0eecba 100644
--- a/parsing/extend.ml4
+++ b/parsing/extend.ml4
@@ -186,8 +186,8 @@ let interp_grammar_command univ astl =
 
 (* Converting and checking pretty-printing command *)
 
-type parenRelation = L | E | Any
 type precedence = int * int * int
+type parenRelation = L | E | Any | Prec of precedence
 
 let compare_prec (a1,b1,c1) (a2,b2,c2) =
   match (a1=a2),(b1=b2),(c1=c2) with
@@ -200,6 +200,7 @@ let tolerable_prec oparent_prec_reln (_,child_prec) =
   match oparent_prec_reln with
     | Some ((_,pprec), L) -> (compare_prec child_prec pprec) < 0
     | Some ((_,pprec), E) -> (compare_prec child_prec pprec) <= 0
+    | Some (_, Prec level) -> (compare_prec child_prec level) <= 0
     | _ -> true
 
 type ppbox =
@@ -212,7 +213,7 @@ type ppbox =
 type tolerability = (string * precedence) * parenRelation
 
 type unparsing_hunk = 
-  | PH of Ast.pat * (string * tolerability option) option * parenRelation
+  | PH of Ast.pat * string option * parenRelation
   | RO of string
   | UNP_BOX of ppbox * unparsing_hunk list
   | UNP_BRK of int * int
@@ -242,13 +243,15 @@ let prec_of_ast = function
   | ast -> invalid_arg_loc (Ast.loc ast,"Syntaxext.prec_of_ast")
 
 let extern_of_ast loc = function
-  | [Str(_,ppextern)] -> Some (ppextern,None)
-  | [Str(_,ppextern);p] -> Some (ppextern,Some ((ppextern,prec_of_ast p),Any))
+  | [Str(_,ppextern)] -> (ppextern, Any)
+  | [Str(_,ppextern);p] ->
+      (ppextern, Prec (prec_of_ast p))
   |  _ -> invalid_arg_loc (loc,"Syntaxext.extern_of_ast")
 
 let rec unparsing_hunk_of_ast vars = function
   | Node(_, "PH", [e; Node (loc,"EXTERN", ext_args)]) ->
-      PH (Ast.val_of_ast vars e, extern_of_ast loc ext_args, Any)
+      let (ppex, rel) = extern_of_ast loc ext_args in
+      PH (Ast.val_of_ast vars e, Some ppex, rel)
   | Node(loc, "PH", [e; Id(_,pr)]) ->
       let reln =
         (match pr with
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 00ffb2097..da77f531d 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -51,8 +51,7 @@ val interp_grammar_command : string -> Coqast.t list -> grammar_command
 (* Dealing with precedences *)
 
 type precedence = int * int * int
-
-type parenRelation = L | E | Any
+type parenRelation = L | E | Any | Prec of precedence
 
 (* Checks if the precedence of the parent printer (None means the
    highest precedence), and the child's one, follow the given
@@ -72,7 +71,7 @@ type ppbox =
   | PpTB
 
 type unparsing_hunk = 
-  | PH of Ast.pat * (string * tolerability option) option * parenRelation
+  | PH of Ast.pat * string option * parenRelation
   | RO of string
   | UNP_BOX of ppbox * unparsing_hunk list
   | UNP_BRK of int * int
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 6792ae044..3b9708dc6 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -414,6 +414,8 @@ open Constr
 open Tactic
 open Vernac
 
+(* current file and toplevel/vernac.ml *)
+
 let define_quotation default s e =
   (if default then
     GEXTEND Gram
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index ef46a0399..ff17c3b74 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -391,15 +391,17 @@ let print_sec_context sec = print_context true (read_sec_context sec)
 
 let print_sec_context_typ sec = print_context false (read_sec_context sec)
 
-let print_val env {uj_val=trm;uj_type=typ} =
-  print_typed_value_in_env env (trm,typ)
+let print_judgment env {uj_val=trm;uj_type=typ} =
+  print_typed_value_in_env env (trm, typ)
     
-let print_type env {uj_val=trm;uj_type=typ} =
-  print_typed_value_in_env env (trm, type_app (nf_betaiota env Evd.empty) typ)
+let print_safe_judgment env j =
+  let trm = Safe_typing.j_val j in
+  let typ = Safe_typing.j_type j in
+  print_typed_value_in_env env (trm, typ)
     
 let print_eval red_fun env {uj_val=trm;uj_type=typ} =
   let ntrm = red_fun env Evd.empty trm in
-  [< 'sTR "     = "; print_type env {uj_val = ntrm; uj_type = typ} >]
+  [< 'sTR "     = "; print_judgment env {uj_val = ntrm; uj_type = typ} >]
 
 let print_name qid = 
   try 
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index c5071367b..c3bf165b1 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -30,8 +30,8 @@ val print_full_context : unit -> std_ppcmds
 val print_full_context_typ : unit -> std_ppcmds
 val print_sec_context : Nametab.qualid -> std_ppcmds
 val print_sec_context_typ : Nametab.qualid -> std_ppcmds
-val print_val : env -> unsafe_judgment -> std_ppcmds
-val print_type : env -> unsafe_judgment -> std_ppcmds
+val print_judgment : env -> unsafe_judgment -> std_ppcmds
+val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
 val print_eval :
   'a reduction_function -> env -> unsafe_judgment -> std_ppcmds
 val print_mutual : section_path -> std_ppcmds