diff options
author | 2016-10-08 00:10:55 +0200 | |
---|---|---|
committer | 2016-10-08 00:56:12 +0200 | |
commit | 9bdd8aff92829aaa7c5a45b6e4e5adfa9e8789df (patch) | |
tree | 9e335c08004f01cf4016a11f83ffa1ca07b720c1 /ltac/extraargs.mli | |
parent | d93e8a7e7c9ae08cfedaf4a3db00ae3f9240bfe5 (diff) |
Fix bug #5098: Symmetry broken in HoTT.
We defactorize the in_clause grammar entry to allow parsing of the "symmetry"
tactic when it has no arguments. Beforehand, the clause_dft_concl entry
accepted the empty stream, preventing the definition of symmetry as a mere
identifier.
Diffstat (limited to 'ltac/extraargs.mli')
-rw-r--r-- | ltac/extraargs.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 0cf77935c..b12187e18 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -71,3 +71,8 @@ val pr_by_arg_tac : val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type + +val wit_in_clause : + (Id.t Loc.located Locus.clause_expr, + Id.t Loc.located Locus.clause_expr, + Id.t Locus.clause_expr) Genarg.genarg_type |