Various improvements in handling of evars in general and typing

constraints in Program:
- normalize types and defs of local fixpoints before checking the
guardness condition to avoid having to give type annotations, e.g:
<<
Definition fold (A B : Set) (f : B -> A -> B) : B -> tree A -> B :=
  fix aux acc t :=
    match t with
      | Leaf x => f acc x
      | Node l => fold_left aux l acc
    end.
>>
- add new inh_coerce_to_prod to allow coercion of the typing constraint
to a product before trying to split it. It's a noop in standard mode, 
and forgets subsets in Program. Allows to typecheck:
<< (λ x, x) : { f : nat -> nat | ... } >>.
- Better handling of the "abstract" typing constraints in Program.
- Correctly normalize w.r.t. evars. the tycon given by users in Program.


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

4 files changed, 20 insertions, 7 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index a8af39bc71..4ff60b41f2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -43,6 +43,10 @@ module type S = sig
   val inh_coerce_to_base : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
+  (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
+  val inh_coerce_to_prod : loc ->
+    env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type
+
   (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
@@ -160,6 +164,8 @@ module Default = struct
 
   let inh_coerce_to_base loc env evd j = (evd, j)
 
+  let inh_coerce_to_prod loc env evd t = (evd, t)
+
   let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
     then
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 00735d8746..ff33d679df 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -39,6 +39,10 @@ module type S = sig
      type its base type (the notion depends on the coercion system) *)
   val inh_coerce_to_base : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
+
+  (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
+  val inh_coerce_to_prod : loc ->
+    env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type
     
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 12826851f2..778fb3f0ea 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1183,11 +1183,12 @@ let split_tycon loc env evd tycon =
 		 if cur = 0 then 
 		   let evd', (x, dom, rng) = real_split c in
 		     evd, (Anonymous, 
-			       Some (Some (init, 0), dom), 
-			       Some (Some (init, 0), rng))
+			  Some (None, dom), 
+			  Some (None, rng))
 		 else
-		   evd, (Anonymous, None, Some (Some (init, pred cur), c)))
-
+		   evd, (Anonymous, None, 
+			Some (if cur = 1 then None,c else Some (init, pred cur), c)))
+	    
 let valcon_of_tycon x = 
   match x with
     | Some (None, t) -> Some t
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 11d3b37104..17c7efb457 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -356,7 +356,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env evdref names ftys vdefj;
-	let fixj = match fixkind with
+	let ftys = Array.map (nf_evar (evars_of !evdref)) ftys in
+	let fdefs = Array.map (fun x -> nf_evar (evars_of !evdref) (j_val x)) vdefj in
+ 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
 	      (* If recursive argument was not given by user, we try all args.
@@ -370,11 +372,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
 		vn)
 	      in 
-	      let fixdecls = (names,ftys,Array.map j_val vdefj) in 
+	      let fixdecls = (names,ftys,fdefs) in 
 	      let indexes = search_guard loc env possible_indexes fixdecls in 
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | RCoFix i ->
-	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+	      let cofix = (i,(names,ftys,fdefs)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon