diff options
| -rw-r--r-- | pretyping/cases.ml | 22 | ||||
| -rw-r--r-- | test-suite/output/Cases.out | 11 |
2 files changed, 12 insertions, 21 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 33ee579eca..a26e1830d7 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1996,10 +1996,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = * type and 1 assumption for each term not _syntactically_ in an * inductive type. - * Each matched terms are independently considered dependent or not. - - * A type constraint but no annotation case: we try to specialize the - * tycon to make the predicate if it is not closed. + * Each matched term is independently considered dependent or not. *) exception LocalOccur @@ -2031,15 +2028,14 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = | None, Some t when not (noccur_with_meta sigma 0 max_int t) -> (* If the tycon is not closed w.r.t real variables, we try *) (* two different strategies *) - (* First strategy: we abstract the tycon wrt to the dependencies *) - let sigma, t = refresh_tycon sigma t in - let p1 = + (* First strategy: we build an "inversion" predicate *) + let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in + (* Optional second strategy: we abstract the tycon wrt to the dependencies *) + let p2 = prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in - (* Second strategy: we build an "inversion" predicate *) - let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in - (match p1 with - | Some (sigma1,pred1,arsign) -> [sigma1, pred1, arsign; sigma2, pred2, arsign] - | None -> [sigma2, pred2, arsign]) + (match p2 with + | Some (sigma2,pred2,arsign) -> [sigma1, pred1, arsign; sigma2, pred2, arsign] + | None -> [sigma1, pred1, arsign]) | None, _ -> (* No dependent type constraint, or no constraints at all: *) (* we use two strategies *) @@ -2052,7 +2048,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = 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 *) + (* Second strategy: we use the evar or tycon as a non dependent pred *) let pred2 = lift (List.length (List.flatten arsign)) t in [sigma1, pred1, arsign; sigma, pred2, arsign] (* Some type annotation *) diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index dfab400baa..cb835ab48d 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -64,14 +64,9 @@ In environment texpDenote : forall t : type, texp t -> typeDenote t t : type e : texp t -t1 : type -t2 : type -t0 : type -b : tbinop t1 t2 t0 -e1 : texp t1 -e2 : texp t2 -The term "0" has type "nat" while it is expected to have type - "typeDenote t0". +n : nat +The term "n" has type "nat" while it is expected to have type + "typeDenote ?t@{t1:=Nat}". fun '{{n, m, _}} => n + m : J -> nat fun '{{n, m, p}} => n + m + p |