diff options
author | 2008-05-11 22:04:26 +0000 | |
---|---|---|
committer | 2008-05-11 22:04:26 +0000 | |
commit | 30443ddaba7a0cc996216b3d692b97e0b05907fe (patch) | |
tree | 1a1bdadcdf69582262bd6bddc21e9e03215d2871 /theories/Classes/EquivDec.v | |
parent | b6c6e36afa8da16a62bf16191baa2531894c54fc (diff) |
- Cleanup parsing of binders, reducing to a single production for all
binders.
- Change syntax of type class instances to better match the usual syntax of
lemmas/definitions with name first, then arguments ":" instance.
Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
Program.Utils, and subset_scope as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/EquivDec.v')
-rw-r--r-- | theories/Classes/EquivDec.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 62744b1d1..d96a532c3 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -94,8 +94,8 @@ Program Instance unit_eqdec : ! EqDec unit eq := reflexivity. Qed. -Program Instance [ EqDec A eq, EqDec B eq ] => - prod_eqdec : ! EqDec (prod A B) eq := +Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] : + ! EqDec (prod A B) eq := equiv_dec x y := let '(x1, x2) := x in let '(y1, y2) := y in @@ -106,8 +106,8 @@ Program Instance [ EqDec A eq, EqDec B eq ] => Solve Obligations using unfold complement, equiv ; program_simpl. -Program Instance [ EqDec A eq, EqDec B eq ] => - sum_eqdec : ! EqDec (sum A B) eq := +Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] : + ! EqDec (sum A B) eq := equiv_dec x y := match x, y with | inl a, inl b => if a == b then in_left else in_right @@ -121,7 +121,7 @@ Program Instance [ EqDec A eq, EqDec B eq ] => Require Import Coq.Program.FunctionalExtensionality. -Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq := +Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq := equiv_dec f g := if f true == g true then if f false == g false then in_left @@ -138,7 +138,7 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq Require Import List. -Program Instance [ eqa : EqDec A eq ] => list_eqdec : ! EqDec (list A) eq := +Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq := equiv_dec := fix aux (x : list A) y { struct x } := match x, y with |