diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 11:57:47 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 11:57:47 -0700 |
| commit | eede58e3330749e3719c5452288ae20906c352e2 (patch) | |
| tree | 24a96260d22c8a68ca8eecd37774611431ceda3c /src/Util/PointedProp.v | |
| parent | ed88b28433ef90f8be554803a4fe852a6634ee87 (diff) | |
Fix a typo
Diffstat (limited to 'src/Util/PointedProp.v')
| -rw-r--r-- | src/Util/PointedProp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/PointedProp.v b/src/Util/PointedProp.v index 76c760632..bc9626477 100644 --- a/src/Util/PointedProp.v +++ b/src/Util/PointedProp.v @@ -4,7 +4,7 @@ express equality of types. *) Require Import Crypto.Util.Notations. -Delimit Scope pointed_prop_scope with pointed_prod. +Delimit Scope pointed_prop_scope with pointed_prop. Inductive pointed_Prop := trivial | inject (_ : Prop). Bind Scope pointed_prop_scope with pointed_Prop. |