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

1 files changed, 5 insertions, 3 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 11d3b3710..17c7efb45 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