diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-17 21:15:43 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-17 21:16:51 -0500 |
| commit | 161486374e7da76ae6b6dde3dbbff7478399008d (patch) | |
| tree | 03ed854e43eea1ea26644aad6b7b9fadf64eeeb5 /src/Reflection | |
| parent | 6aa09f0626ca2f05b2f6c295c39f2616e96cb57f (diff) | |
Remove an admit
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/Z/Syntax.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v index ab47929b1..466dbd4b5 100644 --- a/src/Reflection/Z/Syntax.v +++ b/src/Reflection/Z/Syntax.v @@ -28,9 +28,6 @@ Local Notation eta x := (fst x, snd x). Local Notation eta3 x := (eta (fst x), snd x). Local Notation eta4 x := (eta3 (fst x), snd x). -Axiom proof_admitted : False. -Local Notation admit := (match proof_admitted with end). - Inductive op : flat_type base_type -> flat_type base_type -> Type := | Add : op (tZ * tZ) tZ | Sub : op (tZ * tZ) tZ |