diff options
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r-- | vernac/vernacentries.ml | 53 |
1 files changed, 26 insertions, 27 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ae62fcfeb..814dc1411 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1959,11 +1959,6 @@ let interp ?proof ~atts ~st c = (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - (* Handled elsewhere *) - | VernacProgram _ - | VernacPolymorphic _ - | VernacLocal _ -> assert false - (* Syntax *) | VernacSyntaxExtension (infix, sl) -> vernac_syntax_extension atts infix sl @@ -2200,10 +2195,31 @@ let with_fail st b f = let interp ?(verbosely=true) ?proof ~st (loc,c) = let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in + let flags f atts = + List.fold_left + (fun (polymorphism, atts) f -> + match f with + | VernacProgram when not atts.program -> + (polymorphism, { atts with program = true }) + | VernacProgram -> + user_err Pp.(str "Program mode specified twice") + | VernacPolymorphic b when polymorphism = None -> + (Some b, atts) + | VernacPolymorphic _ -> + user_err Pp.(str "Polymorphism specified twice") + | VernacLocal b when Option.is_empty atts.locality -> + (polymorphism, { atts with locality = Some b }) + | VernacLocal _ -> + user_err Pp.(str "Locality specified twice") + ) + (None, atts) + f + in let rec control = function - | VernacExpr v -> - let atts = { loc; locality = None; polymorphic = false; program = orig_program_mode; } in - aux ~atts v + | VernacExpr (f, v) -> + let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in + aux ~polymorphism ~atts v + | VernacFail v -> with_fail st true (fun () -> control v) | VernacTimeout (n,v) -> current_timeout := Some n; control v @@ -2212,25 +2228,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | VernacTime (batch, (_loc,v)) -> System.with_time ~batch control v; - and aux ?polymorphism ~atts = function - - | VernacProgram c when not atts.program -> - aux ?polymorphism ~atts:{ atts with program = true } c - - | VernacProgram _ -> - user_err Pp.(str "Program mode specified twice") - - | VernacPolymorphic (b, c) when polymorphism = None -> - aux ~polymorphism:b ~atts:atts c - - | VernacPolymorphic (b, c) -> - user_err Pp.(str "Polymorphism specified twice") - - | VernacLocal (b, c) when Option.is_empty atts.locality -> - aux ?polymorphism ~atts:{atts with locality = Some b} c - - | VernacLocal _ -> - user_err Pp.(str "Locality specified twice") + and aux ~polymorphism ~atts : _ -> unit = + function | VernacLoad (_,fname) -> vernac_load control fname |