Paramétrisation vis à vis de existential_key

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

8 files changed, 30 insertions, 27 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 13ed8e8f6c..bb1bfb67e1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -52,7 +52,7 @@ let filter_sign p sign x =
 (* Expanding existential variables (pretyping.ml) *)
 (* 1- whd_ise fails if an existential is undefined *)
 
-exception Uninstantiated_evar of int
+exception Uninstantiated_evar of existential_key
 
 let rec whd_ise sigma c =
   match kind_of_term c with
@@ -92,7 +92,7 @@ let evar_env evd = Global.env_of_context evd.evar_hyps
 (* Generator of existential names *)
 let new_evar =
   let evar_ctr = ref 0 in
-  fun () -> incr evar_ctr; !evar_ctr
+  fun () -> incr evar_ctr; existential_of_int !evar_ctr
 
 let make_evar_instance env =
   fold_named_context
@@ -212,7 +212,7 @@ type evar_constraint = conv_pb * constr * constr
 type evar_defs =
     { mutable evars : Evd.evar_map;
       mutable conv_pbs : evar_constraint list;
-      mutable history : (int * (loc * Rawterm.hole_kind)) list }
+      mutable history : (existential_key * (loc * Rawterm.hole_kind)) list }
 
 let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] }
 let evars_of d = d.evars
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 9ba82bf1f0..4747bf065e 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -33,7 +33,7 @@ val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 (* Replacing all evars *)
-exception Uninstantiated_evar of int
+exception Uninstantiated_evar of existential_key
 val whd_ise :  evar_map -> constr -> constr
 val whd_castappevar :  evar_map -> constr -> constr
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ee99bfb4ba..66ec64ea16 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -15,7 +15,7 @@ open Sign
 
 (* The type of mappings for existential variables *)
 
-type evar = int
+type evar = existential_key
 
 type evar_body =
   | Evar_empty 
@@ -26,18 +26,20 @@ type evar_info = {
   evar_hyps : named_context;
   evar_body : evar_body}
 
-type evar_map = evar_info Intmap.t
+module Evarmap = Intmap
 
-let empty = Intmap.empty
+type evar_map = evar_info Evarmap.t
 
-let to_list evc = Intmap.fold (fun ev x acc -> (ev,x)::acc) evc []
-let dom evc = Intmap.fold (fun ev _ acc -> ev::acc) evc []
-let map evc k = Intmap.find k evc
-let rmv evc k = Intmap.remove k evc
-let remap evc k i = Intmap.add k i evc
-let in_dom evc k = Intmap.mem k evc
+let empty = Evarmap.empty
 
-let add evd ev newinfo =  Intmap.add ev newinfo evd
+let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc []
+let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc []
+let map evc k = Evarmap.find k evc
+let rmv evc k = Evarmap.remove k evc
+let remap evc k i = Evarmap.add k i evc
+let in_dom evc k = Evarmap.mem k evc
+
+let add evd ev newinfo =  Evarmap.add ev newinfo evd
 
 let define evd ev body = 
   let oldinfo = map evd ev in
@@ -47,7 +49,7 @@ let define evd ev body =
       evar_body = Evar_defined body} 
   in
   match oldinfo.evar_body with
-    | Evar_empty -> Intmap.add ev newinfo evd
+    | Evar_empty -> Evarmap.add ev newinfo evd
     | _ -> anomaly "cannot define an isevar twice"
 
 (* The list of non-instantiated existential declarations *)
@@ -67,6 +69,6 @@ let is_defined sigma ev =
 
 let evar_body ev = ev.evar_body
 
-let id_of_existential ev =
-  id_of_string ("?" ^ string_of_int ev)
+let string_of_existential ev = "?" ^ string_of_int ev
 
+let existential_of_int ev = ev
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index f6a2bb43ac..2ad83c16a7 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -20,7 +20,7 @@ open Sign
    it was introduced ([evar_hyps]) and its definition ([evar_body]). 
    [evar_info] is used to add any other kind of information. *)
 
-type evar = int
+type evar = existential_key
 
 type evar_body =
   | Evar_empty 
@@ -53,4 +53,5 @@ val is_defined : evar_map -> evar -> bool
 
 val evar_body : evar_info -> evar_body
 
-val id_of_existential : evar -> identifier
+val string_of_existential : evar -> string
+val existential_of_int : int -> evar
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index ca25938b6c..78c23ae61e 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -71,7 +71,7 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
       let ci = make_default_case_info env RegularStyle ind in
       let depind = build_dependent_inductive env indf in
       let deparsign = (Anonymous,None,depind)::lnamesar in
-      let p = (* mkRel nbprod *)
+      let p =
       it_mkLambda_or_LetIn_name env'
           (appvect
             (mkRel ((if dep then nbargsprod else mip.mind_nrealargs) + nbprod),
diff --git a/pretyping/instantiate.ml b/pretyping/instantiate.ml
index 95ce7b6bfc..358899098c 100644
--- a/pretyping/instantiate.ml
+++ b/pretyping/instantiate.ml
@@ -47,7 +47,7 @@ let existential_type sigma (n,args) =
   let info =
     try Evd.map sigma n
     with Not_found ->
-      anomaly ("Evar ?"^string_of_int n^" was not declared") in
+      anomaly ("Evar "^(string_of_existential n)^" was not declared") in
   let hyps = info.evar_hyps in
   instantiate_evar hyps info.evar_concl (Array.to_list args)
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ef96bfb048..8b913faa9c 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -23,8 +23,8 @@ type pretype_error =
   (* Old Case *)
   | CantFindCaseType of constr
   (* Unification *)
-  | OccurCheck of int * constr
-  | NotClean of int * constr
+  | OccurCheck of existential_key * constr
+  | NotClean of existential_key * constr
   | UnsolvableImplicit of hole_kind
   (* Pretyping *)
   | VarNotFound of identifier
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index cb26d3078d..6fd4fc05ab 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -24,8 +24,8 @@ type pretype_error =
   (* Old Case *)
   | CantFindCaseType of constr
   (* Unification *)
-  | OccurCheck of int * constr
-  | NotClean of int * constr
+  | OccurCheck of existential_key * constr
+  | NotClean of existential_key * constr
   | UnsolvableImplicit of hole_kind
   (* Pretyping *)
   | VarNotFound of identifier
@@ -74,9 +74,9 @@ val error_ill_typed_rec_body_loc :
 
 (*s Implicit arguments synthesis errors *)
 
-val error_occur_check : env ->  Evd.evar_map -> int -> constr -> 'b
+val error_occur_check : env ->  Evd.evar_map -> existential_key -> constr -> 'b
 
-val error_not_clean : env ->  Evd.evar_map -> int -> constr -> 'b
+val error_not_clean : env ->  Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b