diff --git a/dev/ci/user-overlays/20813-dhalilov-better-names-for-induction-principle-cases.sh b/dev/ci/user-overlays/20813-dhalilov-better-names-for-induction-principle-cases.sh new file mode 100644 index 000000000000..8a953f19d237 --- /dev/null +++ b/dev/ci/user-overlays/20813-dhalilov-better-names-for-induction-principle-cases.sh @@ -0,0 +1,3 @@ +overlay hott https://github.com/dhalilov/HoTT better-names-for-induction-principle-cases 20813 + +overlay stdlib https://github.com/dhalilov/stdlib better-names-for-induction-principle-cases 20813 diff --git a/doc/changelog/14-misc/20813-better-names-for-induction-principle-cases-Changed.rst b/doc/changelog/14-misc/20813-better-names-for-induction-principle-cases-Changed.rst new file mode 100644 index 000000000000..b7bc131f3ce7 --- /dev/null +++ b/doc/changelog/14-misc/20813-better-names-for-induction-principle-cases-Changed.rst @@ -0,0 +1,4 @@ +- **Changed:** + Hypotheses of generated induction schemes use the constructor name instead of `f`, `f0`, etc + (`#20813 `_, + by Dario Halilovic). diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 104695cfa1bf..c0b7ebc87108 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -203,8 +203,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib, mip) s = else let cs = lift_constructor (k+1) constrs.(k) in let t = build_branch_type !!env sigma dep (mkRel (k+1)) cs in - let namef = make_name env "f" relevance in - let decl = LocalAssum (namef, t) in + let branch_name = make_annot (Name cs.cs_name) relevance in + let decl = LocalAssum (branch_name, t) in get_branches (RelEnv.push_rel decl env) (k + 1) (decl :: accu) in @@ -589,9 +589,9 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = true dep !!env !evdref (vargs,depPvec,i+j) indi cs recarg in let r_0 = Retyping.relevance_of_sort sfam in - let namef = make_name env "f" r_0 in - mkLambda (namef, p_0, - (onerec (RelEnv.push_rel (LocalAssum (namef,p_0)) env)) (j+1)) + let case_name = make_annot (Name cs.cs_name) r_0 in + mkLambda (case_name, p_0, + (onerec (RelEnv.push_rel (LocalAssum (case_name,p_0)) env)) (j+1)) in onerec env 0 | [] -> makefix i listdepkind diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 46e3d85c6c02..711e60298aba 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -376,6 +376,7 @@ let make_case_info env ind style = (*s Useful functions *) type constructor_summary = { + cs_name : Id.t; cs_cstr : constructor puniverses; cs_params : constr list; cs_nargs : int; @@ -384,6 +385,7 @@ type constructor_summary = { } let lift_constructor n cs = { + cs_name = cs.cs_name; cs_cstr = cs.cs_cstr; cs_params = List.map (lift n) cs.cs_params; cs_nargs = cs.cs_nargs; @@ -412,7 +414,9 @@ let get_constructor ((ind,u),mib,mip,params) j = let (args,ccl) = Term.decompose_prod_decls typi in let (_,allargs) = Constr.decompose_app_list ccl in let vargs = List.skipn (List.length params) allargs in - { cs_cstr = (ith_constructor_of_inductive ind j,u); + let name = mip.mind_consnames.(j-1) in + { cs_name = name; + cs_cstr = (ith_constructor_of_inductive ind j,u); cs_params = params; cs_nargs = Context.Rel.length args; cs_args = EConstr.of_rel_context args; diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 8ceff560aa61..e59c1a4ed706 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -158,6 +158,7 @@ val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> (** Extract information from an inductive family *) type constructor_summary = { + cs_name : Id.t; (* name of the constructor *) cs_cstr : constructor puniverses; (* internal name of the constructor plus universes *) cs_params : constr list; (* parameters of the constructor in current ctx *) cs_nargs : int; (* length of arguments signature (letin included) *) diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 4aa64abe6a0f..58bcc2a0c82d 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -1,13 +1,13 @@ t_rect = -fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => +fun (P : t -> Type) (k : let x := t in forall x0 : x, P x0 -> P (k x0)) => fix F (t : t) : P t := match t as t0 return (P t0) with - | k _ x0 => f x0 (F x0) + | k _ x0 => k x0 (F x0) end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -Arguments t_rect (P f)%_function_scope t +Arguments t_rect (P k)%_function_scope t = fun d : TT => match d with | {| f3 := b |} => b end diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 22fdbdef93f3..0db00fc62c74 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -127,7 +127,7 @@ Alias.eq_ind : forall [A : Type] (x : A) (P : A -> Prop), P x -> forall y : A, x = y -> P y Alias.eq_ind is not universe polymorphic -Arguments Alias.eq_ind [A]%_type_scope x P%_function_scope f y e +Arguments Alias.eq_ind [A]%_type_scope x P%_function_scope eq_refl y e (where some original arguments have been renamed) Alias.eq_ind is transparent Expands to: Constant PrintInfos.Alias.eq_ind (syntactically equal to diff --git a/test-suite/output/PrintMatch.out b/test-suite/output/PrintMatch.out index 0c6e6b5ff77b..3b6556dea323 100644 --- a/test-suite/output/PrintMatch.out +++ b/test-suite/output/PrintMatch.out @@ -1,27 +1,27 @@ eqT_rect@{u u0} = fun (A : Type@{u}) (a : A) (P : forall a0 : A, eqT@{u} a a0 -> Type@{u0}) - (f : P a (reflT@{u} a)) (a0 : A) (e : eqT@{u} a a0) => + (reflT : P a (reflT@{u} a)) (a0 : A) (e : eqT@{u} a a0) => match e :> eqT@{u} a _ as e0 in (eqT _ a1) return (P a1 e0) with -| reflT _ => f +| reflT _ => reflT end : forall (A : Type@{u}) (a : A) (P : forall a0 : A, eqT@{u} a a0 -> Type@{u0}), P a (reflT@{u} a) -> forall (a0 : A) (e : eqT@{u} a a0), P a0 e (* u u0 |= *) -Arguments eqT_rect A%_type_scope a P%_function_scope f a0 e +Arguments eqT_rect A%_type_scope a P%_function_scope reflT a0 e seq_rect = fun (A : Type@{seq_rect.u1}) (a : A) (P : forall a0 : A, seq a a0 -> Type@{seq_rect.u0}) - (f : P a (srefl a)) (a0 : A) (s : seq a a0) => + (srefl : P a (srefl a)) (a0 : A) (s : seq a a0) => match s :> seq a a0 as s0 in (seq _ a1) return (P a1 s0) with -| srefl _ => f +| srefl _ => srefl end : forall (A : Type@{seq_rect.u1}) (a : A) (P : forall a0 : A, seq a a0 -> Type@{seq_rect.u0}), P a (srefl a) -> forall (a0 : A) (s : seq a a0), P a0 s -Arguments seq_rect A%_type_scope a P%_function_scope f a0 s +Arguments seq_rect A%_type_scope a P%_function_scope srefl a0 s eq_sym = fun (A : Type) (x y : A) (H : @eq A x y) => match H in (@eq _ _ a) return (@eq A a x) with diff --git a/test-suite/output/SchemeNames.out b/test-suite/output/SchemeNames.out index 958f6be5ccc8..889027b10915 100644 --- a/test-suite/output/SchemeNames.out +++ b/test-suite/output/SchemeNames.out @@ -20,10 +20,10 @@ Elimination of an inductive object of sort SProp is not allowed on a predicate in sort "Type" because strict proofs can be eliminated only to build strict proofs. fooSProp_inds : -forall P : fooSProp -> SProp, P aSP -> P bSP -> forall f1 : fooSProp, P f1 +forall P : fooSProp -> SProp, P aSP -> P bSP -> forall f : fooSProp, P f fooSProp_inds is not universe polymorphic -Arguments fooSProp_inds P%_function_scope f f0 f1 +Arguments fooSProp_inds P%_function_scope aSP bSP f fooSProp_inds is transparent Expands to: Constant SchemeNames.fooSProp_inds Declared in library SchemeNames, line 13, characters 7-48 @@ -51,7 +51,7 @@ because strict proofs can be eliminated only to build strict proofs. fooSProp_inds_nodep : forall P : SProp, P -> P -> fooSProp -> P fooSProp_inds_nodep is not universe polymorphic -Arguments fooSProp_inds_nodep P%_type_scope f f0 f1 +Arguments fooSProp_inds_nodep P%_type_scope aSP bSP f fooSProp_inds_nodep is transparent Expands to: Constant SchemeNames.fooSProp_inds_nodep Declared in library SchemeNames, line 22, characters 7-49 @@ -77,10 +77,10 @@ Elimination of an inductive object of sort SProp is not allowed on a predicate in sort "Type" because strict proofs can be eliminated only to build strict proofs. fooSProp_cases : -forall P : fooSProp -> SProp, P aSP -> P bSP -> forall f1 : fooSProp, P f1 +forall P : fooSProp -> SProp, P aSP -> P bSP -> forall f : fooSProp, P f fooSProp_cases is not universe polymorphic -Arguments fooSProp_cases P%_function_scope f f0 f1 +Arguments fooSProp_cases P%_function_scope aSP bSP f fooSProp_cases is transparent Expands to: Constant SchemeNames.fooSProp_cases Declared in library SchemeNames, line 31, characters 7-50 @@ -108,7 +108,7 @@ because strict proofs can be eliminated only to build strict proofs. fooSProp_cases_nodep : forall P : SProp, P -> P -> fooSProp -> P fooSProp_cases_nodep is not universe polymorphic -Arguments fooSProp_cases_nodep P%_type_scope f f0 f1 +Arguments fooSProp_cases_nodep P%_type_scope aSP bSP f fooSProp_cases_nodep is transparent Expands to: Constant SchemeNames.fooSProp_cases_nodep Declared in library SchemeNames, line 40, characters 7-43 @@ -131,18 +131,18 @@ Elimination of an inductive object of sort Prop is not allowed on a predicate in sort "Type" because proofs can be eliminated only to build proofs. fooProp_inds_dep : -forall P : fooProp -> SProp, P aP -> P bP -> forall f1 : fooProp, P f1 +forall P : fooProp -> SProp, P aP -> P bP -> forall f : fooProp, P f fooProp_inds_dep is not universe polymorphic -Arguments fooProp_inds_dep P%_function_scope f f0 f1 +Arguments fooProp_inds_dep P%_function_scope aP bP f fooProp_inds_dep is transparent Expands to: Constant SchemeNames.fooProp_inds_dep Declared in library SchemeNames, line 59, characters 7-47 fooProp_ind_dep : -forall P : fooProp -> Prop, P aP -> P bP -> forall f1 : fooProp, P f1 +forall P : fooProp -> Prop, P aP -> P bP -> forall f : fooProp, P f fooProp_ind_dep is not universe polymorphic -Arguments fooProp_ind_dep P%_function_scope f f0 f1 +Arguments fooProp_ind_dep P%_function_scope aP bP f fooProp_ind_dep is transparent Expands to: Constant SchemeNames.fooProp_ind_dep Declared in library SchemeNames, line 60, characters 7-46 @@ -163,14 +163,14 @@ because proofs can be eliminated only to build proofs. fooProp_inds : forall P : SProp, P -> P -> fooProp -> P fooProp_inds is not universe polymorphic -Arguments fooProp_inds P%_type_scope f f0 f1 +Arguments fooProp_inds P%_type_scope aP bP f fooProp_inds is transparent Expands to: Constant SchemeNames.fooProp_inds Declared in library SchemeNames, line 69, characters 7-48 fooProp_ind : forall P : Prop, P -> P -> fooProp -> P fooProp_ind is not universe polymorphic -Arguments fooProp_ind P%_type_scope f f0 f1 +Arguments fooProp_ind P%_type_scope aP bP f fooProp_ind is transparent Expands to: Constant SchemeNames.fooProp_ind Declared in library SchemeNames, line 70, characters 7-47 @@ -189,18 +189,18 @@ Elimination of an inductive object of sort Prop is not allowed on a predicate in sort "Type" because proofs can be eliminated only to build proofs. fooProp_cases_dep : -forall P : fooProp -> SProp, P aP -> P bP -> forall f1 : fooProp, P f1 +forall P : fooProp -> SProp, P aP -> P bP -> forall f : fooProp, P f fooProp_cases_dep is not universe polymorphic -Arguments fooProp_cases_dep P%_function_scope f f0 f1 +Arguments fooProp_cases_dep P%_function_scope aP bP f fooProp_cases_dep is transparent Expands to: Constant SchemeNames.fooProp_cases_dep Declared in library SchemeNames, line 79, characters 7-49 fooProp_case_dep : -forall P : fooProp -> Prop, P aP -> P bP -> forall f1 : fooProp, P f1 +forall P : fooProp -> Prop, P aP -> P bP -> forall f : fooProp, P f fooProp_case_dep is not universe polymorphic -Arguments fooProp_case_dep P%_function_scope f f0 f1 +Arguments fooProp_case_dep P%_function_scope aP bP f fooProp_case_dep is transparent Expands to: Constant SchemeNames.fooProp_case_dep Declared in library SchemeNames, line 80, characters 7-48 @@ -221,14 +221,14 @@ because proofs can be eliminated only to build proofs. fooProp_cases : forall P : SProp, P -> P -> fooProp -> P fooProp_cases is not universe polymorphic -Arguments fooProp_cases P%_type_scope f f0 f1 +Arguments fooProp_cases P%_type_scope aP bP f fooProp_cases is transparent Expands to: Constant SchemeNames.fooProp_cases Declared in library SchemeNames, line 89, characters 7-42 fooProp_case : forall P : Prop, P -> P -> fooProp -> P fooProp_case is not universe polymorphic -Arguments fooProp_case P%_type_scope f f0 f1 +Arguments fooProp_case P%_type_scope aP bP f fooProp_case is transparent Expands to: Constant SchemeNames.fooProp_case Declared in library SchemeNames, line 90, characters 7-41 @@ -237,122 +237,121 @@ The command has indeed failed with message: Cannot extract computational content from proposition "fooProp". fooSet_inds : -forall P : fooSet -> SProp, P aS -> P bS -> forall f1 : fooSet, P f1 +forall P : fooSet -> SProp, P aS -> P bS -> forall f : fooSet, P f fooSet_inds is not universe polymorphic -Arguments fooSet_inds P%_function_scope f f0 f1 +Arguments fooSet_inds P%_function_scope aS bS f fooSet_inds is transparent Expands to: Constant SchemeNames.fooSet_inds Declared in library SchemeNames, line 109, characters 2-41 fooSet_ind : -forall P : fooSet -> Prop, P aS -> P bS -> forall f1 : fooSet, P f1 +forall P : fooSet -> Prop, P aS -> P bS -> forall f : fooSet, P f fooSet_ind is not universe polymorphic -Arguments fooSet_ind P%_function_scope f f0 f1 +Arguments fooSet_ind P%_function_scope aS bS f fooSet_ind is transparent Expands to: Constant SchemeNames.fooSet_ind Declared in library SchemeNames, line 110, characters 2-40 -fooSet_rec : -forall P : fooSet -> Set, P aS -> P bS -> forall f1 : fooSet, P f1 +fooSet_rec : forall P : fooSet -> Set, P aS -> P bS -> forall f : fooSet, P f fooSet_rec is not universe polymorphic -Arguments fooSet_rec P%_function_scope f f0 f1 +Arguments fooSet_rec P%_function_scope aS bS f fooSet_rec is transparent Expands to: Constant SchemeNames.fooSet_rec Declared in library SchemeNames, line 111, characters 2-39 fooSet_rect : -forall P : fooSet -> Type, P aS -> P bS -> forall f1 : fooSet, P f1 +forall P : fooSet -> Type, P aS -> P bS -> forall f : fooSet, P f fooSet_rect is not universe polymorphic -Arguments fooSet_rect P%_function_scope f f0 f1 +Arguments fooSet_rect P%_function_scope aS bS f fooSet_rect is transparent Expands to: Constant SchemeNames.fooSet_rect Declared in library SchemeNames, line 112, characters 2-40 fooSet_inds_nodep : forall P : SProp, P -> P -> fooSet -> P fooSet_inds_nodep is not universe polymorphic -Arguments fooSet_inds_nodep P%_type_scope f f0 f1 +Arguments fooSet_inds_nodep P%_type_scope aS bS f fooSet_inds_nodep is transparent Expands to: Constant SchemeNames.fooSet_inds_nodep Declared in library SchemeNames, line 121, characters 2-42 fooSet_ind_nodep : forall P : Prop, P -> P -> fooSet -> P fooSet_ind_nodep is not universe polymorphic -Arguments fooSet_ind_nodep P%_type_scope f f0 f1 +Arguments fooSet_ind_nodep P%_type_scope aS bS f fooSet_ind_nodep is transparent Expands to: Constant SchemeNames.fooSet_ind_nodep Declared in library SchemeNames, line 122, characters 2-41 fooSet_rec_nodep : forall P : Set, P -> P -> fooSet -> P fooSet_rec_nodep is not universe polymorphic -Arguments fooSet_rec_nodep P%_type_scope f f0 f1 +Arguments fooSet_rec_nodep P%_type_scope aS bS f fooSet_rec_nodep is transparent Expands to: Constant SchemeNames.fooSet_rec_nodep Declared in library SchemeNames, line 123, characters 2-40 fooSet_rect_nodep : forall P : Type, P -> P -> fooSet -> P fooSet_rect_nodep is not universe polymorphic -Arguments fooSet_rect_nodep P%_type_scope f f0 f1 +Arguments fooSet_rect_nodep P%_type_scope aS bS f fooSet_rect_nodep is transparent Expands to: Constant SchemeNames.fooSet_rect_nodep Declared in library SchemeNames, line 124, characters 2-41 fooSet_cases : -forall P : fooSet -> SProp, P aS -> P bS -> forall f1 : fooSet, P f1 +forall P : fooSet -> SProp, P aS -> P bS -> forall f : fooSet, P f fooSet_cases is not universe polymorphic -Arguments fooSet_cases P%_function_scope f f0 f1 +Arguments fooSet_cases P%_function_scope aS bS f fooSet_cases is transparent Expands to: Constant SchemeNames.fooSet_cases Declared in library SchemeNames, line 136, characters 2-43 fooSet_case : -forall P : fooSet -> Prop, P aS -> P bS -> forall f1 : fooSet, P f1 +forall P : fooSet -> Prop, P aS -> P bS -> forall f : fooSet, P f fooSet_case is not universe polymorphic -Arguments fooSet_case P%_function_scope f f0 f1 +Arguments fooSet_case P%_function_scope aS bS f fooSet_case is transparent Expands to: Constant SchemeNames.fooSet_case Declared in library SchemeNames, line 137, characters 2-42 fooSet'_case : -forall P : fooSet' -> Set, P aS' -> P bS' -> forall f1 : fooSet', P f1 +forall P : fooSet' -> Set, P aS' -> P bS' -> forall f : fooSet', P f fooSet'_case is not universe polymorphic -Arguments fooSet'_case P%_function_scope f f0 f1 +Arguments fooSet'_case P%_function_scope aS' bS' f fooSet'_case is transparent Expands to: Constant SchemeNames.fooSet'_case Declared in library SchemeNames, line 138, characters 2-42 fooSet'_caset : -forall P : fooSet' -> Type, P aS' -> P bS' -> forall f1 : fooSet', P f1 +forall P : fooSet' -> Type, P aS' -> P bS' -> forall f : fooSet', P f fooSet'_caset is not universe polymorphic -Arguments fooSet'_caset P%_function_scope f f0 f1 +Arguments fooSet'_caset P%_function_scope aS' bS' f fooSet'_caset is transparent Expands to: Constant SchemeNames.fooSet'_caset Declared in library SchemeNames, line 139, characters 2-43 fooSet_cases_nodep : forall P : SProp, P -> P -> fooSet -> P fooSet_cases_nodep is not universe polymorphic -Arguments fooSet_cases_nodep P%_type_scope f f0 f1 +Arguments fooSet_cases_nodep P%_type_scope aS bS f fooSet_cases_nodep is transparent Expands to: Constant SchemeNames.fooSet_cases_nodep Declared in library SchemeNames, line 148, characters 2-36 fooSet_case_nodep : forall P : Prop, P -> P -> fooSet -> P fooSet_case_nodep is not universe polymorphic -Arguments fooSet_case_nodep P%_type_scope f f0 f1 +Arguments fooSet_case_nodep P%_type_scope aS bS f fooSet_case_nodep is transparent Expands to: Constant SchemeNames.fooSet_case_nodep Declared in library SchemeNames, line 149, characters 2-35 fooSet'_case_nodep : forall P : Set, P -> P -> fooSet' -> P fooSet'_case_nodep is not universe polymorphic -Arguments fooSet'_case_nodep P%_type_scope f f0 f1 +Arguments fooSet'_case_nodep P%_type_scope aS' bS' f fooSet'_case_nodep is transparent Expands to: Constant SchemeNames.fooSet'_case_nodep Declared in library SchemeNames, line 150, characters 2-35 fooSet'_caset_nodep : forall P : Type, P -> P -> fooSet' -> P fooSet'_caset_nodep is not universe polymorphic -Arguments fooSet'_caset_nodep P%_type_scope f f0 f1 +Arguments fooSet'_caset_nodep P%_type_scope aS' bS' f fooSet'_caset_nodep is transparent Expands to: Constant SchemeNames.fooSet'_caset_nodep Declared in library SchemeNames, line 151, characters 2-36 @@ -389,122 +388,122 @@ internal_fooSet_dec_lb is transparent Expands to: Constant SchemeNames.internal_fooSet_dec_lb Declared in library SchemeNames, line 160, characters 2-29 fooType_inds : -forall P : fooType -> SProp, P aT -> P bT -> forall f1 : fooType, P f1 +forall P : fooType -> SProp, P aT -> P bT -> forall f : fooType, P f fooType_inds is not universe polymorphic -Arguments fooType_inds P%_function_scope f f0 f1 +Arguments fooType_inds P%_function_scope aT bT f fooType_inds is transparent Expands to: Constant SchemeNames.fooType_inds Declared in library SchemeNames, line 175, characters 2-42 fooType_ind : -forall P : fooType -> Prop, P aT -> P bT -> forall f1 : fooType, P f1 +forall P : fooType -> Prop, P aT -> P bT -> forall f : fooType, P f fooType_ind is not universe polymorphic -Arguments fooType_ind P%_function_scope f f0 f1 +Arguments fooType_ind P%_function_scope aT bT f fooType_ind is transparent Expands to: Constant SchemeNames.fooType_ind Declared in library SchemeNames, line 176, characters 2-41 fooType_rec : -forall P : fooType -> Set, P aT -> P bT -> forall f1 : fooType, P f1 +forall P : fooType -> Set, P aT -> P bT -> forall f : fooType, P f fooType_rec is not universe polymorphic -Arguments fooType_rec P%_function_scope f f0 f1 +Arguments fooType_rec P%_function_scope aT bT f fooType_rec is transparent Expands to: Constant SchemeNames.fooType_rec Declared in library SchemeNames, line 177, characters 2-40 fooType_rect : -forall P : fooType -> Type, P aT -> P bT -> forall f1 : fooType, P f1 +forall P : fooType -> Type, P aT -> P bT -> forall f : fooType, P f fooType_rect is not universe polymorphic -Arguments fooType_rect P%_function_scope f f0 f1 +Arguments fooType_rect P%_function_scope aT bT f fooType_rect is transparent Expands to: Constant SchemeNames.fooType_rect Declared in library SchemeNames, line 178, characters 2-41 fooType_inds_nodep : forall P : SProp, P -> P -> fooType -> P fooType_inds_nodep is not universe polymorphic -Arguments fooType_inds_nodep P%_type_scope f f0 f1 +Arguments fooType_inds_nodep P%_type_scope aT bT f fooType_inds_nodep is transparent Expands to: Constant SchemeNames.fooType_inds_nodep Declared in library SchemeNames, line 187, characters 2-43 fooType_ind_nodep : forall P : Prop, P -> P -> fooType -> P fooType_ind_nodep is not universe polymorphic -Arguments fooType_ind_nodep P%_type_scope f f0 f1 +Arguments fooType_ind_nodep P%_type_scope aT bT f fooType_ind_nodep is transparent Expands to: Constant SchemeNames.fooType_ind_nodep Declared in library SchemeNames, line 188, characters 2-42 fooType_rec_nodep : forall P : Set, P -> P -> fooType -> P fooType_rec_nodep is not universe polymorphic -Arguments fooType_rec_nodep P%_type_scope f f0 f1 +Arguments fooType_rec_nodep P%_type_scope aT bT f fooType_rec_nodep is transparent Expands to: Constant SchemeNames.fooType_rec_nodep Declared in library SchemeNames, line 189, characters 2-41 fooType_rect_nodep : forall P : Type, P -> P -> fooType -> P fooType_rect_nodep is not universe polymorphic -Arguments fooType_rect_nodep P%_type_scope f f0 f1 +Arguments fooType_rect_nodep P%_type_scope aT bT f fooType_rect_nodep is transparent Expands to: Constant SchemeNames.fooType_rect_nodep Declared in library SchemeNames, line 190, characters 2-42 fooType_cases : -forall P : fooType -> SProp, P aT -> P bT -> forall f1 : fooType, P f1 +forall P : fooType -> SProp, P aT -> P bT -> forall f : fooType, P f fooType_cases is not universe polymorphic -Arguments fooType_cases P%_function_scope f f0 f1 +Arguments fooType_cases P%_function_scope aT bT f fooType_cases is transparent Expands to: Constant SchemeNames.fooType_cases Declared in library SchemeNames, line 202, characters 2-44 fooType_case : -forall P : fooType -> Prop, P aT -> P bT -> forall f1 : fooType, P f1 +forall P : fooType -> Prop, P aT -> P bT -> forall f : fooType, P f fooType_case is not universe polymorphic -Arguments fooType_case P%_function_scope f f0 f1 +Arguments fooType_case P%_function_scope aT bT f fooType_case is transparent Expands to: Constant SchemeNames.fooType_case Declared in library SchemeNames, line 203, characters 2-43 fooType'_case : -forall P : fooType' -> Set, P aT' -> P bT' -> forall f1 : fooType', P f1 +forall P : fooType' -> Set, P aT' -> P bT' -> forall f : fooType', P f fooType'_case is not universe polymorphic -Arguments fooType'_case P%_function_scope f f0 f1 +Arguments fooType'_case P%_function_scope aT' bT' f fooType'_case is transparent Expands to: Constant SchemeNames.fooType'_case Declared in library SchemeNames, line 204, characters 2-43 fooType'_caset : -forall P : fooType' -> Type, P aT' -> P bT' -> forall f1 : fooType', P f1 +forall P : fooType' -> Type, P aT' -> P bT' -> forall f : fooType', P f fooType'_caset is not universe polymorphic -Arguments fooType'_caset P%_function_scope f f0 f1 +Arguments fooType'_caset P%_function_scope aT' bT' f fooType'_caset is transparent Expands to: Constant SchemeNames.fooType'_caset Declared in library SchemeNames, line 205, characters 2-44 fooType_cases_nodep : forall P : SProp, P -> P -> fooType -> P fooType_cases_nodep is not universe polymorphic -Arguments fooType_cases_nodep P%_type_scope f f0 f1 +Arguments fooType_cases_nodep P%_type_scope aT bT f fooType_cases_nodep is transparent Expands to: Constant SchemeNames.fooType_cases_nodep Declared in library SchemeNames, line 214, characters 2-37 fooType_case_nodep : forall P : Prop, P -> P -> fooType -> P fooType_case_nodep is not universe polymorphic -Arguments fooType_case_nodep P%_type_scope f f0 f1 +Arguments fooType_case_nodep P%_type_scope aT bT f fooType_case_nodep is transparent Expands to: Constant SchemeNames.fooType_case_nodep Declared in library SchemeNames, line 215, characters 2-36 fooType'_case_nodep : forall P : Set, P -> P -> fooType' -> P fooType'_case_nodep is not universe polymorphic -Arguments fooType'_case_nodep P%_type_scope f f0 f1 +Arguments fooType'_case_nodep P%_type_scope aT' bT' f fooType'_case_nodep is transparent Expands to: Constant SchemeNames.fooType'_case_nodep Declared in library SchemeNames, line 216, characters 2-36 fooType'_caset_nodep : forall P : Type, P -> P -> fooType' -> P fooType'_caset_nodep is not universe polymorphic -Arguments fooType'_caset_nodep P%_type_scope f f0 f1 +Arguments fooType'_caset_nodep P%_type_scope aT' bT' f fooType'_caset_nodep is transparent Expands to: Constant SchemeNames.fooType'_caset_nodep Declared in library SchemeNames, line 217, characters 2-37 @@ -542,10 +541,10 @@ Expands to: Constant SchemeNames.internal_fooType_dec_lb Declared in library SchemeNames, line 226, characters 2-30 F_rect : forall (f : Type) (P : F f -> Type), -(forall f0 : f, P (C f f0)) -> forall f1 : F f, P f1 +(forall f0 : f, P (C f f0)) -> forall f0 : F f, P f0 F_rect is not universe polymorphic -Arguments F_rect f%_type_scope (P f0)%_function_scope f1 +Arguments F_rect f%_type_scope (P C)%_function_scope f0 F_rect is transparent Expands to: Constant SchemeNames.F_rect Declared in library SchemeNames, line 235, characters 0-30 @@ -554,7 +553,7 @@ forall (P : Type) (P0 : PP P -> Type), (forall p : P, P0 (D P p)) -> forall p : PP P, P0 p PP_rect is not universe polymorphic -Arguments PP_rect P%_type_scope (P0 f)%_function_scope p +Arguments PP_rect P%_type_scope (P0 D)%_function_scope p PP_rect is transparent Expands to: Constant SchemeNames.PP_rect Declared in library SchemeNames, line 238, characters 0-32 diff --git a/test-suite/output/bug_15020.out b/test-suite/output/bug_15020.out index 741f1d0de390..66adb096c1b7 100644 --- a/test-suite/output/bug_15020.out +++ b/test-suite/output/bug_15020.out @@ -3,7 +3,7 @@ forall {A : Type} {x : A} (P : A -> Type), P x -> forall {y : A}, x = y -> P y eq_rect is not universe polymorphic -Arguments eq_rect {A}%_type_scope {x} P%_function_scope f {y} e +Arguments eq_rect {A}%_type_scope {x} P%_function_scope eq_refl {y} e (where some original arguments have been renamed) eq_rect is transparent Expands to: Constant Corelib.Init.Logic.eq_rect