From b9f32144ada6df45194ea011b1c6468e10747c8f Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 1 Apr 2008 13:23:35 +0000 Subject: Finish enhancemenent of return clause inference from tycons, integrating the previous trick of prepare_predicate_from_tycon: if a matched term is dependent, does not appear in the tycon but one of its real arguments is a variable which appears in the tycon, we can transport this dependency in the predicate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10737 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/cases.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7c0ed946f..d14c91f23 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1557,6 +1557,19 @@ let prepare_predicate_from_arsign_tycon loc env evdref tomatchs sign arsign c = | Rel n when dependent tm c && signlen = 1 (* The term to match is not of a dependent type itself *) -> ((n, len) :: subst, len - signlen) + | Rel _ when not (dependent tm c) + && signlen > 1 (* The term is of a dependent type but does not appear in + the tycon, maybe some variable in its type does. *) -> + (match tmtype with + NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *) + | IsInd (_, IndType(indf,realargs)) -> + List.fold_left + (fun (subst, len) arg -> + match kind_of_term arg with + | Rel n when dependent arg c -> + ((n, len) :: subst, pred len) + | _ -> (subst, pred len)) + (subst, len) realargs) | _ -> (subst, len - signlen)) ([], nar) tomatchs arsign in @@ -1596,8 +1609,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function | None -> (match tycon with | Some (None, t) -> - if List.exists (fun (x,_) -> is_dependent_on_rel x t) tomatchs - then + if not (noccur_with_meta 0 max_int t) then (* If the tycon is not closed w.r.t real variables *) let arsign = extract_arity_signature env tomatchs sign in let env' = List.fold_right push_rels arsign env in let names = List.rev (List.map (List.map pi1) arsign) in -- cgit v1.2.3