aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index eb410b1e32..11d8a3061f 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -274,6 +274,7 @@ let rec attribute_of_vernac_command = function
| VernacSyntacticDefinition _ -> []
| VernacDeclareImplicits _ -> []
| VernacReserve _ -> []
+ | VernacGeneralizable _ -> []
| VernacSetOpacity _ -> []
| VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand]
| VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) ->