Skip to content
Snippets Groups Projects
Commit a013bcff authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan Committed by Ralf Jung
Browse files

This Coq bug is fixed.

parent 9ec31359
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 5 deletions
theories/typing/base.v
+ 1
− 5
View file @ a013bcff
...@@ -23,8 +23,4 @@ Hint Extern 1 (@eq nat _ (Z.to_nat _)) => ...@@ -23,8 +23,4 @@ Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
Hint Extern 1 (@eq nat (Z.to_nat _) _) => Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
(etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing. (etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
(* FIXME : I would prefer using a [Hint Resolve <-] for this, but Hint Resolve <- elem_of_app : lrust_typing.
unfortunately, this is not preserved across modules. See:
https://coq.inria.fr/bugs/show_bug.cgi?id=5189
This should be fixed in the next version of Coq. *)
Hint Extern 1 (_ ∈ _ ++ _) => apply <- @elem_of_app : lrust_typing.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment