aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli9
-rw-r--r--parsing/g_vernac.ml49
-rw-r--r--printing/ppvernac.ml15
-rw-r--r--stm/stm.ml4
-rw-r--r--stm/texmacspp.ml8
-rw-r--r--stm/vernac_classifier.ml11
-rw-r--r--toplevel/vernac.ml8
-rw-r--r--toplevel/vernacentries.ml19
8 files changed, 31 insertions, 52 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 99264dbe0..32c0f2975 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -287,8 +287,8 @@ type module_binder = bool option * lident list * module_ast_inl
type vernac_expr =
(* Control *)
| VernacLoad of verbose_flag * string
- | VernacTime of vernac_list
- | VernacRedirect of string * vernac_list
+ | VernacTime of located_vernac_expr
+ | VernacRedirect of string * located_vernac_expr
| VernacTimeout of int * vernac_expr
| VernacFail of vernac_expr
| VernacError of exn (* always fails *)
@@ -386,8 +386,7 @@ type vernac_expr =
| VernacBackTo of int
(* Commands *)
- | VernacDeclareTacticDefinition of
- (rec_flag * (reference * bool * raw_tactic_expr) list)
+ | VernacDeclareTacticDefinition of (reference * bool * raw_tactic_expr) list
| VernacCreateHintDb of string * bool
| VernacRemoveHints of string list * reference list
| VernacHints of obsolete_locality * string list * hints_expr
@@ -455,8 +454,6 @@ type vernac_expr =
| VernacPolymorphic of bool * vernac_expr
| VernacLocal of bool * vernac_expr
-and vernac_list = located_vernac_expr list
-
and located_vernac_expr = Loc.t * vernac_expr
(* A vernac classifier has to tell if a command:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 1f9f57f69..975dee934 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -89,8 +89,8 @@ let default_command_entry =
GEXTEND Gram
GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
vernac: FIRST
- [ [ IDENT "Time"; l = vernac_list -> VernacTime l
- | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l)
+ [ [ IDENT "Time"; c = located_vernac -> VernacTime c
+ | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
| IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
| IDENT "Fail"; v = vernac -> VernacFail v
@@ -128,9 +128,6 @@ GEXTEND Gram
| c = subprf -> c
] ]
;
- vernac_list:
- [ [ c = located_vernac -> [c] ] ]
- ;
vernac_aux: LAST
[ [ prfcom = default_command_entry -> prfcom ] ]
;
@@ -806,7 +803,7 @@ GEXTEND Gram
command:
[ [ IDENT "Ltac";
l = LIST1 tacdef_body SEP "with" ->
- VernacDeclareTacticDefinition (true, l)
+ VernacDeclareTacticDefinition l
| IDENT "Comments"; l = LIST0 comment -> VernacComments l
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d79fb4561..0f065e251 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -635,10 +635,10 @@ module Make
else
spc() ++ qs s
)
- | VernacTime v ->
- return (keyword "Time" ++ spc() ++ pr_vernac_list v)
- | VernacRedirect (s, v) ->
- return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v)
+ | VernacTime (_,v) ->
+ return (keyword "Time" ++ spc() ++ pr_vernac v)
+ | VernacRedirect (s, (_,v)) ->
+ return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac v)
| VernacTimeout(n,v) ->
return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
| VernacFail v ->
@@ -1030,7 +1030,7 @@ module Make
return (keyword "Cd" ++ pr_opt qs s)
(* Commands *)
- | VernacDeclareTacticDefinition (rc,l) ->
+ | VernacDeclareTacticDefinition l ->
let pr_tac_body (id, redef, body) =
let idl, body =
match body with
@@ -1262,11 +1262,6 @@ module Make
| VernacEndSubproof ->
return (str "}")
- and pr_vernac_list l =
- hov 2 (str"[" ++ spc() ++
- prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l
- ++ spc() ++ str"]")
-
and pr_extend s cl =
let pr_arg a =
try pr_gen a
diff --git a/stm/stm.ml b/stm/stm.ml
index ea669b159..e0e787503 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -86,7 +86,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
| VernacResetName _ | VernacResetInitial | VernacBack _
| VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
| VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
- | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el
+ | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
| _ -> false in
if internal_command expr then begin
prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
@@ -1501,7 +1501,7 @@ end = struct (* {{{ *)
let e, etac, time, fail =
let rec find time fail = function
| VernacSolve(_,_,re,b) -> re, b, time, fail
- | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e
+ | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
| VernacFail e -> find time true e
| _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
Hooks.call Hooks.with_fail fail (fun () ->
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index b91208041..95aaea6f0 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -487,12 +487,12 @@ let rec tmpp v loc =
(* Control *)
| VernacLoad (verbose,f) ->
xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
- | VernacTime l ->
+ | VernacTime (loc,e) ->
xmlApply loc (Element("time",[],[]) ::
- List.map (fun(loc,e) ->tmpp e loc) l)
- | VernacRedirect (s, l) ->
+ [tmpp e loc])
+ | VernacRedirect (s, (loc,e)) ->
xmlApply loc (Element("redirect",["path", s],[]) ::
- List.map (fun(loc,e) ->tmpp e loc) l)
+ [tmpp e loc])
| VernacTimeout (s,e) ->
xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
[tmpp e loc])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index a898c687b..32358c592 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -86,7 +86,7 @@ let rec classify_vernac e =
make_polymorphic (classify_vernac e)
else classify_vernac e
| VernacTimeout (_,e) -> classify_vernac e
- | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e
+ | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
@@ -175,7 +175,7 @@ let rec classify_vernac e =
| VernacRegister _
| VernacNameSectionHypSet _
| VernacComments _ -> VtSideff [], VtLater
- | VernacDeclareTacticDefinition (_,l) ->
+ | VernacDeclareTacticDefinition l ->
let open Libnames in
VtSideff (List.map (function
| (Ident (_,r),_,_) -> r
@@ -217,13 +217,6 @@ let rec classify_vernac e =
| VernacExtend (s,l) ->
try List.assoc s !classifiers l ()
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
- and classify_vernac_list = function
- (* spiwack: It would be better to define a monoid on classifiers.
- So that the classifier of the list would be the composition of
- the classifier of the individual commands. Currently: special
- case for singleton lists.*)
- | [_,c] -> static_classifier c
- | l -> VtUnknown,VtNow
in
let res = static_classifier e in
if Flags.is_universe_polymorphism () then
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a0cd618e9..f61129045 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,9 +27,9 @@ let rec is_navigation_vernac = function
| VernacBacktrack _
| VernacBackTo _
| VernacBack _ -> true
- | VernacRedirect (_, l) | VernacTime l ->
- List.exists
- (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
+ | VernacRedirect (_, (_,c))
+ | VernacTime (_,c) ->
+ is_navigation_vernac c (* Time Back* is harmless *)
| c -> is_deep_navigation_vernac c
and is_deep_navigation_vernac = function
@@ -229,7 +229,7 @@ let rec vernac_com verbose checknav (loc,com) =
checknav loc com;
if do_beautify () then pr_new_syntax loc (Some com);
if !Flags.time then display_cmd_header loc com;
- let com = if !Flags.time then VernacTime [loc,com] else com in
+ let com = if !Flags.time then VernacTime (loc,com) else com in
interp com
with reraise ->
let (reraise, info) = Errors.push reraise in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b3512ffde..2f435adfe 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -972,7 +972,7 @@ let make_absolute_name ident repl =
in
NewTac id
-let register_ltac local isrec tacl =
+let register_ltac local tacl =
let map (ident, repl, body) =
let name = make_absolute_name ident repl in
(name, body)
@@ -983,8 +983,7 @@ let register_ltac local isrec tacl =
| UpdateTac _ -> accu
| NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
in
- if isrec then List.fold_left fold [] rfun
- else []
+ List.fold_left fold [] rfun
in
let ist = Tacintern.make_empty_glob_sign () in
let map (name, body) =
@@ -1010,9 +1009,9 @@ let register_ltac local isrec tacl =
in
List.iter iter defs
-let vernac_declare_tactic_definition locality (x,def) =
+let vernac_declare_tactic_definition locality def =
let local = make_module_locality locality in
- register_ltac local x def
+ register_ltac local def
let vernac_create_hintdb locality id b =
let local = make_module_locality locality in
@@ -2132,11 +2131,11 @@ let interp ?(verbosely=true) ?proof (loc,c) =
| VernacTimeout (n,v) ->
current_timeout := Some n;
aux ?locality ?polymorphism isprogcmd v
- | VernacRedirect (s, v) ->
- Pp.with_output_to_file s (aux_list ?locality ?polymorphism isprogcmd) v;
- | VernacTime v ->
+ | VernacRedirect (s, (_,v)) ->
+ Pp.with_output_to_file s (aux false) v
+ | VernacTime (_,v) ->
System.with_time !Flags.time
- (aux_list ?locality ?polymorphism isprogcmd) v;
+ (aux ?locality ?polymorphism isprogcmd) v;
| VernacLoad (_,fname) -> vernac_load (aux false) fname
| c ->
check_vernac_supports_locality c locality;
@@ -2164,8 +2163,6 @@ let interp ?(verbosely=true) ?proof (loc,c) =
Flags.program_mode := orig_program_mode;
ignore (Flags.use_polymorphic_flag ());
iraise e
- and aux_list ?locality ?polymorphism isprogcmd l =
- List.iter (aux false) (List.map snd l)
in
if verbosely then Flags.verbosely (aux false) c
else aux false c
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 14:32:34 +0000