diff options
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Basics.v | 2 | ||||
-rw-r--r-- | theories/Program/Combinators.v | 2 | ||||
-rw-r--r-- | theories/Program/Equality.v | 5 | ||||
-rw-r--r-- | theories/Program/Program.v | 2 | ||||
-rw-r--r-- | theories/Program/Subset.v | 2 | ||||
-rw-r--r-- | theories/Program/Syntax.v | 2 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 4 | ||||
-rw-r--r-- | theories/Program/Utils.v | 2 | ||||
-rw-r--r-- | theories/Program/Wf.v | 6 |
9 files changed, 15 insertions, 12 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index f4017024..a298032f 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Basics.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Standard functions and combinators. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 39fb4093..e61c7027 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Combinators.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** * Proofs about standard combinators, exports functional extensionality. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 1e139497..2764d1b4 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$ i*) +(*i $Id: Equality.v 13359 2010-07-30 08:46:55Z herbelin $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -15,6 +15,9 @@ Require Export JMeq. Require Import Coq.Program.Tactics. +Local Notation "'Π' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + Ltac is_ground_goal := match goal with |- ?T => is_ground T diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 71be3478..929fc47c 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Program.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index ce5f1068..9d82fde8 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Subset.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Tactics related to subsets and proof irrelevance. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 05bf2ea6..0e6b2909 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$ *) +(* $Id: Syntax.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Custom notations and implicits for Coq prelude definitions. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 91a8edff..333dd7a6 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Tactics.v 13332 2010-07-26 22:12:43Z msozeau $ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) @@ -101,7 +101,7 @@ Ltac revert_last := [ H : _ |- _ ] => revert H end. -(** Reapeateadly reverse the last hypothesis, putting everything in the goal. *) +(** Repeatedly reverse the last hypothesis, putting everything in the goal. *) Ltac reverse := repeat revert_last. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index f2aad800..b2b5d4be 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Utils.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Various syntaxic shortands that are useful with [Program]. *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index d16e900f..4159f436 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$ *) +(* $Id: Wf.v 13332 2010-07-26 22:12:43Z msozeau $ *) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) @@ -214,7 +214,7 @@ Ltac fold_sub f := match goal with | [ |- ?T ] => match T with - appcontext C [ @Fix_sub _ _ _ _ ?arg ] => + appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] => let app := context C [ f arg ] in change app end @@ -251,6 +251,6 @@ Module WfExtensionality. Ltac unfold_sub f fargs := set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; - rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig. + rewrite fix_sub_eq_ext ; repeat fold_sub f ; simpl proj1_sig. End WfExtensionality. |