From 16737faa337e3a47bb2d7283cb57ee93342a3eb0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 15:44:48 -0700 Subject: Better implicit arguments for wf types --- src/Reflection/TestCase.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/Reflection/TestCase.v') diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index 7511bb750..0f6384bb2 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -103,17 +103,17 @@ Qed. Ltac reflect_Wf := WfReflective.reflect_Wf base_type_eq_semidec_is_dec op_beq_bl. -Lemma example_expr_wf_slow : Wf _ _ _ example_expr. +Lemma example_expr_wf_slow : Wf example_expr. Proof. Time (vm_compute; intros; repeat match goal with - | [ |- wf _ _ _ _ _ _ ] => constructor; intros - | [ |- wff _ _ _ _ _ _ ] => constructor; intros + | [ |- wf _ _ _ ] => constructor; intros + | [ |- wff _ _ _ ] => constructor; intros | [ |- List.In _ _ ] => vm_compute | [ |- ?x = ?x \/ _ ] => left; reflexivity | [ |- ?x = ?y \/ _ ] => right end). (* 0.036 s *) Qed. -Lemma example_expr_wf : Wf _ _ _ example_expr. +Lemma example_expr_wf : Wf example_expr. Proof. Time reflect_Wf. (* 0.008 s *) Qed. -- cgit v1.2.3