From ab8e47207245277cb5b92b80a92ae78ede5bfafe Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 12 Dec 2017 15:32:59 +0000 Subject: [vernac] vernac_expr no longer recursive --- vernac/vernacprop.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac/vernacprop.ml') diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 4fdc78dd2..3932d1c7b 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -12,14 +12,14 @@ open Vernacexpr let rec under_control = function - | VernacExpr c -> c + | VernacExpr (_, c) -> c | VernacRedirect (_,(_,c)) | VernacTime (_,(_,c)) | VernacFail c | VernacTimeout (_,c) -> under_control c let rec has_Fail = function - | VernacExpr c -> false + | VernacExpr _ -> false | VernacRedirect (_,(_,c)) | VernacTime (_,(_,c)) | VernacTimeout (_,c) -> has_Fail c @@ -45,8 +45,8 @@ let rec is_deep_navigation_vernac = function (* NB: Reset is now allowed again as asked by A. Chlipala *) let is_reset = function - | VernacExpr VernacResetInitial - | VernacExpr (VernacResetName _) -> true + | VernacExpr ( _, VernacResetInitial) + | VernacExpr (_, VernacResetName _) -> true | _ -> false let is_debug cmd = match under_control cmd with -- cgit v1.2.3