ajouts divers pour module Printer

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

7 files changed, 17 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 34261e7355..b4aaed5f0b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -130,6 +130,8 @@ let lowercase_first_char id = String.lowercase (first_char id)
 let id_of_global env = function
   | Const sp -> 
       basename sp
+  | Evar ev ->
+      id_of_existential ev
   | MutInd (sp,tyi) -> 
       (* Does not work with extracted inductive types when the first 
 	 inductive is logic : if tyi=0 then basename sp else *)
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 52e1a936eb..dd387ddfb4 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -66,3 +66,7 @@ let is_defined sigma ev =
   not (info.evar_body = Evar_empty)
 
 let evar_hyps ev = get_globals (context ev.evar_env)
+
+let id_of_existential ev =
+  id_of_string ("?" ^ string_of_int ev)
+
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 2e55f578e9..6aba6f08d6 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -49,3 +49,5 @@ val is_evar : 'a evar_map -> evar -> bool
 val is_defined : 'a evar_map -> evar -> bool
 
 val evar_hyps : 'a evar_info -> typed_type signature
+
+val id_of_existential : evar -> identifier
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 26dc2b6170..5d7d5309b0 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -220,6 +220,7 @@ let map_var_env f (ENVIRON((dom,rang),r)) =
 	     (fun na x (doml,rangl) -> (na::doml,(f x)::rangl))
       	     dom rang ([],[]),r)
 
+let unitize_env env = map_rel_env (fun _ -> ()) env
 
 type ('b,'a) search_result =
   | GLOBNAME of identifier  * 'b
diff --git a/kernel/sign.mli b/kernel/sign.mli
index af8dbe086f..2a0a567dec 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -85,3 +85,5 @@ type 'b assumptions = (typed_type,'b) env
 type context = (typed_type,typed_type) env
 type var_context = typed_type signature
 
+val unitize_env : 'a assumptions -> unit assumptions
+
diff --git a/kernel/term.ml b/kernel/term.ml
index f7b7b607fd..33056e5ba6 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -294,6 +294,10 @@ let is_small = function
 
 let iskind c = isprop c or is_Type c
 
+let is_existential_oper = function
+  | Evar _ -> true
+  | _ -> false
+
 let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2)
 
 let rec contents_of_kind = function
diff --git a/kernel/term.mli b/kernel/term.mli
index 194681154a..b2ca8658ea 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -239,6 +239,8 @@ val isprop : constr -> bool
 val is_Type : constr -> bool
 val iskind : constr -> bool
 
+val is_existential_oper : sorts oper -> bool
+
 val isType : sorts -> bool
 val is_small : sorts -> bool (* true for \textsf{Prop} and \textsf{Set} *)