From 28d45c2413ad24c758fca5cfb00ec4ba20935f39 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 23 Nov 2017 11:38:55 +0100
Subject: Separate vernac controls and regular commands.

Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.

Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.

This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
---
 dev/base_include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index d7059fe74f..4dc9a0bee8 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -193,7 +193,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
+let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
 let parse_tac    = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
-- 
cgit v1.2.3