From a30d1b32016fcb7ffb86170705a9a35ed1b2dd9e Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org> Date: Mon, 6 Mar 2017 14:55:08 +0100 Subject: [PATCH] Try making [lrust_typing] non-discriminated to see whether anything changes. --- .gitlab-ci.yml | 1 + theories/typing/lft_contexts.v | 5 +++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 12d26b50..7b1a6642 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -22,6 +22,7 @@ lrust-coq8.6: - master - ci - /^ralf/ci// + - jh/undiscriminated_hintdb artifacts: paths: - build-time.txt diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v index ae8dbde0..0cd42e35 100644 --- a/theories/typing/lft_contexts.v +++ b/theories/typing/lft_contexts.v @@ -454,6 +454,9 @@ End elctx_incl. Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL. +Create HintDb lrust_typing. +Create HintDb lrust_typing_merge. + (* We first try to solve everything without the merging rules, and then start from scratch with them. @@ -463,8 +466,6 @@ Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL. Ltac solve_typing := (typeclasses eauto with lrust_typing typeclass_instances core; fail) || (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail). -Create HintDb lrust_typing discriminated. -Create HintDb lrust_typing_merge discriminated. Hint Constructors Forall Forall2 elem_of_list : lrust_typing. Hint Resolve of_val_unlock : lrust_typing. -- GitLab