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, 4 insertions, 0 deletions

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