diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 15:35:13 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-21 16:09:29 -0500 |
| commit | 4dd2102b7b12efb3ff7805aab3b7f318c6e3f989 (patch) | |
| tree | 1c325b75c69fd8a4f8e8fff9c4fce9125c3fdbb1 /parsing/pcoq.mli | |
| parent | e1f2a1b97bb61e9c5ebaffda55a3be1ea3267c6b (diff) | |
[parsing] Track need to reinit by typing
This PR is in preparation of #9067 (together with #11647) .
Before this PR, `grammar_extend` always took an optional `reinit`
argument, even if it was never set to `Some ...`. Indeed, there is a
single case where reinit is needed; we track it now by using a
different extension rule constructor.
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 404fbdb4fd..f2fc007a7b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -225,7 +225,7 @@ type 'a extend_statement = Gramlib.Gramext.position option * 'a single_extend_statement list -val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit +val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) @@ -242,7 +242,8 @@ type 'a grammar_command marshallable. *) type extend_rule = -| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule +| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t (** Grammar extension entry point. Given some ['a] and a current grammar state, |