From 25b07a6f824654be2041152d904507bc62102986 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 28 Feb 2018 13:45:04 +0100 Subject: Implement the Export Set/Unset feature. This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313. --- vernac/vernacprop.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/vernacprop.ml') diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 44a7a9b15..a837b77a3 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -52,7 +52,7 @@ let is_reset = function | _ -> false let is_debug cmd = match under_control cmd with - | VernacSetOption (["Ltac";"Debug"], _) -> true + | VernacSetOption (_, ["Ltac";"Debug"], _) -> true | _ -> false let is_undo cmd = match under_control cmd with -- cgit v1.2.3