diff options
| -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. |