Library mathcomp.ssreflect.ssreflect
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- Local additions:
- nonPropType == an interface for non-Prop Types: a nonPropType coerces
- to a Type, and only types that do not have sort
- Prop are canonical nonPropType instances. This is
- useful for applied views.
-> This will become standard with the Coq v8.11 SSReflect core library.
- deprecate old new == new, but warning that old is deprecated and new
- should be used instead.
-> Usage: Notation old := (deprecate old new) (only parsing).
-> Caveat: deprecate old new only inherits new's maximal implicits;
- on-demand implicits should be added after : (deprecate old new _).
-> Caveat 2: if premises or conclusions need to be adjusted, of for
- non-prenex implicits, use the idiom:
- Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...)
- _ ... _) (only printing).
- where all the implicit a_i's occur first, and correspond to the
- trailing 's, making sure deprecate old new is fully applied and
- there are no implicits inside the (fun .. => ..) expression. This
- is to avoid triggering a bug in SSReflect elaboration that is
- triggered by such evars under binders.
- Import Deprecation.Silent :: turn off deprecation warning messages.
- Import Deprecation.Reject :: raise an error instead of only warning.
-
-
-
-
-Module NonPropType.
- -
-Structure call_of (condition : unit) (result : bool) := Call {callee : Type}.
-Definition maybeProp (T : Type) := tt.
-Definition call T := Call (maybeProp T) false T.
- -
-Structure test_of (result : bool) := Test {condition :> unit}.
-Definition test_Prop (P : Prop) := Test true (maybeProp P).
-Definition test_negative := Test false tt.
- -
-Structure type :=
- Check {result : bool; test : test_of result; frame : call_of test result}.
-Definition check result test frame := @Check result test frame.
- -
-Module Exports.
-Canonical call.
-Canonical test_Prop.
-Canonical test_negative.
-Canonical check.
-Notation nonPropType := type.
-Coercion callee : call_of >-> Sortclass.
-Coercion frame : type >-> call_of.
-Notation notProp T := (@check false test_negative (call T)).
-End Exports.
- -
-End NonPropType.
-Export NonPropType.Exports.
- -
-Module Deprecation.
- -
-Definition hidden (T : Type) := T.
-Definition exposed (T : Type) & unit → unit → unit := T.
-Definition hide T u (v : exposed T u) : hidden T := v.
- -
-Ltac warn old_id new_id :=
- idtac "Warning:" old_id "is deprecated; use" new_id "instead".
- -
-Ltac stop old_id new_id :=
- fail 1 "Error:" old_id "is deprecated; use" new_id "instead".
- -
-Structure hinted := Hint {statement; hint : statement}.
-Ltac check cond := let test := constr:(hint _ : cond) in idtac.
- -
-Variant reject := Reject.
-Definition reject_hint := Hint reject Reject.
-Module Reject. Canonical reject_hint. End Reject.
- -
-Variant silent := Silent.
-Definition silent_hint := Hint silent Silent.
-Module Silent. Canonical silent_hint. End Silent.
- -
-Ltac flag old_id new_id :=
- first [check reject; stop old_id new_id | check silent | warn old_id new_id].
- -
-Module Exports.
-Coercion hide : exposed >-> hidden.
-Notation deprecate old_id new_id :=
- (hide (fun old_id new_id ⇒ ltac:(flag old_id new_id; exact tt)) new_id)
- (only parsing).
-End Exports.
- -
-End Deprecation.
-Export Deprecation.Exports.
-
--Module NonPropType.
- -
-Structure call_of (condition : unit) (result : bool) := Call {callee : Type}.
-Definition maybeProp (T : Type) := tt.
-Definition call T := Call (maybeProp T) false T.
- -
-Structure test_of (result : bool) := Test {condition :> unit}.
-Definition test_Prop (P : Prop) := Test true (maybeProp P).
-Definition test_negative := Test false tt.
- -
-Structure type :=
- Check {result : bool; test : test_of result; frame : call_of test result}.
-Definition check result test frame := @Check result test frame.
- -
-Module Exports.
-Canonical call.
-Canonical test_Prop.
-Canonical test_negative.
-Canonical check.
-Notation nonPropType := type.
-Coercion callee : call_of >-> Sortclass.
-Coercion frame : type >-> call_of.
-Notation notProp T := (@check false test_negative (call T)).
-End Exports.
- -
-End NonPropType.
-Export NonPropType.Exports.
- -
-Module Deprecation.
- -
-Definition hidden (T : Type) := T.
-Definition exposed (T : Type) & unit → unit → unit := T.
-Definition hide T u (v : exposed T u) : hidden T := v.
- -
-Ltac warn old_id new_id :=
- idtac "Warning:" old_id "is deprecated; use" new_id "instead".
- -
-Ltac stop old_id new_id :=
- fail 1 "Error:" old_id "is deprecated; use" new_id "instead".
- -
-Structure hinted := Hint {statement; hint : statement}.
-Ltac check cond := let test := constr:(hint _ : cond) in idtac.
- -
-Variant reject := Reject.
-Definition reject_hint := Hint reject Reject.
-Module Reject. Canonical reject_hint. End Reject.
- -
-Variant silent := Silent.
-Definition silent_hint := Hint silent Silent.
-Module Silent. Canonical silent_hint. End Silent.
- -
-Ltac flag old_id new_id :=
- first [check reject; stop old_id new_id | check silent | warn old_id new_id].
- -
-Module Exports.
-Coercion hide : exposed >-> hidden.
-Notation deprecate old_id new_id :=
- (hide (fun old_id new_id ⇒ ltac:(flag old_id new_id; exact tt)) new_id)
- (only parsing).
-End Exports.
- -
-End Deprecation.
-Export Deprecation.Exports.
-