Bug existential_value au lieu de existential_type + divers sur existential

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

7 files changed, 44 insertions, 52 deletions

diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 94ab793c6a..7a929b9fa3 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -58,15 +58,13 @@ let constant_value env cst =
 
 let name_of_existential n = id_of_string ("?" ^ string_of_int n)
 
-let existential_type sigma c =
-  let (n,args) = destEvar c in
+let existential_type sigma (n,args) =
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
   (* TODO: check args [this comment was in Typeops] *)
   instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
 
-let existential_value sigma c =
-  let (n,args) = destEvar c in
+let existential_value sigma (n,args) =
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
   match info.evar_body with
@@ -79,9 +77,9 @@ let const_abst_opt_value env sigma c =
   match c with
     | DOPN(Const sp,_) ->
 	if evaluable_constant env c then Some (constant_value env c) else None
-    | DOPN(Evar ev,_) ->
+    | DOPN(Evar ev,args) ->
 	if Evd.is_defined sigma ev then 
-	  Some (existential_value sigma c) 
+	  Some (existential_value sigma (ev,args)) 
 	else 
 	  None
     | DOPN(Abst sp,_) ->
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index af4dd6f1d3..40601c6045 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -23,7 +23,7 @@ exception NotEvaluableConst of const_evaluation_error
 val constant_value : env -> constr -> constr
 val constant_type : env -> 'a evar_map -> constant -> typed_type
 
-val existential_value : 'a evar_map -> constr -> constr
-val existential_type : 'a evar_map -> constr -> constr
+val existential_value : 'a evar_map -> existential -> constr
+val existential_type : 'a evar_map -> existential -> constr
 
 val const_abst_opt_value : env -> 'a evar_map -> constr -> constr option
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4361a1bf39..4dfeca8823 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -124,8 +124,8 @@ let red_product env sigma c =
 	  DOPN(AppL,Array.append [|redrec (array_hd cl)|] (array_tl cl))
       | DOPN(Const _,_) when evaluable_constant env x -> 
 	  constant_value env x
-      | DOPN(Evar ev,_) when Evd.is_defined sigma ev -> 
-	  existential_value sigma x
+      | DOPN(Evar ev,args) when Evd.is_defined sigma ev -> 
+	  existential_value sigma (ev,args)
       | DOPN(Abst _,_) when evaluable_abst env x -> 
 	  abst_value env x 
       | DOP2(Cast,c,_) -> redrec c
@@ -353,9 +353,9 @@ let whd_delta_stack env sigma =
             whrec (constant_value env c) l
 	  else 
 	    x,l
-      | DOPN(Evar ev,_) as c ->
+      | DOPN(Evar ev,args) ->
 	  if Evd.is_defined sigma ev then
-            whrec (existential_value sigma c) l
+            whrec (existential_value sigma (ev,args)) l
 	  else 
 	    x,l
       | (DOPN(Abst _,_)) as c ->
@@ -380,9 +380,9 @@ let whd_betadelta_stack env sigma =
 	    whrec (constant_value env x) l
           else 
 	    (x,l)
-      | DOPN(Evar ev,_) ->
+      | DOPN(Evar ev,args) ->
           if Evd.is_defined sigma ev then 
-	    whrec (existential_value sigma x) l
+	    whrec (existential_value sigma (ev,args)) l
           else 
 	    (x,l)
       | DOPN(Abst _,_) ->
@@ -406,9 +406,9 @@ let whd_betadelta env sigma c = applist(whd_betadelta_stack env sigma c [])
 let whd_betaevar_stack env sigma = 
   let rec whrec x l =
     match x with
-      | DOPN(Evar ev,_) ->
+      | DOPN(Evar ev,args) ->
           if Evd.is_defined sigma ev then 
-	    whrec (existential_value sigma x) l
+	    whrec (existential_value sigma (ev,args)) l
           else 
 	    (x,l)
       | DOPN(Abst _,_) ->
@@ -437,9 +437,9 @@ let whd_betadeltaeta_stack env sigma =
 	    whrec (constant_value env x) stack
           else 
 	    (x,stack)
-      | DOPN(Evar ev,_) ->
+      | DOPN(Evar ev,args) ->
           if Evd.is_defined sigma ev then 
-	    whrec (existential_value sigma x) stack
+	    whrec (existential_value sigma (ev,args)) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -576,9 +576,9 @@ let whd_betaiota x = applist (whd_betaiota_stack x [])
 let whd_betaiotaevar_stack env sigma = 
   let rec whrec x stack =
     match x with
-      | DOPN(Evar ev,_) ->
+      | DOPN(Evar ev,args) ->
           if Evd.is_defined sigma ev then 
-	    whrec (existential_value sigma x) stack
+	    whrec (existential_value sigma (ev,args)) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -619,9 +619,9 @@ let whd_betadeltaiota_stack env sigma =
 	    bdi_rec (constant_value env x) stack
           else 
 	    (x,stack)
-      | DOPN(Evar ev,_) ->
+      | DOPN(Evar ev,args) ->
           if Evd.is_defined sigma ev then 
-	    bdi_rec (existential_value sigma x) stack
+	    bdi_rec (existential_value sigma (ev,args)) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -662,9 +662,9 @@ let whd_betadeltaiotaeta_stack env sigma =
 	    whrec (constant_value env x) stack
           else 
 	    (x,stack)
-      | DOPN(Evar ev,_) ->
+      | DOPN(Evar ev,args) ->
           if Evd.is_defined sigma ev then 
-	    whrec (existential_value sigma x) stack
+	    whrec (existential_value sigma (ev,args)) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -1240,12 +1240,10 @@ let poly_args env sigma t =
 exception Uninstantiated_evar of int
 
 let rec whd_ise sigma = function
-  | DOPN(Evar sp,_) as k ->
-      if Evd.in_dom sigma sp then
-        if Evd.is_defined sigma sp then
-          whd_ise sigma (existential_value sigma k)
-        else raise (Uninstantiated_evar sp)
-      else k
+  | DOPN(Evar ev,args) when Evd.in_dom sigma ev ->
+      if Evd.is_defined sigma ev then
+        whd_ise sigma (existential_value sigma (ev,args))
+      else raise (Uninstantiated_evar ev)
   | DOP2(Cast,c,_) -> whd_ise sigma c
   | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
   | c -> c
@@ -1253,11 +1251,8 @@ let rec whd_ise sigma = function
 
 (* 2- undefined existentials are left unchanged *)
 let rec whd_ise1 sigma = function
-  | (DOPN(Evar sp,_) as k) ->
-      if Evd.in_dom sigma sp & Evd.is_defined sigma sp then
-        whd_ise1 sigma (existential_value sigma k)
-      else 
-	k
+  | DOPN(Evar ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
+      whd_ise1 sigma (existential_value sigma (ev,args))
   | DOP2(Cast,c,_) -> whd_ise1 sigma c
   (* A quoi servait cette ligne ???
   | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
@@ -1272,16 +1267,14 @@ let whd_evar env = whd_ise1
 (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
  * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
 
-let rec whd_ise1_metas sigma = function
-  | (DOPN(Evar n,_) as k) ->
-      if Evd.in_dom sigma n then
-	if Evd.is_defined sigma n then
-      	  whd_ise1_metas sigma (existential_value sigma k)
-	else 
-      	  let m = DOP0(Meta (new_meta())) in
-	  DOP2(Cast,m,existential_type sigma k)
-      else
-	k
-  | DOP2(Cast,c,_) -> whd_ise1_metas sigma c
-  | c -> c
+let rec whd_ise1_metas sigma t = 
+  let t' = strip_outer_cast t in
+  match kind_of_term t' with
+  | IsEvar (ev,args as k) when Evd.in_dom sigma ev ->
+      if Evd.is_defined sigma ev then
+      	whd_ise1_metas sigma (existential_value sigma k)
+      else 
+      	let m = DOP0(Meta (new_meta())) in
+	DOP2(Cast,m,existential_type sigma k)
+  | _ -> t'
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b62e31714f..6c7e1bbe5e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -114,7 +114,8 @@ let type_inst_construct i (IndFamily (mis,globargs)) =
   let tc = mis_type_mconstruct i mis in
   prod_applist tc globargs
 
-let type_of_existential env sigma c = Instantiate.existential_value sigma c
+let type_of_existential env sigma c =
+  Instantiate.existential_type sigma (destEvar c)
 
 (* Case. *)
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 241e4ec053..a5c60e09a7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -57,7 +57,7 @@ let tjudge_of_cast_safe sigma env var =
 let rec evar_apprec env isevars stack c =
   let (t,stack) = Reduction.apprec env !isevars c stack in 
   if ise_defined isevars t then 
-    evar_apprec env isevars stack (existential_value !isevars t)
+    evar_apprec env isevars stack (existential_value !isevars (destEvar t))
   else 
     (t,stack)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 10723c42b6..5e89dbc5db 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -325,7 +325,7 @@ let has_undefined_isevars isevars c =
     | DOPN(Evar ev,cl) as k ->
 	if ise_in_dom isevars ev then 
 	  if ise_defined isevars k then 
-	    hasrec (existential_value !isevars k)
+	    hasrec (existential_value !isevars (ev,cl))
 	  else 
 	    failwith "caught"
 	else 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index effc8d4697..80bef43d81 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -177,9 +177,9 @@ let unify_0 mc wc m n =
 let whd_castappevar_stack sigma = 
   let rec whrec x l =
     match x with
-      | DOPN(Evar ev,_) as c ->
+      | DOPN(Evar ev,args) as c ->
 	  if is_defined sigma ev then
-	    whrec (existential_value sigma c) l
+	    whrec (existential_value sigma (ev,args)) l
 	  else
 	    x,l
       | DOP2(Cast,c,_) -> whrec c l