From cfba38a75b7166dfaf036833ce0b735242929ba8 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 21 Jun 2008 10:04:11 +0000 Subject: 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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11156 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pretyping.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'pretyping/pretyping.ml') 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 -- cgit v1.2.3