diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 11 | ||||
| -rw-r--r-- | stm/lemmas.ml | 45 | ||||
| -rw-r--r-- | stm/lemmas.mli | 9 | ||||
| -rw-r--r-- | stm/spawned.ml | 13 | ||||
| -rw-r--r-- | stm/stm.ml | 175 | ||||
| -rw-r--r-- | stm/stm.mli | 9 | ||||
| -rw-r--r-- | stm/texmacspp.ml | 38 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 34 |
8 files changed, 160 insertions, 174 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 1214fc4da9..a7b381ad62 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -60,9 +60,7 @@ module Make(T : Task) = struct type more_data = | MoreDataUnivLevel of Univ.universe_level list - - let request_expiry_of_task (t, c) = T.request_of_task t, c - + let slave_respond (Request r) = let res = T.perform r in Response res @@ -106,7 +104,8 @@ module Make(T : Task) = struct marshal_err ("unmarshal_more_data: "^s) let report_status ?(id = !Flags.async_proofs_worker_id) s = - Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s)) + let open Feedback in + feedback ~id:(State Stateid.initial) (WorkerStatus(id, s)) module Worker = Spawn.Sync(struct end) @@ -304,8 +303,8 @@ module Make(T : Task) = struct let main_loop () = let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback fb) []; flush oc in - Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); - Pp.log_via_feedback (); + Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); + Feedback.set_logger Feedback.feedback_logger; Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 5b205e79ef..0a63a3a0fe 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -31,6 +31,7 @@ open Reductionops open Constrexpr open Constrintern open Impargs +open Context.Rel.Declaration type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a let mk_hook hook = hook @@ -44,7 +45,8 @@ let call_hook fix_exn hook l c = let retrieve_first_recthm = function | VarRef id -> - (pi2 (Global.lookup_named id),variable_opacity id) + let open Context.Named.Declaration in + (get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in (Global.body_of_constant_body cb, is_opaque cb) @@ -107,11 +109,12 @@ let find_mutually_recursive_statements thms = (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) (Global.env()) hyps in let ind_hyps = - List.flatten (List.map_i (fun i (_,b,t) -> + List.flatten (List.map_i (fun i decl -> + let t = get_type decl in match kind_of_term t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in - mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b -> + mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl -> [ind,x,i] | _ -> []) 0 (List.rev whnf_hyp_hds)) in @@ -147,7 +150,7 @@ let find_mutually_recursive_statements thms = assert (List.is_empty rest); (* One occ. of common coind ccls and no common inductive hyps *) if not (List.is_empty common_same_indhyp) then - if_verbose msg_info (str "Assuming mutual coinductive statements."); + if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); flush_all (); indccl, true, [] | [], _::_ -> @@ -155,7 +158,7 @@ let find_mutually_recursive_statements thms = | ind :: _ -> if List.distinct_f ind_ord (List.map pi1 ind) then - if_verbose msg_info + if_verbose Feedback.msg_info (strbrk ("Coinductive statements do not follow the order of "^ "definition, assuming the proof to be by induction.")); @@ -303,7 +306,7 @@ let admit (id,k,e) pl hook () = let () = match k with | Global, _, _ -> () | Local, _, _ | Discharge, _, _ -> - msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ + Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ str "declared as an axiom.") in let () = assumption_message id in @@ -329,10 +332,11 @@ let check_exist = ) let universe_proof_terminator compute_guard hook = - let open Proof_global in function + let open Proof_global in + make_terminator begin function | Admitted (id,k,pe,(ctx,pl)) -> admit (id,k,pe) pl (hook (Some ctx)) (); - Pp.feedback Feedback.AddedAxiom + Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff, exports = match opaque with | Vernacexpr.Transparent -> false, true, [] @@ -347,12 +351,16 @@ let universe_proof_terminator compute_guard hook = save_anonymous_with_strength ~export_seff proof kind id end; check_exist exports + end let standard_proof_terminator compute_guard hook = universe_proof_terminator compute_guard (fun _ -> hook) -let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = standard_proof_terminator compute_guard hook in +let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = match terminator with + | None -> standard_proof_terminator compute_guard hook + | Some terminator -> terminator compute_guard hook + in let sign = match sign with | Some sign -> sign @@ -361,8 +369,11 @@ let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = !start_hook c; Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator -let start_proof_univs id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = universe_proof_terminator compute_guard hook in +let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = match terminator with + | None -> universe_proof_terminator compute_guard hook + | Some terminator -> terminator compute_guard hook + in let sign = match sign with | Some sign -> sign @@ -392,7 +403,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = | Anonymous -> Tactics.intro) (List.rev ids) in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> - let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in + let rec_tac = rec_tac_initializer finite guard thms snl in Some (match init_tac with | None -> if Flags.is_auto_intros () then @@ -422,7 +433,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let body,opaq = retrieve_first_recthm ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in + let ctx = UState.context_set (*FIXME*) ctx in let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in @@ -442,7 +453,7 @@ let start_proof_com kind thms hook = let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); - let ids = List.map pi1 ctx in + let ids = List.map get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), @@ -494,7 +505,7 @@ let save_proof ?proof = function Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), (universes, Some binders)) in - Proof_global.get_terminator() pe + Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (is_opaque,idopt) -> let (proof_obj,terminator) = match proof with @@ -504,7 +515,7 @@ let save_proof ?proof = function in (* if the proof is given explicitly, nothing has to be deleted *) if Option.is_empty proof then Pfedit.delete_current_proof (); - terminator (Proof_global.Proved (is_opaque,idopt,proof_obj)) + Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) (* Miscellaneous *) diff --git a/stm/lemmas.mli b/stm/lemmas.mli index ca6af9a3fa..f751598f04 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -9,8 +9,6 @@ open Names open Term open Decl_kinds -open Constrexpr -open Vernacexpr open Pfedit type 'a declaration_hook @@ -24,11 +22,13 @@ val call_hook : val set_start_hook : (types -> unit) -> unit val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit @@ -43,6 +43,11 @@ val start_proof_with_initialization : (types * (Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit +val universe_proof_terminator : + Proof_global.lemma_possible_guards -> + (Evd.evar_universe_context option -> unit declaration_hook) -> + Proof_global.proof_terminator + val standard_proof_terminator : Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator diff --git a/stm/spawned.ml b/stm/spawned.ml index c6df872679..2eae6f5e24 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -13,19 +13,6 @@ let prerr_endline s = if !Flags.debug then begin pr_err s end else () type chandescr = AnonPipe | Socket of string * int * int -let handshake cin cout = - try - match input_value cin with - | Hello(v, pid) when v = proto_version -> - prerr_endline (Printf.sprintf "Handshake with %d OK" pid); - output_value cout (Hello (proto_version,Unix.getpid ())); flush cout - | _ -> raise (Failure "handshake protocol") - with - | Failure s | Invalid_argument s | Sys_error s -> - pr_err ("Handshake failed: " ^ s); raise (Failure "handshake") - | End_of_file -> - pr_err "Handshake failed: End_of_file"; raise (Failure "handshake") - let open_bin_connection h pr pw = let open Unix in let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in diff --git a/stm/stm.ml b/stm/stm.ml index 95cecb7fe2..28e749d5c8 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -18,6 +18,7 @@ open Names open Util open Ppvernac open Vernac_classifier +open Feedback module Hooks = struct @@ -27,28 +28,23 @@ let with_fail, with_fail_hook = Hook.make () let state_computed, state_computed_hook = Hook.make ~default:(fun state_id ~in_cache -> - feedback ~state_id Feedback.Processed) () + feedback ~id:(State state_id) Processed) () let state_ready, state_ready_hook = Hook.make ~default:(fun state_id -> ()) () let forward_feedback, forward_feedback_hook = Hook.make ~default:(function - | { Feedback.id = Feedback.Edit edit_id; route; contents } -> - feedback ~edit_id ~route contents - | { Feedback.id = Feedback.State state_id; route; contents } -> - feedback ~state_id ~route contents) () + | { id = id; route; contents } -> + feedback ~id:id ~route contents) () let parse_error, parse_error_hook = Hook.make - ~default:(function - | Feedback.Edit edit_id -> fun loc msg -> - feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg)) - | Feedback.State state_id -> fun loc msg -> - feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) () + ~default:(fun id loc msg -> + feedback ~id (ErrorMsg (loc, Pp.string_of_ppcmds msg))) () let execution_error, execution_error_hook = Hook.make ~default:(fun state_id loc msg -> - feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) () + feedback ~id:(State state_id) (ErrorMsg (loc, Pp.string_of_ppcmds msg))) () let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -83,6 +79,8 @@ let async_proofs_workers_extra_env = ref [||] type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr } let pr_ast { expr } = pr_vernac expr +let default_proof_mode () = Proof_global.get_default_proof_mode_name () + (* Commands piercing opaque *) let may_pierce_opaque = function | { expr = VernacPrint (PrintName _) } -> true @@ -101,14 +99,14 @@ 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 (fun () -> "ignoring " ^ string_of_ppcmds(pr_vernac expr)) + prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) end else begin - set_id_for_feedback ?route (Feedback.State id); + set_id_for_feedback ?route (State id); Aux_file.record_in_aux_set_at loc; - prerr_endline (fun () -> "interpreting " ^ string_of_ppcmds(pr_vernac expr)); + prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)) with e -> let e = Errors.push e in @@ -118,8 +116,8 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = (* Wrapper for Vernac.parse_sentence to set the feedback id *) let vernac_parse ?newtip ?route eid s = let feedback_id = - if Option.is_empty newtip then Feedback.Edit eid - else Feedback.State (Option.get newtip) in + if Option.is_empty newtip then Edit eid + else State (Option.get newtip) in set_id_for_feedback ?route feedback_id; let pa = Pcoq.Gram.parsable (Stream.of_string s) in Flags.with_option Flags.we_are_parsing (fun () -> @@ -136,7 +134,7 @@ let vernac_parse ?newtip ?route eid s = let pr_open_cur_subgoals () = try Printer.pr_open_subgoals () - with Proof_global.NoCurrentProof -> str"" + with Proof_global.NoCurrentProof -> Pp.str "" let update_global_env () = if Proof_global.there_are_pending_proofs () then @@ -154,7 +152,7 @@ type branch_type = proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ] type cmd_t = { ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *) - ceff : bool; (* is a side-effecting command *) + ceff : bool; (* is a side-effecting command in the middle of a proof *) cast : ast; cids : Id.t list; cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] } @@ -186,7 +184,7 @@ type visit = { step : step; next : Stateid.t } (* Parts of the system state that are morally part of the proof state *) let summary_pstate = [ Evarutil.meta_counter_summary_name; - Evarutil.evar_counter_summary_name; + Evd.evar_counter_summary_name; "program-tcc-table" ] type state = { system : States.state; @@ -228,7 +226,7 @@ end = struct (* {{{ *) let find_proof_at_depth vcs pl = try List.find (function | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl - | _, { Vcs_.kind = `Edit _ } -> anomaly(str"find_proof_at_depth") + | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth") | _ -> false) (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs)) with Not_found -> failwith "find_proof_at_depth" @@ -236,9 +234,9 @@ end = struct (* {{{ *) exception Expired let visit vcs id = if Stateid.equal id Stateid.initial then - anomaly(str"Visiting the initial state id") + anomaly(Pp.str "Visiting the initial state id") else if Stateid.equal id Stateid.dummy then - anomaly(str"Visiting the dummy state id") + anomaly(Pp.str "Visiting the dummy state id") else try match Vcs_.Dag.from_node (Vcs_.dag vcs) id with @@ -254,7 +252,7 @@ end = struct (* {{{ *) | [n, Sideff (Some x); p, Noop] | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n } | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n} - | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id)) + | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id)) with Not_found -> raise Expired end (* }}} *) @@ -313,7 +311,7 @@ module VCS : sig val proof_nesting : unit -> int val checkout_shallowest_proof_branch : unit -> unit - val propagate_sideff : ast option -> unit + val propagate_sideff : replay:ast option -> unit val gc : unit -> unit @@ -337,10 +335,10 @@ end = struct (* {{{ *) "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in let string_of_transaction = function | Cmd { cast = t } | Fork (t, _,_,_) -> - (try string_of_ppcmds (pr_ast t) with _ -> "ERR") + (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff (Some t) -> sprintf "Sideff(%s)" - (try string_of_ppcmds (pr_ast t) with _ -> "ERR") + (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff None -> "EnvChange" | Noop -> " " | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id) @@ -482,10 +480,10 @@ end = struct (* {{{ *) Proof_global.activate_proof_mode mode with Failure _ -> checkout Branch.master; - Proof_global.disactivate_proof_mode "Classic" + Proof_global.disactivate_current_proof_mode () (* copies the transaction on every open branch *) - let propagate_sideff t = + let propagate_sideff ~replay:t = List.iter (fun b -> checkout b; let id = new_node () in @@ -649,10 +647,9 @@ end = struct (* {{{ *) States.unfreeze system; Proof_global.unfreeze proof (* hack to make futures functional *) - let in_t, out_t = Dyn.create "state4future" let () = Future.set_freeze - (fun () -> in_t (freeze_global_state `No, !cur_id)) - (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i) + (fun () -> Obj.magic (freeze_global_state `No, !cur_id)) + (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i) type frozen_state = state type proof_part = @@ -739,7 +736,7 @@ end = struct (* {{{ *) let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id = - feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id); + feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id); let str_id = Stateid.to_string id in if is_cached id && not redefine then anomaly (str"defining state "++str str_id++str" twice"); @@ -1061,7 +1058,7 @@ end = struct (* {{{ *) List.iter (fun (id,s) -> State.assign id s) l; `End | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop }, RespBuiltProof (pl, time) -> - feedback (Feedback.InProgress ~-1); + feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time t_name t_loc time; if !Flags.async_proofs_full || t_drop @@ -1069,7 +1066,7 @@ end = struct (* {{{ *) else `End | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> - feedback (Feedback.InProgress ~-1); + feedback (InProgress ~-1); let info = Stateid.add ~valid Exninfo.null e_error_at in let e = (RemoteException e_msg, info) in t_assign (`Exn e); @@ -1085,7 +1082,7 @@ end = struct (* {{{ *) let e = (RemoteException (strbrk s), info) in t_assign (`Exn e); Hooks.(call execution_error start Loc.ghost (strbrk s)); - feedback (Feedback.InProgress ~-1) + feedback (InProgress ~-1) let build_proof_here ~drop_pt (id,valid) loc eop = Future.create (State.exn_on id ~valid) (fun () -> @@ -1096,7 +1093,7 @@ end = struct (* {{{ *) Aux_file.record_in_aux_at loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); let p = Proof_global.return_proof ~allow_partial:drop_pt () in - if drop_pt then Pp.feedback ~state_id:id Feedback.Complete; + if drop_pt then feedback ~id:(State id) Complete; p) let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states = @@ -1141,9 +1138,10 @@ end = struct (* {{{ *) let perform_states query = if query = [] then [] else - let is_tac = function - | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true - | _ -> false in + let is_tac e = match classify_vernac e with + | VtProofStep _, _ -> true + | _ -> false + in let initial = let rec aux id = try match VCS.visit id with { next } -> aux next @@ -1188,7 +1186,7 @@ end = struct (* {{{ *) "The system state could not be sent to the worker process. "^ "Falling back to local, lazy, evaluation.")); t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop)); - feedback (Feedback.InProgress ~-1) + feedback (InProgress ~-1) end (* }}} *) @@ -1268,7 +1266,7 @@ end = struct (* {{{ *) let (e, info) = Errors.push e in (try match Stateid.get info with | None -> - pperrnl ( + msg_error ( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) | Some (_, cur) -> @@ -1278,12 +1276,12 @@ end = struct (* {{{ *) | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (`Ast ( { loc }, _)) } -> let start, stop = Loc.unloc loc in - pperrnl ( + msg_error ( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ str ": chars " ++ int start ++ str "-" ++ int stop ++ spc () ++ iprint (e, info)) | _ -> - pperrnl ( + msg_error ( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) with e -> @@ -1343,7 +1341,6 @@ end = struct (* {{{ *) let set_perspective idl = ProofTask.set_perspective idl; TaskQueue.broadcast (Option.get !queue); - let open Stateid in let open ProofTask in let overlap s1 s2 = List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in @@ -1377,7 +1374,7 @@ end = struct (* {{{ *) else let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in - feedback (Feedback.InProgress 1); + feedback (InProgress 1); let task = ProofTask.(BuildProof { t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt; t_loc = loc; t_uuid; t_name = pname; @@ -1414,7 +1411,7 @@ and TacTask : sig t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : ast; + t_ast : int * ast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } @@ -1431,7 +1428,7 @@ end = struct (* {{{ *) t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : ast; + t_ast : int * ast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } @@ -1440,7 +1437,7 @@ end = struct (* {{{ *) r_state : Stateid.t; r_state_fb : Stateid.t; r_document : VCS.vcs option; - r_ast : ast; + r_ast : int * ast; r_goal : Goal.goal; r_name : string } @@ -1484,6 +1481,9 @@ end = struct (* {{{ *) | Some { t_kill } -> t_kill () | _ -> () + let command_focus = Proof.new_focus_kind () + let focus_cond = Proof.no_cond command_focus + let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = Option.iter VCS.restore vcs; try @@ -1493,15 +1493,15 @@ end = struct (* {{{ *) let g = Evd.find sigma0 r_goal in if not ( Evarutil.is_ground_term sigma0 Evd.(evar_concl g) && - List.for_all (fun (_,bo,ty) -> - Evarutil.is_ground_term sigma0 ty && - Option.cata (Evarutil.is_ground_term sigma0) true bo) - Evd.(evar_context g)) + List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) + Evd.(evar_context g)) then Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin - vernac_interp r_state_fb r_ast; + let (i, ast) = r_ast in + Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); + vernac_interp r_state_fb ast; let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress") @@ -1530,12 +1530,11 @@ end = struct (* {{{ *) module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } = - let e, etac, time, fail = + let e, 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 + | _ -> e, time, fail in find false false e in Hooks.call Hooks.with_fail fail (fun () -> (if time then System.with_time false else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> @@ -1547,8 +1546,7 @@ end = struct (* {{{ *) Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i) (State.exn_on id ~valid:safe_id) in - let t_ast = - { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in + let t_ast = (i, { verbose; loc; expr = e }) in let t_name = Goal.uid g in TaskQueue.enqueue_task queue ({ t_state = safe_id; t_state_fb = id; @@ -1623,11 +1621,11 @@ end = struct (* {{{ *) Reach.known_state ~cache:`No r_where; try vernac_interp r_for { r_what with verbose = true }; - feedback ~state_id:r_for Feedback.Processed + feedback ~id:(State r_for) Processed with e when Errors.noncritical e -> let e = Errors.push e in let msg = string_of_ppcmds (iprint e) in - feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg)) + feedback ~id:(State r_for) (ErrorMsg (Loc.ghost, msg)) let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what) let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what) @@ -1648,7 +1646,7 @@ end = struct (* {{{ *) let vernac_interp switch prev id q = assert(TaskQueue.n_workers (Option.get !queue) > 0); TaskQueue.enqueue_task (Option.get !queue) - QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch) + QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch) let init () = queue := Some (TaskQueue.create (if !Flags.async_proofs_full then 1 else 0)) @@ -1895,7 +1893,7 @@ let known_state ?(redefine_qed=false) ~cache id = if not delegate then ignore(Future.compute fp); reach view.next; vernac_interp id ~proof x; - feedback ~state_id:id Feedback.Incomplete + feedback ~id:(State id) Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () @@ -2032,7 +2030,6 @@ let check_task name (tasks,rcbackup) i = let vcs = VCS.backup () in try let rc = Future.purify (Slaves.check_task name tasks) i in - pperr_flush (); VCS.restore vcs; rc with e when Errors.noncritical e -> VCS.restore vcs; false @@ -2042,7 +2039,6 @@ let finish_tasks name u d p (t,rcbackup as tasks) = let finish_task u (_,_,i) = let vcs = VCS.backup () in let u = Future.purify (Slaves.finish_task name u d p t) i in - pperr_flush (); VCS.restore vcs; u in try @@ -2050,7 +2046,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = (u,a,true), p with e -> let e = Errors.push e in - pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); + msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 let merge_proof_branch ?valid ?id qast keep brname = @@ -2126,7 +2122,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let head = VCS.current_branch () in VCS.checkout head; let rc = begin - prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); + prerr_endline (fun () -> + " classified as: " ^ string_of_vernac_classification c); match c with (* PG stuff *) | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok @@ -2192,7 +2189,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = may_pierce_opaque x then `SkipQueue else `MainQueue in - VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue }); + VCS.commit id (Cmd { + ctac=false;ceff=false;cast = x; cids = []; cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQuery (false,_), VtLater -> anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") @@ -2215,7 +2213,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = anomaly(str"VtProofMode must be executed VtNow") | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in - VCS.commit id (Cmd {ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue}); + VCS.commit id (Cmd { + ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue}); List.iter (fun bn -> match VCS.get_branch bn with | { VCS.root; kind = `Master; pos } -> () @@ -2233,7 +2232,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtProofStep paral, w -> let id = VCS.new_node ~id:newtip () in let queue = if paral then `TacQueue (ref false) else `MainQueue in - VCS.commit id (Cmd {ctac = true;ceff = false;cast = x;cids = [];cqueue = queue }); + VCS.commit id (Cmd { + ctac = true;ceff = false;cast = x;cids = [];cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> let valid = if tty then Some(VCS.get_branch_pos head) else None in @@ -2247,20 +2247,23 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = vernac_interp (VCS.get_branch_pos head) x; `Ok | VtSideff l, w -> - let ceff_in_proof = not (VCS.Branch.equal head VCS.Branch.master) in + let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; + VCS.commit id (Cmd { + ctac=false;ceff=in_proof;cast=x;cids=l;cqueue=`MainQueue }); + (* We can't replay a Definition since universes may be differently + * inferred. This holds in Coq >= 8.5 *) let replay = match x.expr with | VernacDefinition(_, _, DefineBody _) -> None - | _ -> Some x - in - VCS.commit id (Cmd {ctac=false;ceff=ceff_in_proof;cast=x;cids=l;cqueue=`MainQueue}); - VCS.propagate_sideff replay; + | _ -> Some x in + VCS.propagate_sideff ~replay; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); `Ok (* Unknown: we execute it, check for open goals and propagate sideeff *) | VtUnknown, VtNow -> + let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *) @@ -2270,21 +2273,23 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = Reach.known_state ~cache:(interactive ()) mid; vernac_interp id x; (* Vernac x may or may not start a proof *) - if VCS.Branch.equal head VCS.Branch.master && - Proof_global.there_are_pending_proofs () - then begin + if not in_proof && Proof_global.there_are_pending_proofs () then + begin let bname = VCS.mk_branch_name x in let opacity_of_produced_term = match x.expr with + (* This AST is ambiguous, hence we check it dynamically *) | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity | _ -> Doesn'tGuaranteeOpacity in VCS.commit id (Fork (x,bname,opacity_of_produced_term,[])); - VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); - Proof_global.activate_proof_mode "Classic"; + let proof_mode = default_proof_mode () in + VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); + Proof_global.activate_proof_mode proof_mode; end else begin - VCS.commit id (Cmd {ctac = false; ceff = true; - cast = x; cids = []; cqueue = `MainQueue}); - VCS.propagate_sideff (Some x); + VCS.commit id (Cmd { + ctac=false;ceff=in_proof;cast=x;cids=[];cqueue=`MainQueue }); + (* We hope it can be replayed, but we can't really know *) + VCS.propagate_sideff ~replay:(Some x); VCS.checkout_shallowest_proof_branch (); end in State.define ~safe_id:head_id ~cache:`Yes step id; @@ -2346,7 +2351,7 @@ type focus = { tip : Stateid.t } -let query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s = +let query ~at ?(report_with=(Stateid.dummy,default_route)) s = Future.purify (fun s -> if Stateid.equal at Stateid.dummy then finish () else Reach.known_state ~cache:`Yes at; diff --git a/stm/stm.mli b/stm/stm.mli index ad89eb71f3..6519a62541 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -9,6 +9,7 @@ open Vernacexpr open Names open Feedback +open Loc (** state-transaction-machine interface *) @@ -19,7 +20,7 @@ open Feedback The sentence [s] is parsed in the state [ontop]. If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) -val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> unit) -> +val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) -> bool -> edit_id -> string -> Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] @@ -124,9 +125,9 @@ val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ] (** read-eval-print loop compatible interface ****************************** **) (* Adds a new line to the document. It replaces the core of Vernac.interp. - [finish] is called as the last bit of this function is the system + [finish] is called as the last bit of this function if the system is running interactively (-emacs or coqtop). *) -val interp : bool -> located_vernac_expr -> unit +val interp : bool -> vernac_expr located -> unit (* Queries for backward compatibility *) val current_proof_depth : unit -> int @@ -134,7 +135,7 @@ val get_all_proof_names : unit -> Id.t list val get_current_proof_name : unit -> Id.t option val show_script : ?proof:Proof_global.closed_proof -> unit -> unit -(** Reverse dependency hooks *) +(* Hooks to be set by other Coq components in order to break file cycles *) val process_error_hook : Future.fix_exn Hook.t val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 85cb45708a..d1d6de9ae8 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -20,9 +20,6 @@ let unlock loc = let start, stop = Loc.unloc loc in (string_of_int start, string_of_int stop) -let xmlNoop = (* almost noop *) - PCData "" - let xmlWithLoc loc ename attr xml = let start, stop = unlock loc in Element(ename, [ "begin", start; "end", stop ] @ attr, xml) @@ -307,7 +304,13 @@ and pp_cases_pattern_expr cpe = xmlApply loc (xmlOperator "alias" ~attr:["name", string_of_id id] loc :: [pp_cases_pattern_expr cpe]) - | CPatCstr (loc, ref, cpel1, cpel2) -> + | CPatCstr (loc, ref, None, cpel2) -> + xmlApply loc + (xmlOperator "reference" + ~attr:["name", Libnames.string_of_reference ref] loc :: + [Element ("impargs", [], []); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatCstr (loc, ref, Some cpel1, cpel2) -> xmlApply loc (xmlOperator "reference" ~attr:["name", Libnames.string_of_reference ref] loc :: @@ -347,7 +350,7 @@ and pp_cases_pattern_expr cpe = xmlApply loc (xmlOperator "delimiter" ~attr:["name", delim] loc :: [pp_cases_pattern_expr cpe]) -and pp_case_expr (e, (name, pat)) = +and pp_case_expr (e, name, pat) = match name, pat with | None, None -> xmlScrutinee [pp_expr e] | Some (loc, name), None -> @@ -460,7 +463,7 @@ and pp_expr ?(attr=[]) e = (return @ [Element ("scrutinees", [], List.map pp_case_expr cel)] @ [pp_branch_expr_list bel])) - | CRecord (_, _, _) -> assert false + | CRecord (_, _) -> assert false | CLetIn (loc, (varloc, var), value, body) -> xmlApply loc (xmlOperator "let" loc :: @@ -487,12 +490,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]) @@ -500,9 +503,6 @@ let rec tmpp v loc = | VernacError _ -> xmlWithLoc loc "error" [] [] (* Syntax *) - | VernacTacticNotation _ as x -> - xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] - | VernacSyntaxExtension (_, ((_, name), sml)) -> let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in xmlReservedNotation attrs name loc @@ -513,13 +513,6 @@ let rec tmpp v loc = xmlScope loc "delimit" name ~attr:["delimiter",tag] [] | VernacDelimiters (name,None) -> xmlScope loc "undelimit" name ~attr:[] [] - | VernacBindScope (name,l) -> - xmlScope loc "bind" name - (List.map (function - | ByNotation(loc,name,None) -> xmlNotation [] name loc [] - | ByNotation(loc,name,Some d) -> - xmlNotation ["delimiter",d] name loc [] - | AN ref -> xmlReference ref) l) | VernacInfix (_,((_,name),sml),ce,sn) -> let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in let sc_attr = @@ -535,6 +528,7 @@ let rec tmpp v loc = | Some scope -> ["scope", scope] | None -> [] in xmlNotation (sc_attr @ attrs) name loc [pp_expr ce] + | VernacBindScope _ as x -> xmlTODO loc x | VernacNotationAddFormat _ as x -> xmlTODO loc x | VernacUniverse _ | VernacConstraint _ @@ -668,7 +662,7 @@ let rec tmpp v loc = (* Solving *) - | (VernacSolve _ | VernacSolveExistential _) as x -> + | (VernacSolveExistential _) as x -> xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] (* Auxiliary file and library management *) @@ -694,7 +688,6 @@ let rec tmpp v loc = | VernacBackTo _ -> PCData "VernacBackTo" (* Commands *) - | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x | VernacCreateHintDb _ as x -> xmlTODO loc x | VernacRemoveHints _ as x -> xmlTODO loc x | VernacHints _ as x -> xmlTODO loc x @@ -724,7 +717,6 @@ let rec tmpp v loc = | VernacRegister _ as x -> xmlTODO loc x | VernacComments (cl) -> xmlComment loc (List.flatten (List.map pp_comment cl)) - | VernacNop as x -> xmlTODO loc x (* Stm backdoor *) | VernacStm _ as x -> xmlTODO loc x diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index edb54ece40..b1df3c9ca6 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -10,6 +10,8 @@ open Vernacexpr open Errors open Pp +let default_proof_mode () = Proof_global.get_default_proof_mode_name () + let string_of_in_script b = if b then " (inside script)" else "" let string_of_vernac_type = function @@ -60,7 +62,7 @@ let undo_classifier = ref (fun _ -> assert false) let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = - let rec static_classifier e = match e with + let static_classifier e = match e with (* PG compatibility *) | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) @@ -86,7 +88,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 _ @@ -102,12 +104,10 @@ let rec classify_vernac e = | VernacCheckMayEval _ -> VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater (* ProofStep *) - | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater | VernacProof _ | VernacBullet _ | VernacFocus _ | VernacUnfocus | VernacSubproof _ | VernacEndSubproof - | VernacSolve _ | VernacCheckGuard | VernacUnfocused | VernacSolveExistential _ -> VtProofStep false, VtLater @@ -117,27 +117,27 @@ let rec classify_vernac e = (* StartProof *) | VernacDefinition ( (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) -> - VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater + VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> - VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater + VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater | VernacStartTheoremProof (_,l,_) -> let ids = CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in - VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater - | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater + VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater + | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater | VernacFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> @@ -175,11 +175,6 @@ let rec classify_vernac e = | VernacRegister _ | VernacNameSectionHypSet _ | VernacComments _ -> VtSideff [], VtLater - | VernacDeclareTacticDefinition (_,l) -> - let open Libnames in - VtSideff (List.map (function - | (Ident (_,r),_,_) -> r - | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) @@ -195,7 +190,6 @@ let rec classify_vernac e = | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ - | VernacTacticNotation _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) @@ -208,7 +202,6 @@ let rec classify_vernac e = | VernacResetName _ | VernacResetInitial | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e (* What are these? *) - | VernacNop | VernacToplevelControl _ | VernacRestoreState _ | VernacWriteState _ -> VtUnknown, VtNow @@ -217,13 +210,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 |