diff options
| author | Maxime Dénès | 2015-07-02 16:16:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-07-02 16:16:46 +0200 |
| commit | 27de0f2d7e5cd0cc4b221413dfe3c7b739104350 (patch) | |
| tree | a42625106f71295ebc2011b797603cd1b3b8ec83 /intf | |
| parent | a28d9981e5baf812de14e62de8d904e545e804e5 (diff) | |
| parent | 44f45f58dc0a169286c9fcfa7d2edbc8bc04673b (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 5 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 9 |
2 files changed, 13 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 86714ca4d5..ce53680f38 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -94,8 +94,13 @@ type ('a,'t) match_rule = | Pat of 'a match_context_hyps list * 'a match_pattern * 't | All of 't +(** Extension indentifiers for the TACTIC EXTEND mechanism. *) type ml_tactic_name = { + (** Name of the plugin where the tactic is defined, typically coming from a + DECLARE PLUGIN statement in the source. *) mltac_plugin : string; + (** Name of the tactic entry where the tactic is defined, typically found + after the TACTIC EXTEND statement in the source. *) mltac_tactic : string; } diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 0ca3bb35f6..b72577e1e0 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -225,7 +225,14 @@ type section_subset_expr = type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr -type extend_name = string * int +(** Extension identifiers for the VERNAC EXTEND mechanism. *) +type extend_name = + (** Name of the vernac entry where the tactic is defined, typically found + after the VERNAC EXTEND statement in the source. *) + string * + (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch + is given an offset, starting from zero. *) + int (* This type allows registering the inlining of constants in native compiler. It will be extended with primitive inductive types and operators *) |