Skip to content

Commit

Permalink
Adapt to coq/coq#19690 (Hint Extern respects default proof mode)
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Oct 15, 2024
1 parent e7771d9 commit 1c9562e
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/Rupicola/Lib/IdentParsing.v
Original file line number Diff line number Diff line change
@@ -326,6 +326,8 @@ Module TC.
end).

Class __IdentToString := __identToString: string.

Set Default Proof Mode "Classic". (* after Rocq 9, Default Proof Mode "Ltac2" will parse hint extern as ltac2 *)
#[global] Hint Extern 1 __IdentToString => serialize_ident_in_context : typeclass_instances.

Notation ident_to_string a :=

0 comments on commit 1c9562e

Please sign in to comment.