Reparation bug isevars dans pretyping

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

5 files changed, 8 insertions, 7 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ad02ce58b..67bdfbbcf 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -20,7 +20,7 @@ open Evarutil
 (* This was previously in Indrec but creates existential holes       *)
 
 let mkExistential isevars env =
-  let (c,_) = new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI in c
+  new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI
 
 let norec_branch_scheme env isevars typc =
   let rec crec typc = match whd_betadeltaiota env !isevars typc with 
@@ -789,7 +789,7 @@ let inh_coerce_to_ind isevars env ty tyi =
       (fun (na,ty) (env,evl) ->
 	 let s = get_sort_of env Evd.empty ty in
 	   (push_rel (na,(make_typed ty s)) env,
-	    fst (new_isevar isevars env (mkCast ty (mkSort s)) CCI)::evl))
+	    (new_isevar isevars env (mkCast ty (mkSort s)) CCI)::evl))
       ntys (env,[]) in
   let expected_typ = applist (mkMutInd tyi,evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d80810af5..539a953a1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -324,7 +324,7 @@ and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) =
   let ks =
     List.fold_left
       (fun ks b ->
-	 let (k,_) = new_isevar isevars env (substl ks b) CCI in (k::ks))
+	 (new_isevar isevars env (substl ks b) CCI)::ks)
       [] bs
   in
   if (list_for_all2eq 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 38edd1e32..87fd80963 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -220,7 +220,7 @@ let new_isevar isevars env typ k =
   let (sigma',evar) =
     new_isevar_sign env' !isevars typ' (Array.of_list newargs) in
   isevars := sigma';
-  (evar,typ')
+  evar
 
 
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 03982044e..0758210b1 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -35,7 +35,7 @@ val ise_defined : 'a evar_defs -> constr -> bool
 val real_clean :
   'a evar_defs -> int -> (identifier * constr) list -> constr -> constr
 val new_isevar :
-  'a evar_defs -> env -> constr -> path_kind -> constr * constr
+  'a evar_defs -> env -> constr -> path_kind -> constr
 val evar_define : 'a evar_defs -> constr -> constr -> int list
 val solve_simple_eqn : (constr -> constr -> bool) -> 'a evar_defs ->
   (conv_pb * constr * constr) -> int list option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2ccb6c94b..02742b64c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -298,10 +298,11 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
       let (valc,typc) = (body_of_type v,mkSort (level_of_type v)) in
       {uj_val=valc; uj_type=typc; uj_kind=dummy_sort}
   | (false,(None,Some ty)) ->
-      let (c,ty) = new_isevar isevars env ty CCI in
+      let c = new_isevar isevars env ty CCI in
       {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
   | (true,(None,None)) ->
-      let (c,ty) = new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI in
+      let ty = mkCast dummy_sort dummy_sort in
+      let c = new_isevar isevars env ty CCI in
       {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
   | (false,(None,None)) ->
       (match loc with