diff options
28 files changed, 37 insertions, 109 deletions
diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v index 311748341..3b0de76b4 100644 --- a/plugins/micromega/Refl.v +++ b/plugins/micromega/Refl.v @@ -15,7 +15,6 @@ Require Import List. Require Setoid. -Import Morphisms Morphisms_Prop. (* For Hints *) Set Implicit Arguments. diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index fab676da8..b1d021768 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -15,7 +15,6 @@ Require Import List. Require Import Refl. Require Import Bool. -Import Morphisms Morphisms_Prop. (* For Hints *) Set Implicit Arguments. diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v index a42c3ff72..0444fe74a 100644 --- a/plugins/ring/Setoid_ring_theory.v +++ b/plugins/ring/Setoid_ring_theory.v @@ -8,7 +8,6 @@ Require Export Bool. Require Export Setoid. -Import Morphisms. Set Implicit Arguments. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index dc47e9686..faa83dedc 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -13,7 +13,6 @@ Require Import BinPos. Require Import BinNat. Require Import BinInt. Require Export Ring_theory. -Import Morphisms. (* For Hints *) Open Local Scope positive_scope. Import RingSyntax. diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 028804bb6..b3250a510 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -9,7 +9,6 @@ Require Import Setoid. Require Import BinPos. Require Import BinNat. -Import Morphisms. (* For Hints *) Set Implicit Arguments. diff --git a/pretyping/classops.ml b/pretyping/classops.ml index d57dd7b40..5c30f05aa 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -336,18 +336,7 @@ let class_params = function let add_class cl = add_new_class cl { cl_param = class_params cl } -let automatically_import_coercions = ref false - -open Goptions -let _ = - declare_bool_option - { optsync = true; - optname = "automatic importation of coercions"; - optkey = ["Automatic";"Coercions";"Importation"]; - optread = (fun () -> !automatically_import_coercions); - optwrite = (:=) automatically_import_coercions } - -let cache_coercion (_,(coe,stre,isid,cls,clt,ps)) = +let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) = add_class cls; add_class clt; let is,_ = class_info cls in @@ -361,17 +350,8 @@ let cache_coercion (_,(coe,stre,isid,cls,clt,ps)) = add_new_coercion coe xf; add_coercion_in_graph (xf,is,it) -let load_coercion _ o = - if - !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2 - then - cache_coercion o - -let open_coercion _ o = - if not - (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2) - then - cache_coercion o +let cache_coercion o = + load_coercion 1 o let subst_coercion (subst,(coe,stre,isid,cls,clt,ps as obj)) = let coe' = subst_coe_typ subst coe in @@ -400,7 +380,6 @@ let classify_coercion (coe,stre,isid,cls,clt,ps as obj) = let (inCoercion,_) = declare_object {(default_object "COERCION") with - open_function = open_coercion; load_function = load_coercion; cache_function = cache_coercion; subst_function = subst_coercion; diff --git a/tactics/auto.ml b/tactics/auto.ml index ba38f5458..0448b0b22 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -402,35 +402,12 @@ type hint_action = | CreateDB of bool * transparent_state | AddTransparency of evaluable_global_reference list * bool | AddTactic of (global_reference option * pri_auto_tactic) list -let automatically_import_hints = ref false - -open Goptions -let _ = - declare_bool_option - { optsync = true; - optname = "automatic importation of hints"; - optkey = ["Automatic";"Hints";"Importation"]; - optread = (fun () -> !automatically_import_hints); - optwrite = (:=) automatically_import_hints } - let cache_autohint (_,(local,name,hints)) = match hints with | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b) | AddTransparency (grs, b) -> add_transparency name grs b | AddTactic hints -> add_hint name hints -let load_autohint _ x = - if - !automatically_import_hints || Flags.version_less_or_equal Flags.V8_2 - then - cache_autohint x - -let open_autohint _ x = - if - not (!automatically_import_hints || Flags.version_less_or_equal Flags.V8_2) - then - cache_autohint x - let forward_subst_tactic = ref (fun _ -> failwith "subst_tactic is not installed for auto") @@ -523,8 +500,7 @@ let discharge_autohint (_,(local,name,hintlist as obj)) = let (inAutoHint,_) = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; - open_function = open_autohint; - load_function = load_autohint; + load_function = (fun _ -> cache_autohint); subst_function = subst_autohint; classify_function = classify_autohint } diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index e1ea24b91..c717e9bf5 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -6,8 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Lt Le Plus. -Require Import Compare_dec Even. +Require Import Lt. +Require Import Plus. +Require Import Compare_dec. +Require Import Even. Open Local Scope nat_scope. diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 472af69c5..b41d65c39 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -10,7 +10,6 @@ Require Export Bool Sumbool. Require Import Minus. -Import Lt. (* For Hints *) Open Local Scope nat_scope. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index d6fc88338..f15ab222c 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -13,12 +13,11 @@ left projection. *) Require Import FMapInterface. -Import Morphisms. (* For Hints *) Set Implicit Arguments. Unset Strict Implicit. -Module Raw (Import X:OrderedType). +Module Raw (X:OrderedType). Module Import MX := OrderedTypeFacts X. Module Import PX := KeyOrderedType X. @@ -1155,7 +1154,7 @@ Section Elt. End Make. -Module Make_ord (X: OrderedType)(Import D : OrderedType) <: +Module Make_ord (X: OrderedType)(D : OrderedType) <: Sord with Module Data := D with Module MapS.E := X. @@ -1333,7 +1332,6 @@ Proof. inversion_clear Hm2; auto. destruct (IHm1 Hm11 (Build_slist Hm22)); [ apply LT | apply EQ | apply GT ]; cmp_solve. -Show. Qed. End Make_ord. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index a952d5679..6c1e8ca89 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -12,12 +12,11 @@ [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *) Require Import FMapInterface. -Import Morphisms_Prop. (* For Hints *) Set Implicit Arguments. Unset Strict Implicit. -Module Raw (Import X:DecidableType). +Module Raw (X:DecidableType). Module Import PX := KeyDecidableType X. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 7df48dca0..d1e3f90b3 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -7,7 +7,6 @@ (************************************************************************) Require Import Le Gt Minus Bool. -Import Plus. (* For Hints *) Set Implicit Arguments. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 64f534f90..88ccdb126 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -9,7 +9,6 @@ Require Export List. Require Export Sorting. Require Export Setoid Basics Morphisms. -Import Morphisms_Prop. (* For Hints *) Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 23ca56524..ea53c7d06 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -7,7 +7,6 @@ (************************************************************************) Require Import Bool Setoid Bvector BinPos BinNat. -Import Le Morphisms. (* For Hints *) (** Operation over bits of a [N] number. *) diff --git a/theories/NArith/Pminmax.v b/theories/NArith/Pminmax.v index 98d447824..4cc48af66 100644 --- a/theories/NArith/Pminmax.v +++ b/theories/NArith/Pminmax.v @@ -7,7 +7,6 @@ (************************************************************************) Require Import Orders BinPos Pnat POrderedType GenericMinMax. -Import Plus. (* For Hints *) (** * Maximum and Minimum of two positive numbers *) @@ -124,4 +123,4 @@ Proof. apply plus_min_distr_l. Qed. -End P. +End P.
\ No newline at end of file diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 321c9eb89..9f587a1d0 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -9,7 +9,6 @@ (************************************************************************) Require Import NZAxioms. -Import Morphisms_Prop. (* For Hints *) Module Type NZBasePropSig (Import NZ : NZDomainSig'). diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 79c95ded6..1f6c615bc 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -9,7 +9,6 @@ (** Euclidean Division *) Require Import NZAxioms NZMulOrder. -Import Morphisms_Prop. (* For Hints *) (** The first signatures will be common to all divisions over NZ, N and Z *) diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 6aa09dd54..acc43fc17 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -10,7 +10,6 @@ Require Import NZAxioms. Require Import NZAddOrder. -Import Morphisms_Prop. (* For Hints *) Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig'). Include NZAddOrderPropSig NZ. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index dc62b1717..bfbcc2c65 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -9,7 +9,6 @@ (************************************************************************) Require Import NZAxioms NZBase Decidable OrdersTac. -Import Morphisms_Prop. (* For Hints *) Module Type NZOrderPropSig (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ). diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 249674f3e..f26f56d0c 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -11,7 +11,6 @@ Require Export Decidable. Require Export NAxioms. Require Import NZProperties. -Import Morphisms_Prop. (* For Hints *) Module NBasePropFunct (Import N : NAxiomsSig'). (** First, we import all known facts about both natural numbers and integers. *) diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 4cada985d..5b7aa24b7 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -68,7 +68,7 @@ Section multiset_defs. Qed. - Require Import Plus. (* comm. and ass. of plus *) + Require Plus. (* comm. and ass. of plus *) Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x). Proof. @@ -168,8 +168,6 @@ Section multiset_defs. (** SingletonBag *) -Import Morphisms_Prop Morphisms. (* For Hints *) - Lemma meq_singleton : forall a a', eqA a a' -> meq (SingletonBag a) (SingletonBag a'). Proof. diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 3b7dea5e4..68f201897 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -7,7 +7,6 @@ (***********************************************************************) Require Import Orders OrdersTac OrdersFacts Setoid Morphisms Basics. -Import Morphisms_Prop. (* For Hints *) (** * A Generic construction of min and max *) diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 5919a7646..6b9007fdd 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -7,7 +7,6 @@ (***********************************************************************) Require Export SetoidList Morphisms OrdersTac. -Import Morphisms_Prop. (* For Hints *) Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 01c6c62e7..f83e77ed8 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -7,8 +7,6 @@ (***********************************************************************) Require Export Relations Morphisms Setoid Equalities. -Import Morphisms_Prop. (* For Hints *) - Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 69a7c3b9e..a28b79776 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -8,7 +8,6 @@ Require Import Basics OrdersTac. Require Export Orders. -Import Morphisms_Prop. (* For Hints *) Set Implicit Arguments. Unset Strict Implicit. @@ -207,7 +206,6 @@ End OrderedTypeTest. Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull. -Import O. Definition t := O.t. Definition eq := O.eq. Instance eq_equiv : Equivalence eq. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 80871d102..66a672c92 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -87,7 +87,6 @@ Ltac subst_eqns := Definition interp_ord o := match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end. Local Notation "#" := interp_ord. -Import Morphisms_Prop. (* For Hints *) Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. Proof. @@ -268,21 +267,19 @@ End OT_to_OrderTac. Module TotalOrderRev (O:TotalOrder) <: TotalOrder. -Import O. Definition t := O.t. Definition eq := O.eq. Definition lt := flip O.lt. Definition le := flip O.le. Include EqLtLeNotation. -Import RelationClasses. (* For hints *) (* No Instance syntax to avoid saturating the Equivalence tables *) Definition eq_equiv := O.eq_equiv. Instance lt_strorder: StrictOrder lt. -Proof. unfold lt. auto using O.lt_strorder with *. Qed. +Proof. unfold lt; auto with *. Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. -Proof. unfold lt; auto using O.lt_compat with *. Qed. +Proof. unfold lt; auto with *. Qed. Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y. Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed. diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index a8b5576f5..2dce5fbe4 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -100,8 +100,8 @@ Section decidability. Definition Z_le_gt_dec : {x <= y} + {x > y}. Proof. - elim Z_le_dec; auto. - intro. right. apply Znot_le_gt; auto. + elim Z_le_dec; auto with arith. + intro. right. apply Znot_le_gt; auto with arith. Defined. Definition Z_gt_le_dec : {x > y} + {x <= y}. @@ -111,17 +111,17 @@ Section decidability. Definition Z_ge_lt_dec : {x >= y} + {x < y}. Proof. - elim Z_ge_dec; auto. - intro. right. apply Znot_ge_lt; auto. + elim Z_ge_dec; auto with arith. + intro. right. apply Znot_ge_lt; auto with arith. Defined. Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}. Proof. intro H. apply Zcompare_rec with (n := x) (m := y). - intro. right. elim (Zcompare_Eq_iff_eq x y); auto. - intro. left. elim (Zcompare_Eq_iff_eq x y); auto. - intro H1. absurd (x > y); auto. + intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith. + intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith. + intro H1. absurd (x > y); auto with arith. Defined. End decidability. diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 0c87f6223..4dfce35ce 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -145,32 +145,32 @@ Definition Zdiv2 (z:Z) := Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n. Proof. intro x; destruct x. - auto. - destruct p; auto. - intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto. - intros. absurd (Zeven 1); red in |- *; auto. - destruct p; auto. - intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto. - intros. absurd (Zeven (-1)); red in |- *; auto. + auto with arith. + destruct p; auto with arith. + intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto with arith. + intros. absurd (Zeven 1); red in |- *; auto with arith. + destruct p; auto with arith. + intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto with arith. + intros. absurd (Zeven (-1)); red in |- *; auto with arith. Qed. Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1. Proof. intro x; destruct x. - intros. absurd (Zodd 0); red in |- *; auto. - destruct p; auto. - intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto. - intros. absurd (Zneg p >= 0); red in |- *; auto. + intros. absurd (Zodd 0); red in |- *; auto with arith. + destruct p; auto with arith. + intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith. + intros. absurd (Zneg p >= 0); red in |- *; auto with arith. Qed. Lemma Zodd_div2_neg : forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1. Proof. intro x; destruct x. - intros. absurd (Zodd 0); red in |- *; auto. - intros. absurd (Zneg p >= 0); red in |- *; auto. - destruct p; auto. - intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto. + intros. absurd (Zodd 0); red in |- *; auto with arith. + intros. absurd (Zneg p >= 0); red in |- *; auto with arith. + destruct p; auto with arith. + intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith. Qed. Lemma Z_modulo_2 : |