From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- theories/Classes/RelationClasses.v | 8 ++++---- theories/FSets/FMapAVL.v | 2 +- theories/Init/Wf.v | 4 +++- theories/Program/Equality.v | 23 ++++++++++++----------- theories/Program/Syntax.v | 16 +++++++--------- theories/Program/Wf.v | 4 +--- theories/Structures/Equalities.v | 5 ++--- 7 files changed, 30 insertions(+), 32 deletions(-) (limited to 'theories') diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 1aad3cec..2bfebfd8 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -15,7 +15,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: RelationClasses.v 13344 2010-07-28 15:04:36Z msozeau $ *) +(* $Id: RelationClasses.v 13476 2010-09-30 11:42:11Z letouzey $ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. @@ -149,9 +149,9 @@ Program Instance iff_Transitive : Transitive iff. (** Leibniz equality. *) -Program Instance eq_Reflexive : Reflexive (@eq A). -Program Instance eq_Symmetric : Symmetric (@eq A). -Program Instance eq_Transitive : Transitive (@eq A). +Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A. +Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A. +Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A. (** Various combinations of reflexivity, symmetry and transitivity. *) diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 7b64ded7..cf0449f8 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -8,7 +8,7 @@ (* Finite map library. *) -(* $Id: FMapAVL.v 13090 2010-06-08 13:56:14Z herbelin $ *) +(* $Id: FMapAVL.v 13427 2010-09-17 17:37:52Z letouzey $ *) (** * FMapAVL *) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index be7becda..c8c5e3d6 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Wf.v 13492 2010-10-04 21:20:01Z herbelin $ i*) (** * This module proves the validity of - well-founded recursion (also known as course of values) @@ -36,6 +36,8 @@ Section Well_founded. destruct 1; trivial. Defined. + Global Implicit Arguments Acc_inv [x y] [x]. + (** A relation is well-founded if every element is accessible *) Definition well_founded := forall a:A, Acc a. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 2764d1b4..53e12723 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 13359 2010-07-30 08:46:55Z herbelin $ i*) +(*i $Id: Equality.v 13492 2010-10-04 21:20:01Z herbelin $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -33,7 +33,8 @@ Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso. Definition block {A : Type} (a : A) := a. Ltac block_goal := match goal with [ |- ?T ] => change (block T) end. -Ltac unblock_goal := unfold block in *. +Ltac unblock_goal := unfold block at 1. +Ltac unblock_all := unfold block in *. (** Notation for heterogenous equality. *) @@ -41,8 +42,8 @@ Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). (** Notation for the single element of [x = x] and [x ~= x]. *) -Implicit Arguments eq_refl [[A] [x]]. -Implicit Arguments JMeq_refl [[A] [x]]. +Implicit Arguments eq_refl [[A] [x]] [A]. +Implicit Arguments JMeq_refl [[A] [x]] [A]. (** Do something on an heterogeneous equality appearing in the context. *) @@ -224,7 +225,7 @@ Ltac simplify_eqs := Ltac simplify_IH_hyps := repeat match goal with - | [ hyp : _ |- _ ] => specialize_eqs hyp + | [ hyp : context [ block _ ] |- _ ] => specialize_eqs hyp ; unfold block in hyp end. (** We split substitution tactics in the two directions depending on which @@ -389,18 +390,18 @@ Tactic Notation "intro_block_id" ident(H) := (is_introduced H ; block_goal ; revert_until H) || (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal). -Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. +Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_all. Ltac do_intros H := (try intros until H) ; (intro_block_id H || intro_block H). -Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; tac H. +Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; block_goal ; tac H ; unblock_goal. Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim. Ltac do_depind tac H := - (try intros until H) ; intro_block H ; - generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. + do_intros H ; generalize_eqs_vars H ; block_goal ; tac H ; + unblock_goal ; simplify_dep_elim ; simplify_IH_hyps ; unblock_all. (** To dependent elimination on some hyp. *) @@ -417,8 +418,8 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id. (** A variant where generalized variables should be given by the user. *) Ltac do_depelim' tac H := - (try intros until H) ; block_goal ; generalize_eqs H ; tac H ; simplify_dep_elim ; - simplify_IH_hyps ; unblock_goal. + (try intros until H) ; block_goal ; generalize_eqs H ; block_goal ; tac H ; unblock_goal ; + simplify_dep_elim ; simplify_IH_hyps ; unblock_all. (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. By default, we don't try to generalize the hyp by its variable indices. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 0e6b2909..2f89ff53 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Syntax.v 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: Syntax.v 13492 2010-10-04 21:20:01Z herbelin $ *) (** Custom notations and implicits for Coq prelude definitions. @@ -20,16 +20,14 @@ Notation " () " := tt. (** Set maximally inserted implicit arguments for standard definitions. *) -Implicit Arguments eq [[A]]. - Implicit Arguments Some [[A]]. Implicit Arguments None [[A]]. -Implicit Arguments inl [[A] [B]]. -Implicit Arguments inr [[A] [B]]. +Implicit Arguments inl [[A] [B]] [A]. +Implicit Arguments inr [[A] [B]] [B]. -Implicit Arguments left [[A] [B]]. -Implicit Arguments right [[A] [B]]. +Implicit Arguments left [[A] [B]] [A]. +Implicit Arguments right [[A] [B]] [B]. Implicit Arguments pair [[A] [B]]. Implicit Arguments fst [[A] [B]]. @@ -50,8 +48,8 @@ Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. Require Import Bvector. -Implicit Arguments Vnil [[A]]. -Implicit Arguments Vcons [[A] [n]]. +Implicit Arguments Vnil [[A]] []. +Implicit Arguments Vcons [[A] [n]] []. (** Treating n-ary exists *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 4159f436..4ca49c41 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Wf.v 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: Wf.v 13492 2010-10-04 21:20:01Z herbelin $ *) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) @@ -16,8 +16,6 @@ Require Import ProofIrrelevance. Open Local Scope program_scope. -Implicit Arguments Acc_inv [A R x y]. - Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index d205c0e0..382511d9 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: Equalities.v 12662 2010-01-13 16:53:01Z letouzey $ *) +(* $Id: Equalities.v 13475 2010-09-29 14:33:13Z letouzey $ *) Require Export RelationClasses. @@ -176,8 +176,7 @@ Module Type UsualEq <: Eq := Typ <+ HasUsualEq. Module Type UsualIsEq (E:UsualEq) <: IsEq E. (* No Instance syntax to avoid saturating the Equivalence tables *) - Lemma eq_equiv : Equivalence E.eq. - Proof. exact eq_equivalence. Qed. + Definition eq_equiv : Equivalence E.eq := eq_equivalence. End UsualIsEq. Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E. -- cgit v1.2.3