diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 15:44:48 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 15:44:48 -0700 |
| commit | 16737faa337e3a47bb2d7283cb57ee93342a3eb0 (patch) | |
| tree | d151040bc517da73316c75147d5c522716e9664f /src/Reflection/TestCase.v | |
| parent | 02c9314745f8105043833ef46c683b5ba7486e6a (diff) | |
Better implicit arguments for wf types
Diffstat (limited to 'src/Reflection/TestCase.v')
| -rw-r--r-- | src/Reflection/TestCase.v | 8 |
1 files changed, 4 insertions, 4 deletions
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. |