diff options
| -rw-r--r-- | kernel/term.mli | 2 | ||||
| -rw-r--r-- | pretyping/cases.ml | 39 | ||||
| -rw-r--r-- | test-suite/success/CasesDep.v | 7 |
3 files changed, 27 insertions, 21 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 848befbeca..f92471ce03 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -520,7 +520,7 @@ val noccur_between : int -> int -> constr -> bool (** Checking function for terms containing existential- or meta-variables. The function [noccur_with_meta] does not consider - meta-variables applied to some terms (intented to be its local + meta-variables applied to some terms (intended to be its local context) (for existential variables, it is necessarily the case) *) val noccur_with_meta : int -> int -> constr -> bool diff --git a/pretyping/cases.ml b/pretyping/cases.ml index f749efdc78..c61edbc55e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1601,7 +1601,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs sign arsign c = * tycon to make the predicate if it is not closed. *) -let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred = +let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred = let arsign = extract_arity_signature env tomatchs sign in let names = List.rev (List.map (List.map pi1) arsign) in let preds = @@ -1614,32 +1614,31 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred = let pred1 = prepare_predicate_from_arsign_tycon loc tomatchs sign arsign t in (* Second strategy: we build an "inversion" predicate *) - let sigma2,pred2 = build_inversion_problem loc env !evdref tomatchs t in - [!evdref, KnownDep, pred1; sigma2, DepUnknown, pred2] - | None, Some (None, t) -> - (* Only one strategy: we build an "inversion" predicate *) - let sigma,pred = build_inversion_problem loc env !evdref tomatchs t in - [sigma, DepUnknown, pred] - | None, _ -> - (* No type constaints: we use two strategies *) - let t = mkExistential env ~src:(loc, CasesType) evdref in - (* First strategy: we build an inversion problem *) - let sigma1,pred1 = build_inversion_problem loc env !evdref tomatchs t in + let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in + [sigma, KnownDep, pred1; sigma2, DepUnknown, pred2] + | None, _ -> + (* No dependent type constraint, or no constraints at all: *) + (* we use two strategies *) + let sigma,t = match tycon with + | Some (None, t) -> sigma,t + | _ -> new_evar sigma env ~src:(loc, CasesType) (new_Type ()) in + (* First strategy: we build an "inversion" predicate *) + let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Second strategy: we directly use the evar as a non dependent pred *) let pred2 = lift (List.length names) t in - [sigma1, DepUnknown, pred1; !evdref, KnownNotDep, pred2] + [sigma1, DepUnknown, pred1; sigma, KnownNotDep, pred2] (* Some type annotation *) | Some rtntyp, _ -> (* We extract the signature of the arity *) let env = List.fold_right push_rels arsign env in + let evdref = ref sigma in let predcclj = typing_fun (mk_tycon (new_Type ())) env evdref rtntyp in - Option.iter (fun tycon -> + let sigma = Option.cata (fun tycon -> let tycon = lift_tycon_type (List.length arsign) tycon in - evdref := - Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon) - tycon; - let predccl = (j_nf_evar !evdref predcclj).uj_val in - [!evdref, KnownDep, predccl] + Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon) + !evdref tycon in + let predccl = (j_nf_evar sigma predcclj).uj_val in + [sigma, KnownDep, predccl] in List.map (fun (sigma,dep,pred) -> @@ -1663,7 +1662,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e with the type of arguments to match; if none is provided, we build alternative possible predicates *) let sign = List.map snd tomatchl in - let preds = prepare_predicate loc typing_fun evdref env tomatchs sign tycon predopt in + let preds = prepare_predicate loc typing_fun !evdref env tomatchs sign tycon predopt in let compile_for_one_predicate (sigma,nal,pred) = (* We push the initial terms to match and push their alias to rhs' envs *) diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 2972184338..af6e2cd336 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -506,3 +506,10 @@ Definition test (s:step E E) := | Step nil _ (cons E nil) _ Plus l l' => true | _ => false end. + +(* Testing regression of bug 2454 ("get" used not be type-checkable when + defined with its type constraint) *) + +Inductive K : nat -> Type := KC : forall (p q:nat), K p. + +Definition get : K O -> nat := fun x => match x with KC p q => q end. |