L'instantiation des evars quand un produit ou une sorte étaient attendus n'était pas fait

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

3 files changed, 31 insertions, 17 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5bbd393483..84a6483417 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -66,6 +66,10 @@ let inh_app_fun env isevars j =
   let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
   match kind_of_term t with
     | IsProd (_,_,_) -> j
+    | IsEvar ev when not (is_defined_evar isevars ev) ->
+	let (sigma',t) = define_evar_as_arrow (evars_of isevars) ev in
+	evars_reset_evd sigma' isevars;
+	{ uj_val = j.uj_val; uj_type = t }
     | _ ->
        	(try
  	   let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
@@ -85,6 +89,10 @@ let inh_coerce_to_sort env isevars j =
   let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
   match kind_of_term typ with
     | IsSort s -> { utj_val = j.uj_val; utj_type = s }
+    | IsEvar ev when not (is_defined_evar isevars ev) ->
+	let (sigma', s) = define_evar_as_sort (evars_of isevars) ev in
+	evars_reset_evd sigma' isevars;
+	{ utj_val = j.uj_val; utj_type = s }
     | _ ->
         let j1 = inh_tosort_force env isevars j in 
 	type_judgment env (evars_of isevars) j1 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f23a9c7a12..a1432ff88d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -140,8 +140,7 @@ let new_type_var env sigma =
   let (sigma',c) = new_isevar_sign env sigma (new_Type ()) instance in
   (sigma', c)
 
-let split_evar_to_arrow sigma c =
-  let (ev,args) = destEvar c in
+let split_evar_to_arrow sigma (ev,args) =
   let evd = Evd.map sigma ev in
   let evenv = evar_env evd in
   let (sigma1,dom) = new_type_var evenv sigma in
@@ -153,10 +152,17 @@ let split_evar_to_arrow sigma c =
   let sigma3 = Evd.define sigma2 ev prod in
   let dsp = num_of_evar dom in
   let rsp = num_of_evar rng in
-  (sigma3,
-   mkEvar (dsp,args),
-   mkEvar (rsp, array_cons (mkRel 1) (Array.map (lift 1) args)))
+  (sigma3, prod,
+   (dsp,args), (rsp, array_cons (mkRel 1) (Array.map (lift 1) args)))
 
+let define_evar_as_arrow sigma ev =
+  let (sigma, prod, _, _) = split_evar_to_arrow sigma ev in
+  (sigma, prod)
+
+let define_evar_as_sort sigma (ev,args) =
+  let s = new_Type () in
+  let sigma = Evd.define sigma ev s in
+  (sigma, destSort s)
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
  * variables) such that c becomes closed.
@@ -231,13 +237,11 @@ let ise_map isevars sp = Evd.map isevars.evars sp
 let ise_define isevars sp body =
   isevars.evars <- Evd.define isevars.evars sp body
 
+let is_defined_evar isevars (n,_) = Evd.is_defined isevars.evars n
+
 (* Does k corresponds to an (un)defined existential ? *)
 let ise_undefined isevars c = match kind_of_term c with
-  | IsEvar (n,_) -> not (Evd.is_defined isevars.evars n)
-  | _ -> false
-
-let ise_defined isevars c = match kind_of_term c with
-  | IsEvar (n,_) -> Evd.is_defined isevars.evars n
+  | IsEvar ev -> not (is_defined_evar isevars ev)
   | _ -> false
 
 let need_restriction isevars args = not (array_for_all closed0 args)
@@ -519,13 +523,11 @@ let split_tycon loc env isevars = function
       let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
         | IsProd (na,dom,rng) -> Some dom, Some rng
-	| _ ->
-	    if ise_undefined isevars t then
-	      let (sigma',dom,rng) = split_evar_to_arrow sigma t in
-	      evars_reset_evd sigma' isevars;
-	      Some dom, Some rng
-	    else
-	      error_not_product_loc loc env sigma c
+	| IsEvar (n,_ as ev) when not (Evd.is_defined isevars.evars n) ->
+	    let (sigma',_,evdom,evrng) = split_evar_to_arrow sigma ev in
+	    evars_reset_evd sigma' isevars;
+	    Some (mkEvar evdom), Some (mkEvar evrng)
+	| _ -> error_not_product_loc loc env sigma c
 
 let valcon_of_tycon x = x
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 2d6681f815..73dae829a1 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -50,6 +50,7 @@ val evars_reset_evd : 'a evar_map -> 'a evar_defs -> unit
 type evar_constraint = conv_pb * constr * constr
 val add_conv_pb : 'a evar_defs -> evar_constraint -> unit
 
+val is_defined_evar : 'a evar_defs -> existential -> bool
 val ise_try : 'a evar_defs -> (unit -> bool) list -> bool
 val ise_undefined : 'a evar_defs -> constr -> bool
 val has_undefined_isevars : 'a evar_defs -> constr -> bool
@@ -62,6 +63,9 @@ val solve_simple_eqn :
   (env -> 'a evar_defs -> conv_pb -> constr -> constr -> bool)
   -> env -> 'a evar_defs -> conv_pb * existential * constr -> bool
 
+val define_evar_as_arrow : 'a evar_map -> existential -> 'a evar_map * types
+val define_evar_as_sort : 'a evar_map -> existential -> 'a evar_map * sorts
+
 (* Value/Type constraints *)
 
 val new_Type_sort : unit -> sorts