aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/idetop.ml12
-rw-r--r--plugins/funind/g_indfun.mlg2
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--stm/proofBlockDelimiter.ml4
-rw-r--r--stm/stm.ml88
-rw-r--r--stm/stm.mli4
-rw-r--r--stm/vernac_classifier.ml10
-rw-r--r--toplevel/coqloop.ml10
-rw-r--r--toplevel/g_toplevel.mlg10
-rw-r--r--toplevel/vernac.ml11
-rw-r--r--toplevel/vernac.mli2
-rw-r--r--vernac/g_vernac.mlg13
-rw-r--r--vernac/ppvernac.ml10
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/pvernac.mli4
-rw-r--r--vernac/topfmt.ml4
-rw-r--r--vernac/topfmt.mli2
-rw-r--r--vernac/vernacentries.ml2
-rw-r--r--vernac/vernacentries.mli2
-rw-r--r--vernac/vernacexpr.ml11
-rw-r--r--vernac/vernacprop.ml35
21 files changed, 120 insertions, 122 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 38839f3488..ce00ba6d8c 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -64,7 +64,7 @@ let is_known_option cmd = match Vernacprop.under_control cmd with
(** Check whether a command is forbidden in the IDE *)
-let ide_cmd_checks ~last_valid {CAst.loc;v=ast} =
+let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
let user_error s =
try CErrors.user_err ?loc ~hdr:"IDE" (str s)
with e ->
@@ -72,14 +72,14 @@ let ide_cmd_checks ~last_valid {CAst.loc;v=ast} =
let info = Stateid.add info ~valid:last_valid Stateid.dummy in
Exninfo.raise ~info e
in
- if is_debug ast then
+ if is_debug cmd then
user_error "Debug mode not available in the IDE"
-let ide_cmd_warns ~id {CAst.loc;v=ast} =
+let ide_cmd_warns ~id ({ CAst.loc; _ } as cmd) =
let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
- if is_known_option ast then
+ if is_known_option cmd then
warn "Set this option from the IDE menu instead";
- if is_navigation_vernac ast || is_undo ast then
+ if is_navigation_vernac cmd || is_undo cmd then
warn "Use IDE navigation instead"
(** Interpretation (cf. [Ide_intf.interp]) *)
@@ -137,7 +137,7 @@ let annotate phrase =
| None -> Richpp.richpp_of_pp 78 (Pp.mt ())
| Some ast ->
(* XXX: Width should be a parameter of annotate... *)
- Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast.CAst.v)
+ Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
(** Goal display *)
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index a3973732ad..dbfc0fc91d 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -185,7 +185,7 @@ VERNAC COMMAND EXTEND Function
| _,((_,None,_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
- (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+ (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
with
| Vernacextend.VtSideff ids, _ when hard ->
Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 45a4e61846..e15e167ff3 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1518,7 +1518,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
msg
in
@@ -1533,7 +1533,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
CErrors.print reraise
in
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index d13763cdec..2b32838964 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -99,7 +99,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
+ recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
}
| `Not -> `Leaks
@@ -128,7 +128,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
+ recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
}
| `Not -> `Leaks
diff --git a/stm/stm.ml b/stm/stm.ml
index 06bc6e3340..3eb6d03529 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -121,7 +121,6 @@ let async_proofs_workers_extra_env = ref [||]
type aast = {
verbose : bool;
- loc : Loc.t option;
indentation : int;
strlen : int;
mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *)
@@ -1149,12 +1148,12 @@ end
(* Wrapper for Vernacentries.interp to set the feedback id *)
(* It is currently called 19 times, this number should be certainly
reduced... *)
-let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t =
+let stm_vernac_interp ?proof ?route id st { verbose; expr } : Vernacstate.t =
(* The Stm will gain the capability to interpret commmads affecting
the whole document state, such as backtrack, etc... so we start
to design the stm command interpreter now *)
set_id_for_feedback ?route dummy_doc id;
- Aux_file.record_in_aux_set_at ?loc ();
+ Aux_file.record_in_aux_set_at ?loc:expr.CAst.loc ();
(* We need to check if a command should be filtered from
* vernac_entries, as it cannot handle it. This should go away in
* future refactorings.
@@ -1175,7 +1174,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
| VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *)
| _ ->
stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
- try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr)
+ try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr
with e ->
let e = CErrors.push e in
Exninfo.iraise Hooks.(call_process_error_once e)
@@ -1630,8 +1629,8 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_vernac_interp stop
~proof:(pobject, terminator) st
- { verbose = false; loc; indentation = 0; strlen = 0;
- expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
+ { verbose = false; indentation = 0; strlen = 0;
+ expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
ignore(Future.join checked_proof);
end;
(* STATE: Restore the state XXX: handle exn *)
@@ -1780,8 +1779,8 @@ end = struct (* {{{ *)
(* STATE We use the state resulting from reaching start. *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp stop ~proof st
- { verbose = false; loc; indentation = 0; strlen = 0;
- expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
+ { verbose = false; indentation = 0; strlen = 0;
+ expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
`OK proof
end
with e ->
@@ -1793,10 +1792,11 @@ end = struct (* {{{ *)
spc () ++ iprint (e, info))
| Some (_, cur) ->
match VCS.visit cur with
- | { step = `Cmd { cast = { loc } } }
- | { step = `Fork (( { loc }, _, _, _), _) }
- | { step = `Qed ( { qast = { loc } }, _) }
- | { step = `Sideff (ReplayCommand { loc }, _) } ->
+ | { step = `Cmd { cast } }
+ | { step = `Fork (( cast, _, _, _), _) }
+ | { step = `Qed ( { qast = cast }, _) }
+ | { step = `Sideff (ReplayCommand cast, _) } ->
+ let loc = cast.expr.CAst.loc in
let start, stop = Option.cata Loc.unloc (0,0) loc in
msg_warning Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
@@ -2073,14 +2073,14 @@ end = struct (* {{{ *)
f ()
let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
- { indentation; verbose; loc; expr = e; strlen } : unit
+ { indentation; verbose; expr = e; strlen } : unit
=
let e, time, batch, fail =
- let rec find ~time ~batch ~fail = function
- | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e
- | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e
- | VernacFail {CAst.v=e} -> find ~time ~batch ~fail:true e
- | e -> e, time, batch, fail in
+ let rec find ~time ~batch ~fail v = CAst.with_loc_val (fun ?loc -> function
+ | VernacTime (batch,e) -> find ~time:true ~batch ~fail e
+ | VernacRedirect (_,e) -> find ~time ~batch ~fail e
+ | VernacFail e -> find ~time ~batch ~fail:true e
+ | e -> CAst.make ?loc e, time, batch, fail) v in
find ~time:false ~batch:false ~fail:false e in
let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_fail ~st fail (fun () ->
@@ -2094,7 +2094,7 @@ end = struct (* {{{ *)
Future.create_delegate
~name:(Printf.sprintf "subgoal %d" i)
(State.exn_on id ~valid:safe_id) in
- let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) in
+ let t_ast = (i, { indentation; verbose; expr = e; strlen }) in
let t_name = Goal.uid g in
TaskQueue.enqueue_task queue
{ t_state = safe_id; t_state_fb = id;
@@ -2243,7 +2243,7 @@ let collect_proof keep cur hd brkind id =
let name = function
| [] -> no_name
| id :: _ -> Names.Id.to_string id in
- let loc = (snd cur).loc in
+ let loc = (snd cur).expr.CAst.loc in
let is_defined_expr = function
| VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
| _ -> false in
@@ -2309,7 +2309,7 @@ let collect_proof keep cur hd brkind id =
(try
let name, hint = name ids, get_hint_ctx loc in
let t, v = proof_no_using last in
- v.expr <- VernacExpr([], VernacProof(t, Some hint));
+ v.expr <- CAst.map (fun _ -> VernacExpr([], VernacProof(t, Some hint))) v.expr;
`ASync (parent last,accn,name,delegate name)
with Not_found ->
let name = name ids in
@@ -2412,7 +2412,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
(* STATE: We use an updated state with proof *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
Option.iter (fun expr -> ignore(stm_vernac_interp id st {
- verbose = true; loc = None; expr; indentation = 0;
+ verbose = true; expr; indentation = 0;
strlen = 0 } ))
recovery_command
| _ -> assert false
@@ -2532,7 +2532,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| `ASync (block_start, nodes, name, delegate) -> (fun () ->
let keep' = get_vtkeep keep in
let drop_pt = keep' == VtKeepAxiom in
- let block_stop, exn_info, loc = eop, (id, eop), x.loc in
+ let block_stop, exn_info, loc = eop, (id, eop), x.expr.CAst.loc in
log_processing_async id name;
VCS.create_proof_task_box nodes ~qed:id ~block_start;
begin match brinfo, qed.fproof with
@@ -2592,7 +2592,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
log_processing_sync id name reason;
reach eop;
let wall_clock = Unix.gettimeofday () in
- record_pb_time name ?loc:x.loc (wall_clock -. !wall_clock_last_fork);
+ record_pb_time name ?loc:x.expr.CAst.loc (wall_clock -. !wall_clock_last_fork);
let proof =
match keep with
| VtDrop -> None
@@ -2614,7 +2614,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id ?proof st x);
let wall_clock3 = Unix.gettimeofday () in
- Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
+ Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time"
(Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
PG_compat.discard_all ()
), true, true
@@ -2934,7 +2934,7 @@ let get_allow_nested_proofs =
(** [process_transaction] adds a node in the document *)
let process_transaction ~doc ?(newtip=Stateid.fresh ())
- ({ verbose; loc; expr } as x) c =
+ ({ verbose; expr } as x) c =
stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
let vcs = VCS.backup () in
try
@@ -3120,11 +3120,11 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
let get_ast ~doc id =
match VCS.visit id with
- | { step = `Cmd { cast = { loc; expr } } }
- | { step = `Fork (({ loc; expr }, _, _, _), _) }
- | { step = `Sideff ((ReplayCommand {loc; expr}) , _) }
- | { step = `Qed ({ qast = { loc; expr } }, _) } ->
- Some (Loc.tag ?loc expr)
+ | { step = `Cmd { cast = { expr } } }
+ | { step = `Fork (({ expr }, _, _, _), _) }
+ | { step = `Sideff ((ReplayCommand { expr }) , _) }
+ | { step = `Qed ({ qast = { expr } }, _) } ->
+ Some expr
| _ -> None
let stop_worker n = Slaves.cancel_worker n
@@ -3141,8 +3141,8 @@ let parse_sentence ~doc sid ~entry pa =
let ind_len_loc_of_id sid =
if Stateid.equal sid Stateid.initial then None
else match (VCS.visit sid).step with
- | `Cmd { ctac = true; cast = { indentation; strlen; loc } } ->
- Some (indentation, strlen, loc)
+ | `Cmd { ctac = true; cast = { indentation; strlen; expr } } ->
+ Some (indentation, strlen, expr.CAst.loc)
| _ -> None
(* the indentation logic works like this: if the beginning of the
@@ -3169,7 +3169,8 @@ let compute_indentation ?loc sid = Option.cata (fun loc ->
eff_indent, len
) (0, 0) loc
-let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
+let add ~doc ~ontop ?newtip verb ast =
+ let loc = ast.CAst.loc in
let cur_tip = VCS.cur_tip () in
if not (Stateid.equal ontop cur_tip) then
user_err ?loc ~hdr:"Stm.add"
@@ -3179,7 +3180,7 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
let indentation, strlen = compute_indentation ?loc ontop in
(* XXX: Classifiy vernac should be moved inside process transaction *)
let clas = Vernac_classifier.classify_vernac ast in
- let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
+ let aast = { verbose = verb; indentation; strlen; expr = ast } in
match process_transaction ~doc ?newtip aast clas with
| `Ok -> doc, VCS.cur_tip (), `NewTip
| `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ())
@@ -3199,14 +3200,15 @@ let query ~doc ~at ~route s =
let rec loop () =
match parse_sentence ~doc at ~entry:Pvernac.main_entry s with
| None -> ()
- | Some {CAst.loc; v=ast} ->
- let indentation, strlen = compute_indentation ?loc at in
- let st = State.get_cached at in
- let aast = {
- verbose = true; indentation; strlen;
- loc; expr = ast } in
- ignore(stm_vernac_interp ~route at st aast);
- loop ()
+ | Some ast ->
+ let loc = ast.CAst.loc in
+ let indentation, strlen = compute_indentation ?loc at in
+ let st = State.get_cached at in
+ let aast = {
+ verbose = true; indentation; strlen;
+ expr = ast } in
+ ignore(stm_vernac_interp ~route at st aast);
+ loop ()
in
loop ()
)
diff --git a/stm/stm.mli b/stm/stm.mli
index 91651e3534..9d2bf56629 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -111,7 +111,7 @@ val parse_sentence :
If [newtip] is provided, then the returned state id is guaranteed
to be [newtip] *)
val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
- bool -> Vernacexpr.vernac_control CAst.t ->
+ bool -> Vernacexpr.vernac_control ->
doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
(* Returns the proof state before the last tactic that was applied at or before
@@ -175,7 +175,7 @@ val get_current_state : doc:doc -> Stateid.t
val get_ldir : doc:doc -> Names.DirPath.t
(* This returns the node at that position *)
-val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option
+val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option
(* Filename *)
val set_compilation_hints : string -> unit
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 243b5c333d..674b4285d2 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -200,20 +200,20 @@ let classify_vernac e =
try Vernacextend.get_vernac_classifier s l
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
in
- let rec static_control_classifier = function
+ let rec static_control_classifier v = v |> CAst.with_val (function
| VernacExpr (f, e) ->
let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in
static_classifier ~poly e
- | VernacTimeout (_,{v=e}) -> static_control_classifier e
- | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
+ | VernacTimeout (_,e) -> static_control_classifier e
+ | VernacTime (_,e) | VernacRedirect (_, e) ->
static_control_classifier e
- | VernacFail {v=e} -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+ | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match static_control_classifier e with
| ( VtQuery | VtProofStep _ | VtSideff _
| VtMeta), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
VtLater
- | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)
+ | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater))
in
static_control_classifier e
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 087cd67f3a..de447db51f 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -279,7 +279,7 @@ let extract_default_loc loc doc_id sid : Loc.t option =
| None ->
try
let doc = Stm.get_doc doc_id in
- Option.cata fst None Stm.(get_ast ~doc sid)
+ Option.cata (fun {CAst.loc} -> loc) None Stm.(get_ast ~doc sid)
with _ -> loc
(** Coqloop Console feedback handler *)
@@ -383,22 +383,22 @@ let rec vernac_loop ~state =
try
let input = top_buffer.tokens in
match read_sentence ~state input with
- | Some { v = VernacBacktrack(bid,_,_) } ->
+ | Some (VernacBacktrack(bid,_,_)) ->
let bid = Stateid.of_int bid in
let doc, res = Stm.edit_at ~doc:state.doc bid in
assert (res = `NewTip);
let state = { state with doc; sid = bid } in
vernac_loop ~state
- | Some { v = VernacQuit } ->
+ | Some VernacQuit ->
exit 0
- | Some { v = VernacDrop } ->
+ | Some VernacDrop ->
if Mltop.is_ocaml_top()
then (drop_last_doc := Some state; state)
else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state)
- | Some { v = VernacControl c; loc } ->
+ | Some VernacControl { loc; v=c } ->
let nstate = Vernac.process_expr ~state (make ?loc c) in
top_goal_print ~doc:state.doc c state.proof nstate.proof;
vernac_loop ~state:nstate
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index f2025858d7..0cac024300 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -21,7 +21,7 @@ type vernac_toplevel =
| VernacControl of vernac_control
module Toplevel_ : sig
- val vernac_toplevel : vernac_toplevel CAst.t option Entry.t
+ val vernac_toplevel : vernac_toplevel option Entry.t
end = struct
let gec_vernac s = Entry.create ("toplevel:" ^ s)
let vernac_toplevel = gec_vernac "vernac_toplevel"
@@ -34,14 +34,14 @@ open Toplevel_
GRAMMAR EXTEND Gram
GLOBAL: vernac_toplevel;
vernac_toplevel: FIRST
- [ [ IDENT "Drop"; "." -> { Some (CAst.make VernacDrop) }
- | IDENT "Quit"; "." -> { Some (CAst.make VernacQuit) }
+ [ [ IDENT "Drop"; "." -> { Some VernacDrop }
+ | IDENT "Quit"; "." -> { Some VernacQuit }
| IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
- { Some (CAst.make (VernacBacktrack (n,m,p))) }
+ { Some (VernacBacktrack (n,m,p)) }
| cmd = Pvernac.Vernac_.main_entry ->
{ match cmd with
| None -> None
- | Some {CAst.loc; v} -> Some (CAst.make ?loc (VernacControl v)) }
+ | Some v -> Some (VernacControl v) }
]
]
;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6c6379ec5e..c41f16c95b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -20,12 +20,12 @@ open Vernacprop
Use the module Coqtoplevel, which catches these exceptions
(the exceptions are explained only at the toplevel). *)
-let checknav_simple {CAst.loc;v=cmd} =
+let checknav_simple ({ CAst.loc; _ } as cmd) =
if is_navigation_vernac cmd && not (is_reset cmd) then
CErrors.user_err ?loc (str "Navigation commands forbidden in files.")
-let checknav_deep {CAst.loc;v=ast} =
- if is_deep_navigation_vernac ast then
+let checknav_deep ({ CAst.loc; _ } as cmd) =
+ if is_deep_navigation_vernac cmd then
CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.")
(* Echo from a buffer based on position.
@@ -163,10 +163,7 @@ let beautify_pass ~doc ~comments ~ids ~filename =
set the comments, then we call print. This has to be done for
each file. *)
Pputils.beautify_comments := comments;
- List.iter (fun id ->
- Option.iter (fun (loc,ast) ->
- pr_new_syntax ?loc ft_beautify (Some ast))
- (Stm.get_ast ~doc id)) ids;
+ List.iter (fun id -> pr_new_syntax ft_beautify (Stm.get_ast ~doc id)) ids;
(* Is this called so comments at EOF are printed? *)
pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) ft_beautify None;
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 1269540235..197891707c 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -24,7 +24,7 @@ end
expected to handle and print errors in form of exceptions, however
care is taken so the state machine is left in a consistent
state. *)
-val process_expr : state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t
+val process_expr : state:State.t -> Vernacexpr.vernac_control -> State.t
(** [load_vernac echo sid file] Loads [file] on top of [sid], will
echo the commands if [echo] is set. Callers are expected to handle
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3f491d1dd4..d97fb523f7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -77,11 +77,11 @@ let parse_compat_version = let open Flags in function
GRAMMAR EXTEND Gram
GLOBAL: vernac_control gallina_ext noedit_mode subprf;
vernac_control: FIRST
- [ [ IDENT "Time"; c = located_vernac -> { VernacTime (false,c) }
- | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) }
- | IDENT "Timeout"; n = natural; v = located_vernac -> { VernacTimeout(n,v) }
- | IDENT "Fail"; v = located_vernac -> { VernacFail v }
- | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
+ [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) }
+ | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) }
+ | IDENT "Timeout"; n = natural; v = vernac_control -> { CAst.make ~loc @@ VernacTimeout(n,v) }
+ | IDENT "Fail"; v = vernac_control -> { CAst.make ~loc @@ VernacFail v }
+ | v = decorated_vernac -> { let (f, v) = v in CAst.make ~loc @@ VernacExpr(f, v) } ]
]
;
decorated_vernac:
@@ -147,9 +147,6 @@ GRAMMAR EXTEND Gram
] ]
;
- located_vernac:
- [ [ v = vernac_control -> { CAst.make ~loc v } ] ]
- ;
END
{
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 4e4d431e89..327efcda2b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1262,15 +1262,15 @@ let pr_vernac_attributes =
let rec pr_vernac_control v =
let return = tag_vernac v in
- match v with
+ match v.v with
| VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v'
- | VernacTime (_,{v}) ->
+ | VernacTime (_,v) ->
return (keyword "Time" ++ spc() ++ pr_vernac_control v)
- | VernacRedirect (s, {v}) ->
+ | VernacRedirect (s, v) ->
return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
- | VernacTimeout(n,{v}) ->
+ | VernacTimeout(n,v) ->
return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
- | VernacFail {v} ->
+ | VernacFail v->
return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
let pr_vernac v =
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index d474ef8637..4d9157089c 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -52,7 +52,7 @@ module Vernac_ =
let () =
let open Extend in
- let act_vernac v loc = Some CAst.(make ~loc v) in
+ let act_vernac v loc = Some v in
let act_eoi _ loc = None in
let rule = [
Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 4bf7c9f7bd..41a2e7fd6f 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -26,7 +26,7 @@ module Vernac_ :
val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
val noedit_mode : vernac_expr Entry.t
val command_entry : vernac_expr Entry.t
- val main_entry : vernac_control CAst.t option Entry.t
+ val main_entry : vernac_control option Entry.t
val red_expr : raw_red_expr Entry.t
val hint_info : Hints.hint_info_expr Entry.t
end
@@ -40,7 +40,7 @@ module Unsafe : sig
end
(** The main entry: reads an optional vernac command *)
-val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t
+val main_entry : proof_mode option -> vernac_control option Entry.t
(** Grammar entry for tactics: proof mode(s).
By default Coq's grammar has an empty entry (non-terminal) for
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 7bc3264968..118c126970 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -425,7 +425,7 @@ let with_output_to_file fname func input =
(* For coqtop -time, we display the position in the file,
and a glimpse of the executed command *)
-let pr_cmd_header {CAst.loc;v=com} =
+let pr_cmd_header com =
let shorten s =
if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
in
@@ -435,7 +435,7 @@ let pr_cmd_header {CAst.loc;v=com} =
| x -> x
) s
in
- let (start,stop) = Option.cata Loc.unloc (0,0) loc in
+ let (start,stop) = Option.cata Loc.unloc (0,0) com.CAst.loc in
let safe_pr_vernac x =
try Ppvernac.pr_vernac x
with e -> str (Printexc.to_string e) in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index a1e289cd5a..3d522a9e0f 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -73,4 +73,4 @@ val print_err_exn : exn -> unit
redirected to a file [file] *)
val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t
+val pr_cmd_header : Vernacexpr.vernac_control -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fa170e4104..0f6374c506 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2599,7 +2599,7 @@ and vernac_load ?proof ~verbosely ~st fname =
CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
pstate
-and interp_control ?proof ~st = function
+and interp_control ?proof ~st v = match v with
| { v=VernacExpr (atts, cmd) } ->
interp_expr ?proof ~atts ~st cmd
| { v=VernacFail v } ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 71cc29b6e1..12451370c8 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -23,7 +23,7 @@ val vernac_require :
val interp :
?verbosely:bool ->
?proof:Proof_global.closed_proof ->
- st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t
+ st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index d0dae1aa53..99b457effe 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -398,11 +398,12 @@ type nonrec vernac_expr =
(* For extension *)
| VernacExtend of extend_name * Genarg.raw_generic_argument list
-type vernac_control =
+type vernac_control_r =
| VernacExpr of Attributes.vernac_flags * vernac_expr
(* boolean is true when the `-time` batch-mode command line flag was set.
the flag is used to print differently in `-time` vs `Time foo` *)
- | VernacTime of bool * vernac_control CAst.t
- | VernacRedirect of string * vernac_control CAst.t
- | VernacTimeout of int * vernac_control CAst.t
- | VernacFail of vernac_control CAst.t
+ | VernacTime of bool * vernac_control
+ | VernacRedirect of string * vernac_control
+ | VernacTimeout of int * vernac_control
+ | VernacFail of vernac_control
+and vernac_control = vernac_control_r CAst.t
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 704c5b2170..b3490c7dc6 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,19 +13,20 @@
open Vernacexpr
-let rec under_control = function
+let rec under_control v = v |> CAst.with_val (function
| VernacExpr (_, c) -> c
- | VernacRedirect (_,{CAst.v=c})
- | VernacTime (_,{CAst.v=c})
- | VernacFail {CAst.v=c}
- | VernacTimeout (_,{CAst.v=c}) -> under_control c
+ | VernacRedirect (_,c)
+ | VernacTime (_,c)
+ | VernacFail c
+ | VernacTimeout (_,c) -> under_control c
+ )
-let rec has_Fail = function
+let rec has_Fail v = v |> CAst.with_val (function
| VernacExpr _ -> false
- | VernacRedirect (_,{CAst.v=c})
- | VernacTime (_,{CAst.v=c})
- | VernacTimeout (_,{CAst.v=c}) -> has_Fail c
- | VernacFail _ -> true
+ | VernacRedirect (_,c)
+ | VernacTime (_,c)
+ | VernacTimeout (_,c) -> has_Fail c
+ | VernacFail _ -> true)
(* Navigation commands are allowed in a coqtop session but not in a .v file *)
let is_navigation_vernac_expr = function
@@ -38,17 +39,17 @@ let is_navigation_vernac_expr = function
let is_navigation_vernac c =
is_navigation_vernac_expr (under_control c)
-let rec is_deep_navigation_vernac = function
- | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c
- | VernacRedirect (_, {CAst.v=c})
- | VernacTimeout (_,{CAst.v=c}) | VernacFail {CAst.v=c} -> is_navigation_vernac c
- | VernacExpr _ -> false
+let rec is_deep_navigation_vernac v = v |> CAst.with_val (function
+ | VernacTime (_,c) -> is_deep_navigation_vernac c
+ | VernacRedirect (_, c)
+ | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c
+ | VernacExpr _ -> false)
(* NB: Reset is now allowed again as asked by A. Chlipala *)
-let is_reset = function
+let is_reset = CAst.with_val (function
| VernacExpr ( _, VernacResetInitial)
| VernacExpr (_, VernacResetName _) -> true
- | _ -> false
+ | _ -> false)
let is_debug cmd = match under_control cmd with
| VernacSetOption (_, ["Ltac";"Debug"], _) -> true
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 06:40:23 +0000