diff options
Diffstat (limited to 'vernac/vernacextend.ml')
| -rw-r--r-- | vernac/vernacextend.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 2541f73582..05687afd8b 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -42,8 +42,11 @@ and vernac_sideff_type = Names.Id.t list and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) + and solving_tac = bool (** a terminator *) + and anon_abstracting_tac = bool (** abstracting anonymously its result *) + and proof_block_name = string (** open type of delimiters *) type vernac_when = |