diff options
| author | coqbot-app[bot] | 2021-04-08 15:45:19 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-08 15:45:19 +0000 |
| commit | e4a8b03d94128ccc05dd429756f07247a1f929cc (patch) | |
| tree | a15708e9036506347e2c1772407a85b097f7ad4b /user-contrib | |
| parent | 3bff0b42f5549c371872ddaca1ccd1b1b3b4dce5 (diff) | |
| parent | 45e064836ec1f50300198f89c099b71d0e2059b9 (diff) | |
Merge PR #14093: Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular
Reviewed-by: JasonGross
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 6be5ba80d5..7af530ab0f 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -50,6 +50,12 @@ let q_pose = Pcoq.Entry.create "q_pose" let q_assert = Pcoq.Entry.create "q_assert" end +let () = + let entries = [ + Pcoq.AnyEntry Pltac.ltac2_expr; + ] in + Pcoq.register_grammars_by_name "ltac2" entries + (** Tactic definition *) type tacdef = { |