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

4 files changed, 9 insertions, 8 deletions

diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 55c7282c22..c578ceeca4 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -50,7 +50,7 @@ val w_conv_x            : wc -> constr -> constr -> bool
 val w_const_value       : wc -> constant -> constr
 val w_defined_evar      : wc -> existential_key -> bool
 
-val instantiate : evar -> constr -> tactic
+val instantiate : int -> constr -> tactic
 (*
 val instantiate_tac : tactic_arg list -> tactic
 *)
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 1ad520ec1d..1e0abc02c1 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -199,7 +199,7 @@ let pr_evd evd =
   prlist_with_sep pr_fnl
     (fun (ev,evd) ->
        let pe = pr_decl evd in 
-       h 0 (pr_id (id_of_existential ev)  ++ str"=="  ++ pe))
+       h 0 (str (string_of_existential ev)  ++ str"=="  ++ pe))
     (Evd.to_list evd)
     
 let pr_decls decls = pr_evd decls
@@ -212,7 +212,7 @@ let pr_evars =
   prlist_with_sep pr_fnl
     (fun (ev,evd) ->
        let pegl = pr_evgl_sign evd in 
-       (pr_id (id_of_existential ev) ++ str " : " ++ pegl))
+       (str (string_of_existential ev) ++ str " : " ++ pegl))
 
 (* Print an enumerated list of existential variables *)
 let rec pr_evars_int i = function
@@ -221,7 +221,7 @@ let rec pr_evars_int i = function
       let pegl = pr_evgl_sign evd in 
       let pei = pr_evars_int (i+1) rest in
       (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
-              pr_id (id_of_existential ev)  ++ str " : " ++ pegl)) ++ 
+              str (string_of_existential ev)  ++ str " : " ++ pegl)) ++ 
       fnl () ++ pei
 
 let pr_subgoals_existential sigma = function 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 3181adb9b8..70e0d8565a 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -37,7 +37,8 @@ val is_tactic_proof   : proof_tree -> bool
     of existential variables and a signature. *)
 
 val rc_of_gc  : evar_map -> goal -> named_context sigma
-val rc_add    : named_context sigma -> int * goal -> named_context sigma
+val rc_add    : named_context sigma -> existential_key * goal -> 
+  named_context sigma
 val get_hyps  : named_context sigma -> named_context
 val get_env   : named_context sigma -> env
 val get_gc    : named_context sigma -> evar_map
@@ -62,8 +63,8 @@ val pr_evc       : named_context sigma -> std_ppcmds
 
 val prgl         : goal -> std_ppcmds
 val pr_seq       : goal -> std_ppcmds
-val pr_evars     : (int * goal) list -> std_ppcmds
-val pr_evars_int : int -> (int * goal) list -> std_ppcmds
+val pr_evars     : (existential_key * goal) list -> std_ppcmds
+val pr_evars_int : int -> (existential_key * goal) list -> std_ppcmds
 val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds
 
 (* Gives the ast corresponding to a tactic argument *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7ab2003e35..644380f3d3 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -277,7 +277,7 @@ let extract_open_proof sigma pf =
     let meta_cnt = ref 0 in
     let rec f () =
       incr meta_cnt; 
-      if in_dom sigma !meta_cnt then f ()
+      if in_dom sigma (existential_of_int !meta_cnt) then f ()
       else !meta_cnt
     in f
   in