diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-27 19:43:51 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-27 19:43:51 +0000 |
| commit | 36c448f43c7fa16163b543b941be4a917a712a37 (patch) | |
| tree | 73affd4fede1fea0dd56a2600bc420de769432e2 /theories/Classes/SetoidTactics.v | |
| parent | 3178c7a29ff8b57a4598c4c5ded2eb29b8067dcf (diff) | |
Add a new vernacular command for controling implicit generalization of
variables with syntax:
[Local?|Global] Generalizable Variable(s)? [all|none|id1 idn].
By default no variable is generalizable, so this patch breaks backward
compatibility with files that used implicit generalization (through
Instance declarations for example). To get back the old behavior, one
just needs to use [Global Generalizable Variables all].
Make coq_makefile more robust using [mkdir -p].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidTactics.v')
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index c40e37e24..669be8b0f 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -18,6 +18,8 @@ Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions. Require Import Coq.Classes.Equivalence Coq.Program.Basics. +Generalizable Variables A R. + Export ProperNotations. Set Implicit Arguments. @@ -177,3 +179,5 @@ Ltac default_add_morphism_tactic := Ltac add_morphism_tactic := default_add_morphism_tactic. Obligation Tactic := program_simpl. + +(* Notation "'Morphism' s t " := (@Proper _ (s%signature) t) (at level 10, s at next level, t at next level). *) |