diff options
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Equality.v | 23 | ||||
-rw-r--r-- | theories/Program/Syntax.v | 16 | ||||
-rw-r--r-- | theories/Program/Wf.v | 4 |
3 files changed, 20 insertions, 23 deletions
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. |