From ae96b60dc9264703ed6a43c48e0c4892bffad131 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 7 Nov 2017 15:08:26 -0500 Subject: Remove function evar package in favor of generic rel one --- src/Util/SideConditions/CorePackages.v | 27 +++++---------------------- 1 file changed, 5 insertions(+), 22 deletions(-) (limited to 'src/Util/SideConditions') diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v index 8126c5280..c1041d040 100644 --- a/src/Util/SideConditions/CorePackages.v +++ b/src/Util/SideConditions/CorePackages.v @@ -6,11 +6,11 @@ Record evar_package {T} (v : T) := Arguments val {T v} _. Arguments evar_package_pf {T v} _. -Record evar_function_package {A B} (f : forall x : A, B x) := - { valf : forall x : A, B x; - evarf_package_pf : forall x, valf x = f x }. -Arguments valf {A B f} _. -Arguments evarf_package_pf {A B f} _ _. +Record evar_rel_package {A} (f : A) B (R : B -> A -> Prop) := + { valr : B; + evarr_package_pf : R valr f }. +Arguments valr {A f B R} _. +Arguments evarr_package_pf {A f B R} _. Record evard_package {s d} (v : s) := { vald : d; @@ -20,21 +20,4 @@ Arguments vald {s d v} _. Arguments evard_package_pfT {s d v} _. Arguments evard_package_pf {s d v} _. -Local Notation "'rew' 'dependent' H 'in' H'" - := (match H with - | eq_refl => H' - end) - (at level 10, H' at level 10, - format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'"). - -Record evard_function_package {sA sB dA dB} (f : forall x : sA, sB x) := - { valdf : forall x : dA, dB x; - evardf_package_pfTA : dA = sA; - evardf_package_pfTB : forall x, sB (rew evardf_package_pfTA in x) = dB x; - evardf_package_pf : forall x, valdf x = rew dependent evardf_package_pfTB x in (f (rew evardf_package_pfTA in x)) }. -Arguments valdf {sA sB dA dB f} _ _. -Arguments evardf_package_pfTA {sA sB dA dB f} _. -Arguments evardf_package_pfTB {sA sB dA dB f} _. -Arguments evardf_package_pf {sA sB dA dB f} _ _. - Ltac autosolve else_tac := else_tac (). -- cgit v1.2.3