aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test-suite/bugs/closed/bug_3513.v2
-rw-r--r--test-suite/bugs/closed/bug_4095.v2
-rw-r--r--test-suite/bugs/closed/bug_6042.v7
-rw-r--r--theories/Classes/CMorphisms.v22
-rw-r--r--theories/Classes/Morphisms.v16
-rw-r--r--theories/Classes/Morphisms_Relations.v8
-rw-r--r--theories/Classes/RelationClasses.v6
-rw-r--r--theories/Classes/RelationPairs.v14
-rw-r--r--vernac/classes.ml25
9 files changed, 57 insertions, 45 deletions
diff --git a/test-suite/bugs/closed/bug_3513.v b/test-suite/bugs/closed/bug_3513.v
index 462a615d91..f3a19c2b89 100644
--- a/test-suite/bugs/closed/bug_3513.v
+++ b/test-suite/bugs/closed/bug_3513.v
@@ -13,7 +13,7 @@ Infix "|--" := lentails (at level 79, no associativity).
Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
Infix "-|-" := lequiv (at level 85, no associativity).
-Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.
Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
Section ILogic_Fun.
Context (T: Type) `{TType: type T}.
diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v
index d667022e68..2d4d7d02cc 100644
--- a/test-suite/bugs/closed/bug_4095.v
+++ b/test-suite/bugs/closed/bug_4095.v
@@ -15,7 +15,7 @@ Infix "|--" := lentails (at level 79, no associativity).
Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
Infix "-|-" := lequiv (at level 85, no associativity).
-Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.
Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
Section ILogic_Fun.
Context (T: Type) `{TType: type T}.
diff --git a/test-suite/bugs/closed/bug_6042.v b/test-suite/bugs/closed/bug_6042.v
new file mode 100644
index 0000000000..72f612560b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6042.v
@@ -0,0 +1,7 @@
+Class C (n: nat) := T{x:True}.
+Generalizable All Variables.
+
+Fail Instance i : C n.
+
+Instance i : `(C n).
+Proof. repeat constructor. Defined.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 9a3a1d3709..aae24e0e0a 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.CMorphisms") -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.CMorphisms") -*- *)
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
@@ -308,7 +308,7 @@ Section GenericInstances.
Global Program
Instance trans_contra_inv_impl_type_morphism
- `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3.
+ `(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -318,7 +318,7 @@ Section GenericInstances.
Global Program
Instance trans_co_impl_type_morphism
- `(Transitive A R) : Proper (R ++> arrow) (R x) | 3.
+ `(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -328,7 +328,7 @@ Section GenericInstances.
Global Program
Instance trans_sym_co_inv_impl_type_morphism
- `(PER A R) : Proper (R ++> flip arrow) (R x) | 3.
+ `(PER A R) {x} : Proper (R ++> flip arrow) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -337,7 +337,7 @@ Section GenericInstances.
Qed.
Global Program Instance trans_sym_contra_arrow_morphism
- `(PER A R) : Proper (R --> arrow) (R x) | 3.
+ `(PER A R) {x} : Proper (R --> arrow) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -346,7 +346,7 @@ Section GenericInstances.
Qed.
Global Program Instance per_partial_app_type_morphism
- `(PER A R) : Proper (R ==> iffT) (R x) | 2.
+ `(PER A R) {x} : Proper (R ==> iffT) (R x) | 2.
Next Obligation.
Proof with auto.
@@ -399,17 +399,17 @@ Section GenericInstances.
(** Coq functions are morphisms for Leibniz equality,
applied only if really needed. *)
- Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') :
+ Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') {A} :
Reflexive (@Logic.eq A ==> R').
Proof. simpl_crelation. Qed.
(** [respectful] is a morphism for crelation equivalence . *)
- Global Instance respectful_morphism :
+ Global Instance respectful_morphism {A B} :
Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence)
(@respectful A B).
Proof.
- intros A B R R' HRR' S S' HSS' f g.
+ intros R R' HRR' S S' HSS' f g.
unfold respectful , relation_equivalence in *; simpl in *.
split ; intros H x y Hxy.
- apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)).
@@ -511,9 +511,9 @@ Ltac partial_application_tactic :=
(** Bootstrap !!! *)
-Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
+Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
Proof.
- intros A R R' HRR' x y <-. red in HRR'.
+ intros R R' HRR' x y <-. red in HRR'.
split ; red ; intros.
- now apply (fst (HRR' _ _)).
- now apply (snd (HRR' _ _)).
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index c70e3fe478..867d9cb9b3 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.Morphisms") -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.Morphisms") -*- *)
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
@@ -309,7 +309,7 @@ Section GenericInstances.
Global Program
Instance trans_contra_inv_impl_morphism
- `(Transitive A R) : Proper (R --> flip impl) (R x) | 3.
+ `(Transitive A R) {x} : Proper (R --> flip impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -319,7 +319,7 @@ Section GenericInstances.
Global Program
Instance trans_co_impl_morphism
- `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
+ `(Transitive A R) {x} : Proper (R ++> impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -329,7 +329,7 @@ Section GenericInstances.
Global Program
Instance trans_sym_co_inv_impl_morphism
- `(PER A R) : Proper (R ++> flip impl) (R x) | 3.
+ `(PER A R) {x} : Proper (R ++> flip impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -338,7 +338,7 @@ Section GenericInstances.
Qed.
Global Program Instance trans_sym_contra_impl_morphism
- `(PER A R) : Proper (R --> impl) (R x) | 3.
+ `(PER A R) {x} : Proper (R --> impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -347,7 +347,7 @@ Section GenericInstances.
Qed.
Global Program Instance per_partial_app_morphism
- `(PER A R) : Proper (R ==> iff) (R x) | 2.
+ `(PER A R) {x} : Proper (R ==> iff) (R x) | 2.
Next Obligation.
Proof with auto.
@@ -520,9 +520,9 @@ Ltac partial_application_tactic :=
(** Bootstrap !!! *)
-Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
+Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
Proof.
- intros A x y H y0 y1 e; destruct e.
+ intros x y H y0 y1 e; destruct e.
reduce in H.
split ; red ; intros H0.
- setoid_rewrite <- H.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index a168a8e7cd..964786d8e6 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -22,11 +22,11 @@ Generalizable Variables A l.
(** Morphisms for relations *)
-Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==>
+Instance relation_conjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==>
relation_equivalence ==> relation_equivalence) relation_conjunction.
Proof. firstorder. Qed.
-Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==>
+Instance relation_disjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==>
relation_equivalence ==> relation_equivalence) relation_disjunction.
Proof. firstorder. Qed.
@@ -43,11 +43,11 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed.
(** The instantiation at relation allows rewriting applications of relations
[R x y] to [R' x y] when [R] and [R'] are in [relation_equivalence]. *)
-Instance relation_equivalence_pointwise :
+Instance relation_equivalence_pointwise {A} :
Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id.
Proof. intro. apply (predicate_equivalence_pointwise (Tcons A (Tcons A Tnil))). Qed.
-Instance subrelation_pointwise :
+Instance subrelation_pointwise {A} :
Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id.
Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 5381e91997..401d7007e2 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -395,7 +395,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
-Program Instance predicate_equivalence_equivalence :
+Program Instance predicate_equivalence_equivalence {l} :
Equivalence (@predicate_equivalence l).
Next Obligation.
@@ -413,7 +413,7 @@ Program Instance predicate_equivalence_equivalence :
firstorder.
Qed.
-Program Instance predicate_implication_preorder :
+Program Instance predicate_implication_preorder {l} :
PreOrder (@predicate_implication l).
Next Obligation.
intro l; induction l ; firstorder.
@@ -480,7 +480,7 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type
(** The partial order defined by subrelation and relation equivalence. *)
-Program Instance subrelation_partial_order :
+Program Instance subrelation_partial_order {A} :
PartialOrder (@relation_equivalence A) subrelation.
Next Obligation.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index b4034b9cf9..09c25b38a6 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -61,11 +61,9 @@ Class Measure {A B} (f : A -> B).
(** Standard measures. *)
-Instance fst_measure : @Measure (A * B) A Fst.
-Defined.
+Instance fst_measure {A B} : @Measure (A * B) A Fst := {}.
-Instance snd_measure : @Measure (A * B) B Snd.
-Defined.
+Instance snd_measure {A B} : @Measure (A * B) B Snd := {}.
(** We define a product relation over [A*B]: each components should
satisfy the corresponding initial relation. *)
@@ -96,11 +94,11 @@ Section RelCompFun_Instances.
`(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
Proof. firstorder. Qed.
- Global Program Instance RelCompFun_Equivalence
- `(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
+ Global Instance RelCompFun_Equivalence
+ `(Measure A B f, Equivalence _ R) : Equivalence (R@@f) := {}.
- Global Program Instance RelCompFun_StrictOrder
- `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
+ Global Instance RelCompFun_StrictOrder
+ `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f) := {}.
End RelCompFun_Instances.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 054addc542..062cc90f8f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -502,9 +502,16 @@ let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx'
else
declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype
-let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
+let auto_generalize =
+ Goptions.declare_bool_option_and_ref
+ ~depr:true
+ ~key:["Instance";"Generalized";"Output"]
+ ~value:false
+
+let interp_instance_context ~program_mode env ctx ?(generalize=auto_generalize()) pl tclass =
let sigma, decl = interp_univ_decl_opt env pl in
let tclass =
+ (* when we remove this code, we can remove the middle argument of CGeneralization *)
if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass)
else tclass
in
@@ -530,10 +537,10 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
sigma, cl, u, c', ctx', ctx, imps, args, decl
-let new_instance_common ~program_mode ~generalize env instid ctx cl =
+let new_instance_common ~program_mode ?generalize env instid ctx cl =
let ({CAst.loc;v=instid}, pl) = instid in
let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
- interp_instance_context ~program_mode env ~generalize ctx pl cl
+ interp_instance_context ~program_mode env ?generalize ctx pl cl
in
(* The name generator should not be here *)
let id =
@@ -548,20 +555,20 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl =
let new_instance_interactive ?(global=false)
~poly instid ctx cl
- ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook
+ ?generalize ?(tac:unit Proofview.tactic option) ?hook
pri opt_props =
let env = Global.env() in
let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
- new_instance_common ~program_mode:false ~generalize env instid ctx cl in
+ new_instance_common ~program_mode:false ?generalize env instid ctx cl in
id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly
cty k u ctx ctx' pri decl imps subst id opt_props
let new_instance_program ?(global=false) ~pm
~poly instid ctx cl opt_props
- ?(generalize=true) ?hook pri =
+ ?generalize ?hook pri =
let env = Global.env() in
let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
- new_instance_common ~program_mode:true ~generalize env instid ctx cl in
+ new_instance_common ~program_mode:true ?generalize env instid ctx cl in
let pm =
do_instance_program ~pm env env' sigma ?hook ~global ~poly
cty k u ctx ctx' pri decl imps subst id opt_props in
@@ -569,10 +576,10 @@ let new_instance_program ?(global=false) ~pm
let new_instance ?(global=false)
~poly instid ctx cl props
- ?(generalize=true) ?hook pri =
+ ?generalize ?hook pri =
let env = Global.env() in
let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
- new_instance_common ~program_mode:false ~generalize env instid ctx cl in
+ new_instance_common ~program_mode:false ?generalize env instid ctx cl in
do_instance env env' sigma ?hook ~global ~poly
cty k u ctx ctx' pri decl imps subst id props;
id
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:03:54 +0000