diff options
92 files changed, 315 insertions, 176 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 0f2dd89975..b0e79fb1b2 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -314,7 +314,7 @@ azure-pipelines.yml @coq/ci-maintainers /test-suite/README.md @gares # Secondary maintainer @SkySkimmer -/test-suite/save-logs @SkySkimmer +/test-suite/report.sh @SkySkimmer /test-suite/complexity/ @herbelin diff --git a/CHANGES.md b/CHANGES.md index d64b5accd7..6789bc038e 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -135,6 +135,17 @@ Universes for the "Private Polymorphic Universes" option (and Unset it to get the previous behaviour). +Inductives + +- An option and attributes to control the automatic decision to + declare an inductive type as template polymorphic were added. + Warning "auto-template" will trigger when an inductive is + automatically declared template polymorphic without the attribute. + +Funind + +- Inductive types declared by Funind will never be template polymorphic. + Misc - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. @@ -144,7 +155,7 @@ SSReflect - New intro patterns: - temporary introduction: => + - block introduction: => [^ prefix ] [^~ suffix ] - - fast introduction: => >H + - fast introduction: => > - tactics as views: => /ltac:mytac See the reference manual for the actual documentation. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md index 8eee2009c9..0720cf6210 100644 --- a/CODE_OF_CONDUCT.md +++ b/CODE_OF_CONDUCT.md @@ -78,7 +78,8 @@ affect a person's ability to participate within them. If you believe someone is violating the code of conduct, we ask that you report it by emailing the Coq Code of Conduct enforcement team at -<coq-conduct@inria.fr>. Confidentiality with regard to the reporter of an +<coq-conduct@inria.fr> or, at your discretion, any member of the team. +Confidentiality with regard to the reporter of an incident will be maintained while dealing with it. In particular, you should seek support from the team instead of dealing by @@ -96,6 +97,11 @@ behavior is wrong). We consider short bans to form part of the pedagogical approach, especially when they come with explanatory comments, as this can give some time to the offender to calm down and think about their actions. +The members of the team are currently: + +- Matthieu Sozeau +- Théo Zimmermann + ## Questions? ## If you have questions, feel free to write to <coq-conduct@inria.fr>. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 1a33a9a46e..8fa631174f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -230,7 +230,7 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. themselves are typing the proofs. We denote propositions by :production:`form`. This constitutes a semantic subclass of the syntactic class :token:`term`. -- :g:`Set` is is the universe of *program types* or *specifications*. The +- :g:`Set` is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index bffbe3e284..92bd4dbd1d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1559,7 +1559,7 @@ whose general syntax is i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) .. prodn:: - i_pattern ::= @ident %| > @ident %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] .. prodn:: i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] @@ -1615,16 +1615,17 @@ annotation: views are interpreted opening the ``ssripat`` scope. a new constant, fact, or defined constant :token:`ident`, respectively. Note that defined constants cannot be introduced when δ-expansion is required to expose the top variable or assumption. -``>``:token:`ident` - pops the first assumption. Type class instances are not considered - as assumptions. - The tactic ``move=> >H`` is equivalent to - ``move=> ? ? H`` with enough ``?`` to name ``H`` the first assumption. - On a goal:: +``>`` + pops every variable occurring in the rest of the stack. + Type class instances are popped even if they don't occur + in the rest of the stack. + The tactic ``move=> >`` is equivalent to + ``move=> ? ?`` on a goal such as:: forall x y, x < y -> G - it names ``H`` the assumption ``x < y``. + A typical use if ``move=>> H`` to name ``H`` the first assumption, + in the example above ``x < y``. ``?`` pops the top variable into an anonymous constant or fact, whose name is picked by the tactic interpreter. |SSR| only generates names that cannot @@ -5305,7 +5306,7 @@ discharge item see :ref:`discharge_ssr` generalization item see :ref:`structure_ssr` -.. prodn:: i_pattern ::= @ident %| > @ident %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] +.. prodn:: i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] intro pattern :ref:`introduction_ssr` diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 98aaa081c3..4b6caea70d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1494,7 +1494,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds false false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ae4cd06022..3e7479903a 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1957,7 +1957,9 @@ let lifts f = (); fun ist x -> Ftactic.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let (sigma, v) = f ist env sigma x in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Ftactic.return v) + (* FIXME once we don't need to catch side effects *) + (Proofview.tclTHEN (Proofview.Unsafe.tclSETENV (Global.env())) + (Ftactic.return v)) end let interp_bindings' ist bl = Ftactic.return begin fun env sigma -> diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 4042959b50..eb84b1203d 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -118,6 +118,7 @@ Section MakeRingPol. - (Pinj i (Pc c)) is (Pc c) *) + #[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol @@ -939,6 +940,7 @@ Qed. (** Definition of polynomial expressions *) + #[universes(template)] Inductive PExpr : Type := | PEc : C -> PExpr | PEX : positive -> PExpr diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index f066ea462f..782fab5e68 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -289,6 +289,7 @@ destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor). now apply (Rplus_nonneg_nonneg sor). Qed. +#[universes(template)] Inductive Psatz : Type := | PsatzIn : nat -> Psatz | PsatzSquare : PolC -> Psatz @@ -685,6 +686,7 @@ end. Definition eval_pexpr : PolEnv -> PExpr C -> R := PEeval rplus rtimes rminus ropp phi pow_phi rpow. +#[universes(template)] Record Formula (T:Type) : Type := { Flhs : PExpr T; Fop : Op2; diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index 458844e1b9..587f2f1fa4 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -21,6 +21,7 @@ Require Import Bool. Set Implicit Arguments. + #[universes(template)] Inductive BFormula (A:Type) : Type := | TT : BFormula A | FF : BFormula A diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index 2d2c0bc77a..c888f9af45 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -30,6 +30,7 @@ Section MakeVarMap. Variable A : Type. Variable default : A. + #[universes(template)] Inductive t : Type := | Empty : t | Leaf : A -> t diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 99c02995fb..751f0d8334 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -81,10 +81,12 @@ Section Store. Variable A:Type. +#[universes(template)] Inductive Poption : Type:= PSome : A -> Poption | PNone : Poption. +#[universes(template)] Inductive Tree : Type := Tempty : Tree | Branch0 : Tree -> Tree -> Tree @@ -177,6 +179,7 @@ generalize i;clear i;induction j;destruct T;simpl in H|-*; destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence. Qed. +#[universes(template)] Record Store : Type := mkStore {index:positive;contents:Tree}. @@ -191,6 +194,7 @@ Lemma get_empty : forall i, get i empty = PNone. intro i; case i; unfold empty,get; simpl;reflexivity. Qed. +#[universes(template)] Inductive Full : Store -> Type:= F_empty : Full empty | F_push : forall a S, Full S -> Full (push a S). diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index ce115f564f..dba72337b2 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -730,6 +730,7 @@ Qed. (* The input: syntax of a field expression *) +#[universes(template)] Inductive FExpr : Type := | FEO : FExpr | FEI : FExpr @@ -762,6 +763,7 @@ Strategy expand [FEeval]. (* The result of the normalisation *) +#[universes(template)] Record linear : Type := mk_linear { num : PExpr C; denum : PExpr C; @@ -944,6 +946,7 @@ induction e2; intros p1 p2; now rewrite <- PEpow_mul_r. Qed. +#[universes(template)] Record rsplit : Type := mk_rsplit { rsplit_left : PExpr C; rsplit_common : PExpr C; diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index f5db275465..15d490a6ab 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -740,6 +740,7 @@ Ltac abstract_ring_morphism set ext rspec := | _ => fail 1 "bad ring structure" end. +#[universes(template)] Record hypo : Type := mkhypo { hypo_type : Type; hypo_proof : hypo_type diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 12208ff6b9..31182f51e2 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -32,6 +32,7 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. with coefficients in C : *) +#[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | PX : Pol -> positive -> positive -> Pol -> Pol. @@ -43,6 +44,7 @@ Definition cI:C . exact ring1. Defined. Definition P1 := Pc 1. Variable Ceqb:C->C->bool. +#[universes(template)] Class Equalityb (A : Type):= {equalityb : A -> A -> bool}. Notation "x =? y" := (equalityb x y) (at level 70, no associativity). Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y). diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index ccd82eabcd..9ef24144d2 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -121,6 +121,7 @@ Section MakeRingPol. - (Pinj i (Pc c)) is (Pc c) *) + #[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol @@ -908,6 +909,7 @@ Section MakeRingPol. (** Definition of polynomial expressions *) + #[universes(template)] Inductive PExpr : Type := | PEO : PExpr | PEI : PExpr diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index d67a8d8dce..6c782269ab 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -540,6 +540,7 @@ Section AddRing. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). Variable req : R -> R -> Prop. *) +#[universes(template)] Inductive ring_kind : Type := | Abstract | Computational diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index fac524da6b..dd2c2d0ba4 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -64,8 +64,6 @@ type ast_closure_term = { type ssrview = ast_closure_term list -type id_mod = Dependent - type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int (* Only [One] forces an introduction, possibly reducing the goal. *) @@ -77,7 +75,7 @@ type anon_iter = type ssripat = | IPatNoop - | IPatId of id_mod option * Id.t + | IPatId of Id.t | IPatAnon of anon_iter (* inaccessible name *) (* TODO | IPatClearMark *) | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss_or_block (* (..|..) *) @@ -88,6 +86,7 @@ type ssripat = | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl | IPatAbstractVars of Id.t list + | IPatFastNondep | IPatEqGen of unit Proofview.tactic (* internal use: generation of eqn *) and ssripats = ssripat list diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 3a7cf41d43..ed4ff2aa66 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -609,6 +609,7 @@ Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3. (** Allow the direct application of a reflection lemma to a boolean assertion. **) Coercion elimT : reflect >-> Funclass. +#[universes(template)] Variant implies P Q := Implies of P -> Q. Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed. Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P. @@ -1130,10 +1131,12 @@ Proof. by move=> *; apply/orP; left. Qed. Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2). Proof. by move=> *; apply/orP; right. Qed. +#[universes(template)] Variant mem_pred := Mem of pred T. Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]). +#[universes(template)] Structure predType := PredType { pred_sort :> Type; topred : pred_sort -> pred T; @@ -1275,6 +1278,7 @@ Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT). implementation of unification, notably improper expansion of telescope projections and overwriting of a variable assignment by a later unification (probably due to conversion cache cross-talk). **) +#[universes(template)] Structure manifest_applicative_pred p := ManifestApplicativePred { manifest_applicative_pred_value :> pred T; _ : manifest_applicative_pred_value = p @@ -1283,18 +1287,21 @@ Definition ApplicativePred p := ManifestApplicativePred (erefl p). Canonical applicative_pred_applicative sp := ApplicativePred (applicative_pred_of_simpl sp). +#[universes(template)] Structure manifest_simpl_pred p := ManifestSimplPred { manifest_simpl_pred_value :> simpl_pred T; _ : manifest_simpl_pred_value = SimplPred p }. Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)). +#[universes(template)] Structure manifest_mem_pred p := ManifestMemPred { manifest_mem_pred_value :> mem_pred T; _ : manifest_mem_pred_value= Mem [eta p] }. Canonical expose_mem_pred p := @ManifestMemPred p _ (erefl _). +#[universes(template)] Structure applicative_mem_pred p := ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}. Canonical check_applicative_mem_pred p (ap : manifest_applicative_pred p) mp := @@ -1345,6 +1352,7 @@ End simpl_mem. (** Qualifiers and keyed predicates. **) +#[universes(template)] Variant qualifier (q : nat) T := Qualifier of predPredType T. Coercion has_quality n T (q : qualifier n T) : pred_class := @@ -1392,9 +1400,11 @@ Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B)) Section KeyPred. Variable T : Type. +#[universes(template)] Variant pred_key (p : predPredType T) := DefaultPredKey. Variable p : predPredType T. +#[universes(template)] Structure keyed_pred (k : pred_key p) := PackKeyedPred {unkey_pred :> pred_class; _ : unkey_pred =i p}. @@ -1426,6 +1436,7 @@ Section KeyedQualifier. Variables (T : Type) (n : nat) (q : qualifier n T). +#[universes(template)] Structure keyed_qualifier (k : pred_key q) := PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}. Definition KeyedQualifier k := PackKeyedQualifier k (erefl q). diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 7596f6638a..4721e19a8b 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -178,6 +178,7 @@ Register abstract_key as plugins.ssreflect.abstract_key. Register abstract as plugins.ssreflect.abstract. (** Constants for tactic-views **) +#[universes(template)] Inductive external_view : Type := tactic_view of Type. (** @@ -206,6 +207,7 @@ Inductive external_view : Type := tactic_view of Type. Module TheCanonical. +#[universes(template)] Variant put vT sT (v1 v2 : vT) (s : sT) := Put. Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s. @@ -301,9 +303,11 @@ Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) We also define a simpler version ("phant" / "Phant") of phantom for the common case where p_type is Type. **) +#[universes(template)] Variant phantom T (p : T) := Phantom. Arguments phantom : clear implicits. Arguments Phantom : clear implicits. +#[universes(template)] Variant phant (p : Type) := Phant. (** Internal tagging used by the implementation of the ssreflect elim. **) @@ -389,6 +393,7 @@ Ltac ssrdone0 := | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. (** To unlock opaque constants. **) +#[universes(template)] Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}. Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed. diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 6535cad8b7..b51ffada0c 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -285,6 +285,7 @@ Lemma unitE : all_equal_to tt. Proof. by case. Qed. (** A generic wrapper type **) +#[universes(template)] Structure wrapped T := Wrap {unwrap : T}. Canonical wrap T x := @Wrap T x. @@ -334,6 +335,7 @@ Section SimplFun. Variables aT rT : Type. +#[universes(template)] Variant simpl_fun := SimplFun of aT -> rT. Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 37c583ab53..257ecd2a85 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -206,7 +206,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let mkabs gen = abs_wgen false (fun x -> x) gen in let mkclr gen clrs = clr_of_wgen gen clrs in let mkpats = function - | _, Some ((x, _), _) -> fun pats -> IPatId (None,hoi_id x) :: pats + | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats | _ -> fun x -> x in let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with | (a, (b, Some ct)) -> @@ -265,7 +265,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = if gens = [] then errorstrm(str"gen have requires some generalizations"); let clear0 = old_cleartac clr0 in let id, name_general_hyp, cleanup, pats = match id, pats with - | None, (IPatId(_, id) as ip)::pats -> Some id, tacipat [ip], clear0, pats + | None, (IPatId id as ip)::pats -> Some id, tacipat [ip], clear0, pats | None, _ -> None, Tacticals.tclIDTAC, clear0, pats | Some (Some id),_ -> Some id, introid id, clear0, pats | Some _,_ -> diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index e71e1bae0d..ce81d83661 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -292,7 +292,7 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl -> | Prefix fix -> Id.to_string fix ^ Id.to_string id | SuffixNum n -> Id.to_string id ^ string_of_int n | SuffixId fix -> Id.to_string id ^ Id.to_string fix in - IPatId (None, Id.of_string s)) seeds in + IPatId (Id.of_string s)) seeds in interp_ipats ipats end end @@ -377,9 +377,8 @@ let rec ipat_tac1 ipat : bool tactic = | IPatDispatch(_,Block id_block) -> tac_intro_seed ipat_tac id_block <*> notTAC - | IPatId (None, id) -> Ssrcommon.tclINTRO_ID id <*> notTAC - | IPatId (Some Dependent, id) -> - intro_anon_deps <*> Ssrcommon.tclINTRO_ID id <*> notTAC + | IPatId id -> Ssrcommon.tclINTRO_ID id <*> notTAC + | IPatFastNondep -> intro_anon_deps <*> notTAC | IPatCase (Block id_block) -> Ssrcommon.tclWITHTOP tac_case <*> tac_intro_seed ipat_tac id_block <*> notTAC @@ -456,7 +455,7 @@ let elaborate_ipats l = | IPatDispatch(s, Regular p) :: rest -> IPatDispatch (s, Regular (List.map elab p)) :: elab rest | IPatCase (Regular p) :: rest -> IPatCase (Regular (List.map elab p)) :: elab rest | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest - | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ | + | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ | IPatFastNondep | IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ | IPatAbstractVars _ | IPatDispatch(_, Block _) | IPatCase(Block _)) as x :: rest -> x :: elab rest in @@ -512,8 +511,7 @@ let mkCoqRefl t c env sigma = let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr = let intro_eq = match eqid with - | Some (IPatId (Some _, _)) -> assert false (* parser *) - | Some (IPatId (None,ipat)) when not is_rec -> + | Some (IPatId ipat) when not is_rec -> let rec intro_eq () = Goal.enter begin fun g -> let sigma, env, concl = Goal.(sigma g, env g, concl g) in match EConstr.kind_of_type sigma concl with @@ -527,7 +525,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr = |_ -> Ssrcommon.errorstrm (Pp.str "Too many names in intro pattern") end in intro_eq () - | Some (IPatId (None,ipat)) -> + | Some (IPatId ipat) -> let intro_lhs = Goal.enter begin fun g -> let sigma = Goal.sigma g in let elim_name = match clr, what with @@ -860,7 +858,7 @@ let ssrabstract dgens = let ipats = List.map (fun (_,cp) -> match id_of_pattern (interp_cpattern gl0 cp None) with | None -> IPatAnon (One None) - | Some id -> IPatId (None,id)) + | Some id -> IPatId id) (List.tl gens) in conclusion ipats end in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 6938bbc9f6..76726009ac 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -605,7 +605,7 @@ let remove_loc x = x.CAst.v let ipat_of_intro_pattern p = Tactypes.( let rec ipat_of_intro_pattern = function - | IntroNaming (IntroIdentifier id) -> IPatId (None,id) + | IntroNaming (IntroIdentifier id) -> IPatId id | IntroAction IntroWildcard -> IPatAnon Drop | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) -> IPatCase (Regular( @@ -629,8 +629,8 @@ let ipat_of_intro_pattern p = Tactypes.( ) let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function - | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x - | IPatId (m,id) -> IPatId (m,map_id id) + | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x + | IPatId id -> IPatId (map_id id) | IPatAbstractVars l -> IPatAbstractVars (List.map map_id l) | IPatClear clr -> IPatClear (List.map map_ssrhyp clr) | IPatCase (Regular iorpat) -> IPatCase (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) @@ -707,7 +707,7 @@ let interp_ipat ist gl = end | x -> x in let rec interp = function - | IPatId(_, id) when ltacvar id -> + | IPatId id when ltacvar id -> ipat_of_intro_pattern (interp_introid ist gl id) | IPatId _ as x -> x | IPatClear clr -> @@ -729,7 +729,7 @@ let interp_ipat ist gl = IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) - | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x + | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x | IPatEqGen _ -> assert false (*internal usage only *) in interp @@ -751,8 +751,8 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } GLOBALIZED BY { intern_ipats } | [ "_" ] -> { [IPatAnon Drop] } | [ "*" ] -> { [IPatAnon All] } - | [ ">" ident(id) ] -> { [IPatId(Some Dependent,id)] } - | [ ident(id) ] -> { [IPatId (None,id)] } + | [ ">" ] -> { [IPatFastNondep] } + | [ ident(id) ] -> { [IPatId id] } | [ "?" ] -> { [IPatAnon (One None)] } | [ "+" ] -> { [IPatAnon Temporary] } | [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] } @@ -1492,7 +1492,7 @@ END { let intro_id_to_binder = List.map (function - | IPatId (None,id) -> + | IPatId id -> let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], @@ -1502,8 +1502,8 @@ let intro_id_to_binder = List.map (function let binder_to_intro_id = CAst.(List.map (function | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } -> - List.map (function {v=Name id} -> IPatId (None,id) | _ -> IPatAnon (One None)) ids - | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId (None,id)] + List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon (One None)) ids + | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id] | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)] | _ -> anomaly "ssrbinder is not a binder")) @@ -1994,7 +1994,7 @@ let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid GRAMMAR EXTEND Gram GLOBAL: ssreqid; ssreqpat: [ - [ id = Prim.ident -> { IPatId (None,id) } + [ id = Prim.ident -> { IPatId id } | "_" -> { IPatAnon Drop } | "?" -> { IPatAnon (One None) } | "+" -> { IPatAnon Temporary } diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 6ccefa1cab..898e03b00e 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -97,8 +97,7 @@ let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c) let rec pr_ipat p = match p with - | IPatId (None,id) -> Id.print id - | IPatId (Some Dependent,id) -> str">" ++ Id.print id + | IPatId id -> Id.print id | IPatSimpl sim -> pr_simpl sim | IPatClear clr -> pr_clear mt clr | IPatCase (Regular iorpat) -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]") @@ -115,6 +114,7 @@ let rec pr_ipat p = | IPatAnon Temporary -> str "+" | IPatNoop -> str "-" | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]" + | IPatFastNondep -> str">" | IPatEqGen _ -> str "<tac>" and pr_ipats ipats = pr_list spc pr_ipat ipats and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8f7e4470f9..c417ef8a66 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -575,7 +575,7 @@ let print_constant with_values sep sp udecl = in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in - hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++ + hov 0 ( match val_0 with | None -> str"*** [ " ++ diff --git a/printing/printer.ml b/printing/printer.ml index be0139da06..3f7837fd6e 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -982,14 +982,6 @@ let pr_assumptionset env sigma s = ] in prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums) -let pr_cumulative poly cum = - if poly then - if cum then str "Cumulative " else str "NonCumulative " - else mt () - -let pr_polymorphic b = - if b then str"Polymorphic " else str"Monomorphic " - (* print the proof step, possibly with diffs highlighted, *) let print_and_diff oldp newp = match newp with diff --git a/printing/printer.mli b/printing/printer.mli index fd4682a086..9a06d555e4 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -81,8 +81,6 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t (** Universe constraints *) -val pr_polymorphic : bool -> Pp.t -val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> diff --git a/printing/printmod.ml b/printing/printmod.ml index a8d7b0c1a8..898f231a8b 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -123,11 +123,7 @@ let print_mutual_inductive env mind mib udecl = (Declareops.inductive_polymorphic_context mib) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in - hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ - Printer.pr_cumulative - (Declareops.inductive_is_polymorphic mib) - (Declareops.inductive_is_cumulative mib) ++ - def keyword ++ spc () ++ + hov 0 (def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env sigma mib) inds ++ match mib.mind_universes with @@ -172,10 +168,6 @@ let print_record env mind mib udecl = in hov 0 ( hov 0 ( - Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ - Printer.pr_cumulative - (Declareops.inductive_is_polymorphic mib) - (Declareops.inductive_is_cumulative mib) ++ def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ diff --git a/test-suite/bugs/opened/bug_4781.v b/test-suite/bugs/closed/bug_4781.v index 8b651ac22e..464a3de1b3 100644 --- a/test-suite/bugs/opened/bug_4781.v +++ b/test-suite/bugs/closed/bug_4781.v @@ -25,29 +25,29 @@ Goal True. let x := match constr:(Set) with ?y => constr:(y) end in pose x. (* This fails with an error: *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := match constr:(x) with ?y => constr:(y) end in pose x. (* The command has indeed failed with message: Error: Variable y should be bound to a term. *) (* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := match constr:(x) with ?y => y end in pose x. - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := (eval cbv iota in x) in pose x. - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := type of x in pose x. (* should succeed *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:(_ : abstract_term term) in let x := type of x in @@ -70,7 +70,7 @@ Even stranger, consider:*) (*This works fine. But if I change the period to a semicolon, I get:*) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let y := (eval cbv iota in (let v : T := x in v)) in @@ -82,7 +82,7 @@ Even stranger, consider:*) (* should succeed *) (*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let y := (eval cbv iota in (let v : T := x in v)) in @@ -92,3 +92,5 @@ Even stranger, consider:*) let x := (eval cbv delta [x'] in x') in let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *) idtac. (* should succeed *) + exact I. +Qed. diff --git a/test-suite/bugs/closed/bug_7904.v b/test-suite/bugs/closed/bug_7904.v new file mode 100644 index 0000000000..1e518e2adf --- /dev/null +++ b/test-suite/bugs/closed/bug_7904.v @@ -0,0 +1,13 @@ + + +Class abstract_term {T} (x : T) := by_abstract_term : T. +Hint Extern 0 (@abstract_term ?T ?x) => change T; abstract (exact x) : typeclass_instances. + +Goal True. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => y end in + pose x as v. (* was Error: Variable x should be bound to a term but is bound to a constr. *) + exact v. +Qed. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index b071da86c9..583ea0cb43 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ eq_refl : ?y = ?y where ?y : [ |- nat] -Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y For eq: Argument A is implicit and maximally inserted @@ -31,8 +31,7 @@ When applied to 1 argument: Argument B is implicit Argument scopes are [type_scope _] Expands to: Constructor Coq.Init.Logic.eq_refl -Monomorphic Inductive myEq (B : Type) (x : A) : A -> Prop := - myrefl : B -> myEq B x x +Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x For myrefl: Arguments are renamed to C, x, _ For myrefl: Argument C is implicit and maximally inserted @@ -45,7 +44,7 @@ Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] Expands to: Constructor Arguments_renaming.Test1.myrefl -Monomorphic myplus = +myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with | 0 => m @@ -69,7 +68,7 @@ myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat -Monomorphic Inductive myEq (A B : Type) (x : A) : A -> Prop := +Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x For myrefl: Arguments are renamed to A, C, x, _ @@ -85,7 +84,7 @@ Argument scopes are [type_scope type_scope _ _] Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x -Monomorphic myplus = +myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with | 0 => m diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out index 9c46ace463..6e27837b26 100644 --- a/test-suite/output/Binder.out +++ b/test-suite/output/Binder.out @@ -1,10 +1,10 @@ -Monomorphic foo = fun '(x, y) => x + y +foo = fun '(x, y) => x + y : nat * nat -> nat foo is not universe polymorphic forall '(a, b), a /\ b : Prop -Monomorphic foo = λ '(x, y), x + y +foo = λ '(x, y), x + y : nat * nat → nat foo is not universe polymorphic diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 0a02c5a7dd..efcc299e82 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -1,4 +1,4 @@ -Monomorphic t_rect = +t_rect = fun (P : t -> Type) (f : 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 @@ -17,7 +17,7 @@ Argument scopes are [function_scope function_scope _] | {| f3 := b |} => b end : TT -> 0 = 0 -Monomorphic proj = +proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match Nat.eq_dec x y with | left eqprf => match eqprf in (_ = z) return (P z) with @@ -29,7 +29,7 @@ end proj is not universe polymorphic Argument scopes are [nat_scope nat_scope function_scope _ _] -Monomorphic foo = +foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with | nil => None @@ -40,7 +40,7 @@ fix foo (A : Type) (l : list A) {struct l} : option A := foo is not universe polymorphic Argument scopes are [type_scope list_scope] -Monomorphic uncast = +uncast = fun (A : Type) (x : I A) => match x with | x0 <: _ => x0 end @@ -48,11 +48,11 @@ fun (A : Type) (x : I A) => match x with uncast is not universe polymorphic Argument scopes are [type_scope _] -Monomorphic foo' = if A 0 then true else false +foo' = if A 0 then true else false : bool foo' is not universe polymorphic -Monomorphic f = +f = fun H : B => match H with | AC x => @@ -83,18 +83,18 @@ fun '(D n m p q) => n + m + p + q : J -> nat The command has indeed failed with message: The constructor D (in type J) expects 3 arguments. -Monomorphic lem1 = +lem1 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k lem1 is not universe polymorphic -Monomorphic lem2 = +lem2 = fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl : forall k : bool, k = k lem2 is not universe polymorphic Argument scope is [bool_scope] -Monomorphic lem3 = +lem3 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 43718a0f07..4e949dcb04 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -43,6 +43,7 @@ Print foo. (* Accept and use notation with binded parameters *) +#[universes(template)] Inductive I (A: Type) : Type := C : A -> I A. Notation "x <: T" := (C T x) (at level 38). @@ -83,6 +84,7 @@ Print f. (* Was enhancement request #5142 (error message reported on the most general return clause heuristic) *) +#[universes(template)] Inductive gadt : Type -> Type := | gadtNat : nat -> gadt nat | gadtTy : forall T, T -> gadt T. diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index 0e84bf3966..6976f35a88 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -1,7 +1,7 @@ (* Submitted by Randy Pollack *) -Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. -Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. +#[universes(template)] Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +#[universes(template)] Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. Section testSection. Variables (S : Set) (P : pred S) (R : rel S) (x : S). diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index 1ecd9771eb..f9398fdca9 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -101,7 +101,7 @@ Section decoder_result. Variable inst : Type. - Inductive decoder_result : Type := + #[universes(template)] Inductive decoder_result : Type := | DecUndefined : decoder_result | DecUnpredictable : decoder_result | DecInst : inst -> decoder_result diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 61ae4edbd1..9b25c2dbd3 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). omega. Qed. -CoInductive Inf := S { projS : Inf }. +#[universes(template)] CoInductive Inf := S { projS : Inf }. Definition expand_Inf (x : Inf) := S (projS x). CoFixpoint inf := S inf. Eval compute in inf. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 71c7070f2b..0b0f501f9a 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -2,8 +2,7 @@ compose (C:=nat) S : (nat -> nat) -> nat -> nat ex_intro (P:=fun _ : nat => True) (x:=0) I : ex (fun _ : nat => True) -Monomorphic d2 = -fun x : nat => d1 (y:=x) +d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x d2 is not universe polymorphic diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 5a548cfae4..2ba02924c9 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,8 +1,7 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)". -Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop := - Foo : foo A x +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x For foo: Argument scopes are [type_scope _] For Foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 8ff91268a6..9eec9a7dad 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -3,5 +3,5 @@ Fail Inductive list' (A:Set) : Set := | cons' : A -> list' A -> list' (A*A). (* Check printing of let-ins *) -Inductive foo (A : Type) (x : A) (y := x) := Foo. +#[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo. Print foo. diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 4743fb0d0a..c17c63e724 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,4 +1,4 @@ -Monomorphic Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := +Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} For sig2: Argument A is implicit diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out index f84cedfa62..ebbd5d422b 100644 --- a/test-suite/output/Load.out +++ b/test-suite/output/Load.out @@ -1,8 +1,8 @@ -Monomorphic f = 2 +f = 2 : nat f is not universe polymorphic -Monomorphic u = I +u = I : True u is not universe polymorphic diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index f53313def9..71d92482d0 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -225,7 +225,7 @@ fun S : nat => [[S | S + S]] : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop -Monomorphic foo = +foo = fun l : list nat => match l with | _ :: (_ :: _) as l1 => l1 | _ => l @@ -261,11 +261,11 @@ myfoo01 tt {4; 5; 6}; {7; 8; 9}] : list (list nat) -Monomorphic amatch = mmatch 0 (with 0 => 1| 1 => 2 end) +amatch = mmatch 0 (with 0 => 1| 1 => 2 end) : unit amatch is not universe polymorphic -Monomorphic alist = [0; 1; 2] +alist = [0; 1; 2] : list nat alist is not universe polymorphic diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 15211f1233..2caffad1d9 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). (**********************************************************************) (* Test printing of #4932 *) -Inductive ftele : Type := +#[universes(template)] Inductive ftele : Type := | fb {T:Type} : T -> ftele | fr {T} : (T -> ftele) -> ftele. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index bfeff20524..bdbc5a5960 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -1,4 +1,4 @@ -Monomorphic swap = fun '(x, y) => (y, x) +swap = fun '(x, y) => (y, x) : A * B -> B * A swap is not universe polymorphic @@ -6,22 +6,20 @@ fun '(x, y) => (y, x) : A * B -> B * A forall '(x, y), swap (x, y) = (y, x) : Prop -Monomorphic proj_informative = -fun '(exist _ x _) => x : A +proj_informative = fun '(exist _ x _) => x : A : {x : A | P x} -> A proj_informative is not universe polymorphic -Monomorphic foo = -fun '(Bar n b tt p) => if b then n + p else n - p +foo = fun '(Bar n b tt p) => if b then n + p else n - p : Foo -> nat foo is not universe polymorphic -Monomorphic baz = +baz = fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1 : Foo -> Foo -> nat baz is not universe polymorphic -Monomorphic swap = +swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A @@ -40,7 +38,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) : A * B → B * A ∀ '(x, y), swap (x, y) = (y, x) : Prop -Monomorphic both_z = +both_z = fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat @@ -52,7 +50,7 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop fun (pat : nat) '(x, y) => x + y = pat : nat -> nat * nat -> Prop -Monomorphic f = fun x : nat => x + x +f = fun x : nat => x + x : nat -> nat f is not universe polymorphic diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index d671053c07..0c1b08f5a3 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -53,7 +53,7 @@ Module Suboptimal. (** This test shows an example which exposes the [let] introduced by the pattern notation in binders. *) -Inductive Fin (n:nat) := Z : Fin n. +#[universes(template)] Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index be793dd453..da1fca7134 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -4,7 +4,7 @@ existT is template universe polymorphic Argument A is implicit Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT -Monomorphic Inductive sigT (A : Type) (P : A -> Type) : Type := +Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} For sigT: Argument A is implicit @@ -14,7 +14,7 @@ For existT: Argument scopes are [type_scope function_scope _ _] existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit -Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted For eq_refl, when applied to no arguments: @@ -38,7 +38,7 @@ When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: Argument A is implicit -Monomorphic Nat.add = +Nat.add = fix add (n m : nat) {struct n} : nat := match n with | 0 => m @@ -62,7 +62,7 @@ plus_n_O is not universe polymorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O -Monomorphic Inductive le (n : nat) : nat -> Prop := +Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m For le_S: Argument m is implicit @@ -74,7 +74,7 @@ comparison : Set comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison -Monomorphic Inductive comparison : Set := +Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo @@ -84,7 +84,7 @@ bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted Expands to: Constant PrintInfos.bar -Monomorphic *** [ bar : foo ] +*** [ bar : foo ] bar is not universe polymorphic Expanded type for implicit arguments @@ -94,7 +94,7 @@ Argument x is implicit and maximally inserted Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq -Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted For eq_refl, when applied to no arguments: diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v index 098a518dc4..2713e6a188 100644 --- a/test-suite/output/Projections.v +++ b/test-suite/output/Projections.v @@ -5,7 +5,7 @@ Class HostFunction := host_func : Type. Section store. Context `{HostFunction}. - Record store := { store_funcs : host_func }. + #[universes(template)] Record store := { store_funcs : host_func }. End store. Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index d9a649fadc..4fe7b051f8 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -20,12 +20,12 @@ Check {| field := 5 |}. Check build_r 5. Check build_c 5. -Record N := C { T : Type; _ : True }. +#[universes(template)] Record N := C { T : Type; _ : True }. Check fun x:N => let 'C _ p := x in p. Check fun x:N => let 'C T _ := x in T. Check fun x:N => let 'C T p := x in (T,p). -Record M := D { U : Type; a := 0; q : True }. +#[universes(template)] Record M := D { U : Type; a := 0; q : True }. Check fun x:M => let 'D T _ p := x in p. Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v index 9cf6ad35b8..99183f2064 100644 --- a/test-suite/output/ShowMatch.v +++ b/test-suite/output/ShowMatch.v @@ -3,12 +3,12 @@ *) Module A. - Inductive foo := f. + #[universes(template)] Inductive foo := f. Show Match foo. (* no need to disambiguate *) End A. Module B. - Inductive foo := f. + #[universes(template)] Inductive foo := f. (* local foo shadows A.foo, so constructor "f" needs disambiguation *) Show Match A.foo. End B. diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index bbc936766d..c7e6ef950e 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -1,4 +1,4 @@ -Monomorphic byte_rect = +byte_rect = fun (P : byte -> Type) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") @@ -435,7 +435,7 @@ end byte_rect is not universe polymorphic Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] -Monomorphic byte_rec = +byte_rec = fun P : byte -> Set => byte_rect P : forall P : byte -> Set, P "000" -> @@ -610,7 +610,7 @@ fun P : byte -> Set => byte_rect P byte_rec is not universe polymorphic Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] -Monomorphic byte_ind = +byte_ind = fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index f080f6d0f0..67b65d4b81 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,15 +1,15 @@ -Monomorphic TrM.A = M.A +TrM.A = M.A : Set TrM.A is not universe polymorphic -Monomorphic OpM.A = M.A +OpM.A = M.A : Set OpM.A is not universe polymorphic -Monomorphic TrM.B = M.B +TrM.B = M.B : Set TrM.B is not universe polymorphic -Monomorphic *** [ OpM.B : Set ] +*** [ OpM.B : Set ] OpM.B is not universe polymorphic diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 4d3f7419e6..0bd6ade690 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,37 +1,34 @@ -Polymorphic NonCumulative Inductive Empty@{u} : Type@{u} := -Polymorphic NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap - { punwrap : A } +Inductive Empty@{u} : Type@{u} := +Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] For pwrap: Argument scopes are [type_scope _] -Polymorphic punwrap@{u} = +punwrap@{u} = fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) punwrap is universe polymorphic Argument scopes are [type_scope _] -Polymorphic NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap - { runwrap : A } +Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } For RWrap: Argument scope is [type_scope] For rwrap: Argument scopes are [type_scope _] -Polymorphic runwrap@{u} = +runwrap@{u} = fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap : forall A : Type@{u}, RWrap@{u} A -> A (* u |= *) runwrap is universe polymorphic Argument scopes are [type_scope _] -Polymorphic Wrap@{u} = -fun A : Type@{u} => A +Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) Wrap is universe polymorphic Argument scope is [type_scope] -Polymorphic wrap@{u} = +wrap@{u} = fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) @@ -39,12 +36,12 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap wrap is universe polymorphic Arguments A, Wrap are implicit and maximally inserted Argument scopes are [type_scope _] -Polymorphic bar@{u} = nat +bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) bar is universe polymorphic -Polymorphic foo@{u UnivBinders.17 v} = +foo@{u UnivBinders.17 v} = Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) @@ -56,7 +53,7 @@ Type@{i} -> Type@{j} = Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) -Monomorphic mono = Type@{mono.u} +mono = Type@{mono.u} : Type@{mono.u+1} (* {mono.u} |= *) @@ -77,7 +74,7 @@ mono : Type@{mono.u+1} The command has indeed failed with message: Universe u already exists. -Monomorphic bobmorane = +bobmorane = let tt := Type@{UnivBinders.32} in let ff := Type@{UnivBinders.34} in tt -> ff : Type@{max(UnivBinders.31,UnivBinders.33)} @@ -85,21 +82,20 @@ let ff := Type@{UnivBinders.34} in tt -> ff bobmorane is not universe polymorphic The command has indeed failed with message: Universe u already bound. -Polymorphic foo@{E M N} = +foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1,M+1,N+1)} (* E M N |= *) foo is universe polymorphic -Polymorphic foo@{u UnivBinders.17 v} = +foo@{u UnivBinders.17 v} = Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) foo is universe polymorphic -Polymorphic NonCumulative Inductive Empty@{E} : Type@{E} := -Polymorphic NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap - { punwrap : A } +Inductive Empty@{E} : Type@{E} := +Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] @@ -119,58 +115,55 @@ The command has indeed failed with message: This object does not support universe names. The command has indeed failed with message: Cannot enforce v < u because u < gU < gV < v -Monomorphic bind_univs.mono = +bind_univs.mono = Type@{bind_univs.mono.u} : Type@{bind_univs.mono.u+1} (* {bind_univs.mono.u} |= *) bind_univs.mono is not universe polymorphic -Polymorphic bind_univs.poly@{u} = Type@{u} +bind_univs.poly@{u} = Type@{u} : Type@{u+1} (* u |= *) bind_univs.poly is universe polymorphic -Polymorphic insec@{v} = -Type@{u} -> Type@{v} +insec@{v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* v |= *) insec is universe polymorphic -Polymorphic NonCumulative Inductive insecind@{k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{k} +Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} For inseccstr: Argument scope is [type_scope] -Polymorphic insec@{u v} = -Type@{u} -> Type@{v} +insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) insec is universe polymorphic -Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} := +Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} For inseccstr: Argument scope is [type_scope] -Polymorphic insec2@{u} = Prop +insec2@{u} = Prop : Type@{Set+1} (* u |= *) insec2 is universe polymorphic -Polymorphic inmod@{u} = Type@{u} +inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) inmod is universe polymorphic -Polymorphic SomeMod.inmod@{u} = Type@{u} +SomeMod.inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) SomeMod.inmod is universe polymorphic -Polymorphic inmod@{u} = Type@{u} +inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) inmod is universe polymorphic -Polymorphic Applied.infunct@{u v} = +Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v index 7465442cab..0eb5db1733 100644 --- a/test-suite/output/Warnings.v +++ b/test-suite/output/Warnings.v @@ -1,5 +1,5 @@ (* Term in warning was not printed in the right environment at some time *) -Record A := { B:Type; b:B->B }. +#[universes(template)] Record A := { B:Type; b:B->B }. Definition a B := {| B:=B; b:=fun x => x |}. Canonical Structure a. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 3dad2360c4..20568f742a 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -1,8 +1,8 @@ -Monomorphic Nat.t = nat +Nat.t = nat : Set Nat.t is not universe polymorphic -Monomorphic Nat.t = nat +Nat.t = nat : Set Nat.t is not universe polymorphic diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index a1326596bb..f545ca679c 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -1,4 +1,4 @@ -Monomorphic P = +P = fun e : option L => match e with | Some cl => Some cl | None => None diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 57a4739e9f..209fedc343 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -21,6 +21,6 @@ Print P. (* Note: exact numbers of evars are not important... *) -Inductive T (n:nat) : Type := A : T n. +#[universes(template)] Inductive T (n:nat) : Type := A : T n. Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/report.sh b/test-suite/report.sh index c5e698232f..cef615266b 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -15,7 +15,7 @@ mkdir "$SAVEDIR" FAILMARK="==========> FAILURE <==========" FAILED=$(mktemp /tmp/coq-check-XXXXXX) -find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" +find . '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" cp summary.log "$SAVEDIR"/ diff --git a/test-suite/ssr/ipat_fast_any.v b/test-suite/ssr/ipat_fast_any.v new file mode 100644 index 0000000000..a50984c7c0 --- /dev/null +++ b/test-suite/ssr/ipat_fast_any.v @@ -0,0 +1,21 @@ +Require Import ssreflect. + +Goal forall y x : nat, x = y -> x = x. +Proof. +move=> + > ->. match goal with |- forall y, y = y => by [] end. +Qed. + +Goal forall y x : nat, le x y -> x = y. +Proof. +move=> > [|]. + by []. +match goal with |- forall a, _ <= a -> _ = S a => admit end. +Admitted. + +Goal forall y x : nat, le x y -> x = y. +Proof. +move=> y x. +case E: x => >. + admit. +match goal with |- S _ <= y -> S _ = y => admit end. +Admitted. diff --git a/test-suite/ssr/ipat_fastid.v b/test-suite/ssr/ipat_fastid.v index 8dc0c6cf0b..b0985a0d2f 100644 --- a/test-suite/ssr/ipat_fastid.v +++ b/test-suite/ssr/ipat_fastid.v @@ -11,6 +11,15 @@ lazymatch goal with end. Qed. +Lemma simple2 : + forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True. +Proof. +move=> >; move=>x_ge_3; move=> >; move=>xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + Definition stuff x := 3 <= x -> forall y, odd (y+x) -> x = y -> True. @@ -22,6 +31,14 @@ lazymatch goal with end. Qed. +Lemma harder2 : forall x, stuff x. +Proof. +move=> >; move=>x_ge_3;move=> >; move=>xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + Lemma homotop : forall x : nat, forall e : x = x, e = e -> True. Proof. move=> >eq_ee. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 86a3a88be9..4b97d75cea 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -283,6 +283,7 @@ Local Open Scope list_scope. (** A compact representation of non-dependent arities, with the codomain singled-out. *) (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *) +#[universes(template)] Inductive Tlist : Type := Tnil : Tlist | Tcons : Type -> Tlist -> Tlist. Local Infix "::" := Tcons. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 2673a11917..e6968bd6c2 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -27,6 +27,7 @@ Require Export Coq.Classes.Morphisms. (** A setoid wraps an equivalence. *) +#[universes(template)] Class Setoid A := { equiv : relation A ; setoid_equiv :> Equivalence equiv }. @@ -128,6 +129,7 @@ Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper ( (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *) +#[universes(template)] Class PartialSetoid (A : Type) := { pequiv : relation A ; pequiv_prf :> PER pequiv }. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 8fc04d81e6..9a815d2a7e 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -53,6 +53,7 @@ Variable elt : Type. The fifth field of [Node] is the height of the tree *) +#[universes(template)] Inductive tree := | Leaf : tree | Node : tree -> key -> elt -> tree -> int -> tree. @@ -235,6 +236,7 @@ Fixpoint join l : key -> elt -> t -> t := - [o] is the result of [find x m]. *) +#[universes(template)] Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }. Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). @@ -291,6 +293,7 @@ Variable cmp : elt->elt->bool. (** ** Enumeration of the elements of a tree *) +#[universes(template)] Inductive enumeration := | End : enumeration | More : key -> elt -> t -> enumeration -> enumeration. @@ -1817,6 +1820,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Module Raw := Raw I X. Import Raw.Proofs. + #[universes(template)] Record bst (elt:Type) := Bst {this :> Raw.tree elt; is_bst : Raw.bst this}. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 950b30ee4d..7bc9edff8d 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -451,6 +451,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Import Raw. Import Raw.Proofs. + #[universes(template)] Record bbst (elt:Type) := Bbst {this :> tree elt; is_bst : bst this; is_avl: avl this}. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 6ca158a277..4febd64842 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -1024,6 +1024,7 @@ Module E := X. Definition key := E.t. +#[universes(template)] Record slist (elt:Type) := {this :> Raw.t elt; sorted : sort (@Raw.PX.ltk elt) this}. Definition t (elt:Type) : Type := slist elt. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 0fc68b1433..b47c99244b 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -73,6 +73,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Definition key := positive : Type. + #[universes(template)] Inductive tree (A : Type) := | Leaf : tree A | Node : tree A -> option A -> tree A -> tree A. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 03dce9666d..a923f4e6f9 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -869,6 +869,7 @@ Module Make (X: DecidableType) <: WS with Module E:=X. Module E := X. Definition key := E.t. +#[universes(template)] Record slist (elt:Type) := {this :> Raw.t elt; NoDup : NoDupA (@Raw.PX.eqk elt) this}. Definition t (elt:Type) := slist elt. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 7f0387dd12..3603604a71 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -167,6 +167,7 @@ Register S as num.nat.S. (** [option A] is the extension of [A] with an extra element [None] *) +#[universes(template)] Inductive option (A:Type) : Type := | Some : A -> option A | None : option A. @@ -186,6 +187,7 @@ Definition option_map (A B:Type) (f:A->B) (o : option A) : option B := (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) +#[universes(template)] Inductive sum (A B:Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. @@ -198,6 +200,7 @@ Arguments inr {A B} _ , A [B] _. (** [prod A B], written [A * B], is the product of [A] and [B]; the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) +#[universes(template)] Inductive prod (A B:Type) : Type := pair : A -> B -> A * B @@ -256,6 +259,7 @@ Defined. (** Polymorphic lists and some operations *) +#[universes(template)] Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. @@ -384,6 +388,7 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined. member is the singleton datatype [identity A a a] whose sole inhabitant is denoted [identity_refl A a] *) +#[universes(template)] Inductive identity (A:Type) (a:A) : A -> Type := identity_refl : identity a a. Hint Resolve identity_refl: core. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index e4796a8059..cfba2bae69 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -24,6 +24,7 @@ Require Import Logic. Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset of elements of the type [A] which satisfy both [P] and [Q]. *) +#[universes(template)] Inductive sig (A:Type) (P:A -> Prop) : Type := exist : forall x:A, P x -> sig P. @@ -31,12 +32,14 @@ Register sig as core.sig.type. Register exist as core.sig.intro. Register sig_rect as core.sig.rect. +#[universes(template)] Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := exist2 : forall x:A, P x -> Q x -> sig2 P Q. (** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) +#[universes(template)] Inductive sigT (A:Type) (P:A -> Type) : Type := existT : forall x:A, P x -> sigT P. @@ -44,6 +47,7 @@ Register sigT as core.sigT.type. Register existT as core.sigT.intro. Register sigT_rect as core.sigT.rect. +#[universes(template)] Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := existT2 : forall x:A, P x -> Q x -> sigT2 P Q. @@ -700,6 +704,7 @@ Register sumbool as core.sumbool.type. (** [sumor] is an option type equipped with the justification of why it may not be a regular value *) +#[universes(template)] Inductive sumor (A:Type) (B:Prop) : Type := | inleft : A -> A + {B} | inright : B -> A + {B} diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index 57f558de50..d93816e9ff 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -78,6 +78,7 @@ Section DependentMemoFunction. Variable A: nat -> Type. Variable f: forall n, A n. +#[universes(template)] Inductive memo_val: Type := memo_mval: forall n, A n -> memo_val. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 8a01b8fb19..a03799959e 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -16,6 +16,7 @@ Section Streams. Variable A : Type. +#[universes(template)] CoInductive Stream : Type := Cons : A -> Stream -> Stream. diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v index 02c8998a8d..a70bd92329 100644 --- a/theories/Logic/ExtensionalityFacts.v +++ b/theories/Logic/ExtensionalityFacts.v @@ -40,6 +40,7 @@ Definition is_inverse A B f g := (forall a:A, g (f a) = a) /\ (forall b:B, f (g (** The diagonal over A and the one-one correspondence with A *) +#[universes(template)] Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }. Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}. diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index ac2a143472..13e1dad361 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -208,6 +208,7 @@ Definition concat s1 s2 := - [present] is [true] if and only if [s] contains [x]. *) +#[universes(template)] Record triple := mktriple { t_left:t; t_in:bool; t_right:t }. Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 888f9850c1..a3dcca7dfd 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -48,6 +48,7 @@ Module Type Ops (X:OrderedType)(Info:InfoTyp). Definition elt := X.t. Hint Transparent elt : core. +#[universes(template)] Inductive tree : Type := | Leaf : tree | Node : Info.t -> tree -> X.t -> tree -> tree. @@ -167,6 +168,7 @@ end. (** Enumeration of the elements of a tree. This corresponds to the "samefringe" notion in the litterature. *) +#[universes(template)] Inductive enumeration := | End : enumeration | More : elt -> tree -> enumeration -> enumeration. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index a4bbaef52d..0ba2799bfb 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -439,6 +439,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E. Definition elt := E.t. +#[universes(template)] Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}. Definition t := t_. Arguments Mkt this {is_ok}. diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 951a4ef2b0..9f718cba65 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -28,6 +28,7 @@ Local Open Scope Z_scope. Module ZnZ. + #[universes(template)] Class Ops (t:Type) := MkOps { (* Conversion functions with Z *) diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v index fe0476e4de..b6441bb76a 100644 --- a/theories/Numbers/Cyclic/Abstract/DoubleType.v +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -22,6 +22,7 @@ Section Carry. Variable A : Type. + #[universes(template)] Inductive carry := | C0 : A -> carry | C1 : A -> carry. @@ -44,6 +45,7 @@ Section Zn2Z. first. *) + #[universes(template)] Inductive zn2z := | W0 : zn2z | WW : znz -> znz -> zn2z. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index cf42ed18db..5ae933d433 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -257,6 +257,7 @@ Ltac blocked t := block_goal ; t ; unblock_goal. be used by the [equations] resolver. It is especially useful to register the dependent elimination principles for things in [Prop] which are not automatically generated. *) +#[universes(template)] Class DependentEliminationPackage (A : Type) := { elim_type : Type ; elim : elim_type }. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index ceac021ef2..49a485c741 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -137,6 +137,7 @@ Definition IsStepFun (f:R -> R) (a b:R) : Type := { l:Rlist & is_subdivision f a b l }. (** ** Class of step functions *) +#[universes(template)] Record StepFun (a b:R) : Type := mkStepFun {fe :> R -> R; pre : IsStepFun fe a b}. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index e3e995d201..b6b72de889 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -116,6 +116,7 @@ Qed. (*******************************) (*********) +#[universes(template)] Record Metric_Space : Type := {Base : Type; dist : Base -> Base -> R; diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 171dba5522..f94b5cab65 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -380,6 +380,7 @@ Proof. apply Rinv_0_lt_compat; prove_sup0. Qed. +#[universes(template)] Record family : Type := mkfamily {ind : R -> Prop; f :> R -> R -> Prop; diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 61fe55770b..2ed422ffe9 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -100,9 +100,11 @@ Hint Resolve Totally_ordered_definition Upper_Bound_definition Section Specific_orders. Variable U : Type. + #[universes(template)] Record Cpo : Type := Definition_of_cpo {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}. + #[universes(template)] Record Chain : Type := Definition_of_chain {PO_of_chain : PO U; Chain_cond : Totally_ordered U PO_of_chain (@Carrier_of _ PO_of_chain)}. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index a79ddead20..6a8a3014c3 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -22,6 +22,7 @@ Section multiset_defs. Hypothesis eqA_equiv : Equivalence eqA. Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. + #[universes(template)] Inductive multiset : Type := Bag : (A -> nat) -> multiset. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 17fc0ed25e..5b51c7b953 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -36,6 +36,7 @@ Section Partial_orders. Definition Rel := Relation U. + #[universes(template)] Record PO : Type := Definition_of_PO { Carrier_of : Ensemble U; Rel_of : Relation U; diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 6a22501afa..f5cda792ce 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -42,6 +42,7 @@ Section defs. Let emptyBag := EmptyBag A. Let singletonBag := SingletonBag _ eqA_dec. + #[universes(template)] Inductive Tree := | Tree_Leaf : Tree | Tree_Node : A -> Tree -> Tree -> Tree. @@ -128,6 +129,7 @@ Section defs. (** ** Merging two sorted lists *) + #[universes(template)] Inductive merge_lem (l1 l2:list A) : Type := merge_exist : forall l:list A, @@ -201,6 +203,7 @@ Section defs. (** ** Specification of heap insertion *) + #[universes(template)] Inductive insert_spec (a:A) (T:Tree) : Type := insert_exist : forall T1:Tree, @@ -234,6 +237,7 @@ Section defs. (** ** Building a heap from a list *) + #[universes(template)] Inductive build_heap (l:list A) : Type := heap_exist : forall T:Tree, @@ -258,6 +262,7 @@ Section defs. (** ** Building the sorted list *) + #[universes(template)] Inductive flat_spec (T:Tree) : Type := flat_exist : forall l:list A, diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 7f96aa6b87..906cf79ca9 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -28,6 +28,7 @@ Local Open Scope nat_scope. (** A vector is a list of size n whose elements belong to a set A. *) +#[universes(template)] Inductive t A : nat -> Type := |nil : t A 0 |cons : forall (h:A) (n:nat), t A n -> t A (S n). diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index fd363d02ca..cf46657d36 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -18,6 +18,7 @@ Section WellOrdering. Variable A : Type. Variable B : A -> Type. + #[universes(template)] Inductive WO : Type := sup : forall (a:A) (f:B a -> WO), WO. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 1e35370d29..0b0ed48d51 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -212,6 +212,7 @@ Module MoreInt (Import I:Int). | EZofI : ExprI -> ExprZ | EZraw : Z -> ExprZ. + #[universes(template)] Inductive ExprP : Type := | EPeq : ExprZ -> ExprZ -> ExprP | EPlt : ExprZ -> ExprZ -> ExprP diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 4af6415a4d..348e76da62 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -34,6 +34,13 @@ module RelDecl = Context.Rel.Declaration (* 3b| Mutual inductive definitions *) +let warn_auto_template = + CWarnings.create ~name:"auto-template" ~category:"vernacular" + (fun id -> + Pp.(strbrk "Automatically declaring " ++ Id.print id ++ + strbrk " as template polymorphic. Use attributes or " ++ + strbrk "disable Auto Template Polymorphism to avoid this warning.")) + let should_auto_template = let open Goptions in let auto = ref true in @@ -44,7 +51,10 @@ let should_auto_template = optread = (fun () -> !auto); optwrite = (fun b -> auto := b); } in - fun () -> !auto + fun id would_auto -> + let b = !auto && would_auto in + if b then warn_auto_template id; + b let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c) @@ -431,8 +441,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); template | None -> - should_auto_template () && not poly && - Option.cata (fun s -> not (Sorts.is_small s)) false concl + should_auto_template ind.ind_name (not poly && + Option.cata (fun s -> not (Sorts.is_small s)) false concl) in { mind_entry_typename = ind.ind_name; mind_entry_arity = arity; diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 9df8f7c341..1d6f652385 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -46,7 +46,10 @@ val declare_mutual_inductive_with_eliminations : mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> MutInd.t -val should_auto_template : unit -> bool +val should_auto_template : Id.t -> bool -> bool +(** [should_auto_template x b] is [true] when [b] is [true] and we + automatically use template polymorphism. [x] is the name of the + inductive under consideration. *) (** Exported for Funind *) diff --git a/vernac/record.ml b/vernac/record.ml index ffd4f654c6..2867ad1437 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -415,9 +415,9 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St template | None, template -> (* auto detect template *) - ComInductive.should_auto_template () && template && not poly && + ComInductive.should_auto_template id (template && not poly && let _, s = Reduction.dest_arity (Global.env()) arity in - not (Sorts.is_small s) + not (Sorts.is_small s)) in { mind_entry_typename = id; mind_entry_arity = arity; |