From eede58e3330749e3719c5452288ae20906c352e2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 11:57:47 -0700 Subject: Fix a typo --- src/Util/PointedProp.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/PointedProp.v') 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. -- cgit v1.2.3