Skip to content

Commit dd93d69

Browse files
committed
mk pred_of_argType a coercion from Sortclass
1 parent 7c9125c commit dd93d69

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

theories/ssr/ssrbool.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1366,7 +1366,7 @@ Module Export PredSortOfSimplCoercion := DeclarePredSortOfSimpl PredOfSimpl.
13661366
Definition predArgType := Type.
13671367
Bind Scope type_scope with predArgType.
13681368
Identity Coercion sort_of_predArgType : predArgType >-> Sortclass.
1369-
Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT.
1369+
Coercion pred_of_argType (T : Type) : simpl_pred T := predT.
13701370
Notation "{ : T }" := (T%type : predArgType) : type_scope.
13711371

13721372
(** Boolean relations.

0 commit comments

Comments
 (0)