diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 862 |
1 files changed, 572 insertions, 290 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3be3c6db..75efe139 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* Concrete syntax of the mathematical vernacular MV V2.6 *) open Pp @@ -19,12 +17,9 @@ open Nameops open Term open Pfedit open Tacmach -open Proof_trees -open Decl_mode open Constrintern open Prettyp open Printer -open Tactic_printer open Tacinterp open Command open Goptions @@ -37,6 +32,7 @@ open Pretyping open Redexpr open Syntax_def open Lemmas +open Declaremods (* Pcoq hooks *) @@ -49,7 +45,7 @@ type pcoq_hook = { print_check : Environ.env -> Environ.unsafe_judgment -> unit; print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> Environ.unsafe_judgment -> unit; - show_goal : int option -> unit + show_goal : goal_reference -> unit } let pcoq = ref None @@ -66,60 +62,102 @@ let cl_of_qualid = function (* "Show" commands *) let show_proof () = - let pts = get_pftreestate () in - let cursor = cursor_of_pftreestate pts in - let evc = evc_of_pftreestate pts in - let (pfterm,meta_types) = extract_open_pftreestate pts in - msgnl (str"LOC: " ++ - prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ - str"Subgoals" ++ fnl () ++ - prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++ - pr_ltype ty ++ fnl ()) - meta_types - ++ str"Proof: " ++ pr_lconstr (Evarutil.nf_evar evc pfterm)) + (* spiwack: this would probably be cooler with a bit of polishing. *) + let p = Proof_global.give_me_the_proof () in + let pprf = Proof.partial_proof p in + msgnl (Util.prlist_with_sep Pp.fnl Printer.pr_constr pprf) let show_node () = - let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and cursor = cursor_of_pftreestate pts in - msgnl (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ - pr_goal (goal_of_proof pf) ++ fnl () ++ - (match pf.Proof_type.ref with - | None -> (str"BY <rule>") - | Some(r,spfl) -> - (str"BY " ++ pr_rule r ++ fnl () ++ - str" " ++ - hov 0 (prlist_with_sep pr_fnl pr_goal - (List.map goal_of_proof spfl))))) + (* spiwack: I'm have little clue what this function used to do. I deactivated it, + could, possibly, be cleaned away. (Feb. 2010) *) + () + +(* indentation code for Show Script, initially contributed + by D. de Rauglaudre *) + +let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = + (* ng1 : number of goals remaining at the current level (before cmd) + ngl1 : stack of previous levels with their remaining goals + ng : number of goals after the execution of cmd + beginend : special indentation stack for { } *) + let ngprev = List.fold_left (+) ng1 ngl1 in + let new_ngl = + if ng > ngprev then + (* We've branched *) + (ng - ngprev + 1, ng1 - 1 :: ngl1) + else if ng < ngprev then + (* A subgoal have been solved. Let's compute the new current level + by discarding all levels with 0 remaining goals. *) + let _ = assert (ng = ngprev - 1) in + let rec loop = function + | (0, ng2::ngl2) -> loop (ng2,ngl2) + | p -> p + in loop (ng1-1, ngl1) + else + (* Standard case, same goal number as before *) + (ng1, ngl1) + in + (* When a subgoal have been solved, separate this block by an empty line *) + let new_nl = (ng < ngprev) + in + (* Indentation depth *) + let ind = List.length ngl1 + in + (* Some special handling of bullets and { }, to get a nicer display *) + let pred n = max 0 (n-1) in + let ind, nl, new_beginend = match cmd with + | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend + | VernacEndSubproof -> List.hd beginend, false, List.tl beginend + | VernacBullet _ -> pred ind, nl, beginend + | _ -> ind, nl, beginend + in + let pp = + (if nl then fnl () else mt ()) ++ + (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) + in + (new_ngl, new_nl, new_beginend, pp :: ppl) let show_script () = - let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and evc = evc_of_pftreestate pts in - msgnl_with !Pp_control.deep_ft (print_treescript evc pf) + let prf = Pfedit.get_current_proof_name () in + let cmds = Backtrack.get_script prf in + let _,_,_,indented_cmds = + List.fold_left indent_script_item ((1,[]),false,[],[]) cmds + in + let indented_cmds = List.rev (indented_cmds) in + msgnl (v 0 (Util.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) let show_thesis () = msgnl (anomaly "TODO" ) let show_top_evars () = + (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = get_pftreestate () in - let gls = top_goal_of_pftreestate pfts in - let sigma = project gls in + let gls = Proof.V82.subgoals pfts in + let sigma = gls.Evd.sigma in msg (pr_evars_int 1 (Evarutil.non_instantiated sigma)) + let show_prooftree () = - let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and evc = evc_of_pftreestate pts in - msg (print_proof evc (Global.named_context()) pf) + (* Spiwack: proof tree is currently not working *) + () + +let enable_goal_printing = ref true + +let print_subgoals () = + if !enable_goal_printing && is_verbose () + then msg (pr_open_subgoals ()) + +let try_print_subgoals () = + Pp.flush_all(); + try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> () -let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () (* Simulate the Intro(s) tactic *) let show_intro all = let pf = get_pftreestate() in - let gl = nth_goal_of_pftreestate 1 pf in + let {Evd.it=gls ; sigma=sigma} = Proof.V82.subgoals pf in + let gl = {Evd.it=List.hd gls ; sigma = sigma} in let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in if all then @@ -131,13 +169,12 @@ let show_intro all = msgnl (pr_id (List.hd (Tactics.find_intro_names [n] gl))) with Failure "list_last" -> message "" -let id_of_name = function - | Names.Anonymous -> id_of_string "x" - | Names.Name x -> x - +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) -(* Building of match expression *) -(* From ide/coq.ml *) let make_cases s = let qualified_name = Libnames.qualid_of_string s in let glob_ref = Nametab.locate qualified_name in @@ -147,36 +184,31 @@ let make_cases s = , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } = Global.lookup_inductive i in Util.array_fold_right2 - (fun n t l -> - let (al,_) = Term.decompose_prod t in - let al,_ = Util.list_chop (List.length al - np) al in + (fun consname typ l -> + let al = List.rev (fst (Term.decompose_prod typ)) in + let al = Util.list_skipn np al in let rec rename avoid = function | [] -> [] | (n,_)::l -> - let n' = Namegen.next_ident_away_in_goal (id_of_name n) avoid in + let n' = Namegen.next_name_away_in_cases_pattern n avoid in string_of_id n' :: rename (n'::avoid) l in - let al' = rename [] (List.rev al) in - (string_of_id n :: al') :: l) + let al' = rename [] al in + (string_of_id consname :: al') :: l) carr tarr [] | _ -> raise Not_found +(** Textual display of a generic "match" template *) let show_match id = - try - let s = string_of_id (snd id) in - let patterns = List.rev (make_cases s) in - let cases = - List.fold_left - (fun acc x -> - match x with - | [] -> assert false - | [x] -> "| "^ x ^ " => \n" ^ acc - | x::l -> - "| " ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l - ^ " => \n" ^ acc) - "end" patterns in - msg (str ("match # with\n" ^ cases)) - with Not_found -> error "Unknown inductive type." + let patterns = + try make_cases (string_of_id (snd id)) + with Not_found -> error "Unknown inductive type." + in + let pr_branch l = + str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" + in + msg (v 1 (str "match # with" ++ fnl () ++ + prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ())) (* "Print" commands *) @@ -220,18 +252,55 @@ let print_modtype r = let (loc,qid) = qualid_of_reference r in try let kn = Nametab.locate_modtype qid in - msgnl (Printmod.print_modtype kn) - with - Not_found -> msgnl (str"Unknown Module Type " ++ pr_qualid qid) + msgnl (Printmod.print_modtype kn) + with Not_found -> + (* Is there a module of this name ? If yes we display its type *) + try + let mp = Nametab.locate_module qid in + msgnl (Printmod.print_module false mp) + with Not_found -> + msgnl (str"Unknown Module Type or Module " ++ pr_qualid qid) -let dump_universes s = +let dump_universes_gen g s = let output = open_out s in + let output_constraint, close = + if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin + (* the lazy unit is to handle errors while printing the first line *) + let init = lazy (Printf.fprintf output "digraph universes {\n") in + begin fun kind left right -> + let () = Lazy.force init in + match kind with + | Univ.Lt -> + Printf.fprintf output " \"%s\" -> \"%s\" [style=bold];\n" right left + | Univ.Le -> + Printf.fprintf output " \"%s\" -> \"%s\" [style=solid];\n" right left + | Univ.Eq -> + Printf.fprintf output " \"%s\" -> \"%s\" [style=dashed];\n" left right + end, begin fun () -> + if Lazy.lazy_is_val init then Printf.fprintf output "}\n"; + close_out output + end + end else begin + begin fun kind left right -> + let kind = match kind with + | Univ.Lt -> "<" + | Univ.Le -> "<=" + | Univ.Eq -> "=" + in Printf.fprintf output "%s %s %s ;\n" left kind right + end, (fun () -> close_out output) + end + in try - Univ.dump_universes output (Global.universes ()); - close_out output; + Univ.dump_universes output_constraint g; + close (); msgnl (str ("Universes written to file \""^s^"\".")) with - e -> close_out output; raise e + reraise -> close (); raise reraise + +let dump_universes sorted s = + let g = Global.universes () in + let g = if sorted then Univ.sort_universes g else g in + dump_universes_gen g s (*********************) (* "Locate" commands *) @@ -262,7 +331,7 @@ let msg_notfound_library loc qid = function let print_located_library r = let (loc,qid) = qualid_of_reference r in try msg_found_library (Library.locate_qualified_library false qid) - with e -> msg_notfound_library loc qid e + with e when Errors.noncritical e -> msg_notfound_library loc qid e let print_located_module r = let (loc,qid) = qualid_of_reference r in @@ -291,6 +360,11 @@ let smart_global r = Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr; gr +let dump_global r = + try + let gr = Smartlocate.smart_global r in + Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr + with e when Errors.noncritical e -> () (**********) (* Syntax *) @@ -314,11 +388,12 @@ let vernac_notation = Metasyntax.add_notation (* Gallina *) let start_proof_and_print k l hook = + check_locality (); (* early check, cf #2975 *) start_proof_com k l hook; print_subgoals (); if !pcoq <> None then (Option.get !pcoq).start_proof () -let vernac_definition (local,boxed,k) (loc,id as lid) def hook = +let vernac_definition (local,k) (loc,id as lid) def hook = if local = Local then Dumpglob.dump_definition lid true "var" else Dumpglob.dump_definition lid false "def"; (match def with @@ -331,8 +406,8 @@ let vernac_definition (local,boxed,k) (loc,id as lid) def hook = | None -> None | Some r -> let (evc,env)= get_current_context () in - Some (interp_redexp env evc r) in - let ce,imps = interp_definition boxed bl red_option c typ_opt in + Some (snd (interp_redexp env evc r)) in + let ce,imps = interp_definition bl red_option c typ_opt in declare_definition id (local,k) ce imps hook) let vernac_start_proof kind l lettop hook = @@ -347,27 +422,32 @@ let vernac_start_proof kind l lettop hook = (str "Let declarations can only be used in proof editing mode."); start_proof_and_print (Global, Proof kind) l hook +let qed_display_script = ref true + let vernac_end_proof = function - | Admitted -> admit () + | Admitted -> + Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()]; + admit () | Proved (is_opaque,idopt) -> - if not !Flags.print_emacs then if_verbose show_script (); - match idopt with + let prf = Pfedit.get_current_proof_name () in + if is_verbose () && !qed_display_script then (show_script (); msg (fnl())); + begin match idopt with | None -> save_named is_opaque | Some ((_,id),None) -> save_anonymous is_opaque id | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id + end; + Backtrack.mark_unreachable [prf] (* A stupid macro that should be replaced by ``Exact c. Save.'' all along the theories [??] *) let vernac_exact_proof c = - let pfs = top_of_tree (get_pftreestate()) in - let pf = proof_of_pftreestate pfs in - if (is_leaf_proof pf) then begin - by (Tactics.exact_proof c); - save_named true end - else - errorlabstrm "Vernacentries.ExactProof" - (strbrk "Command 'Proof ...' can only be used at the beginning of the proof.") + (* spiwack: for simplicity I do not enforce that "Proof proof_term" is + called only at the begining of a proof. *) + let prf = Pfedit.get_current_proof_name () in + by (Tactics.exact_proof c); + save_named true; + Backtrack.mark_unreachable [prf] let vernac_assumption kind l nl= let global = fst kind = Global in @@ -386,7 +466,7 @@ let vernac_record k finite infer struc binders sort nameopt cfs = Dumpglob.dump_definition lid false "constr"; id in if Dumpglob.dump () then ( Dumpglob.dump_definition (snd struc) false "rec"; - List.iter (fun ((_, x), _) -> + List.iter (fun (((_, x), _), _) -> match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); @@ -409,7 +489,8 @@ let vernac_inductive finite infer indl = | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in - ((coe, AssumExpr ((loc, Name id), ce)), []) + let coe' = if coe then Some true else None in + (((coe', AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) finite infer id bl c None [f] | [ ( id , bl , c , Class true, _), _ ] -> Util.error "Definitional classes must have a single method" @@ -424,19 +505,31 @@ let vernac_inductive finite infer indl = let indl = List.map unpack indl in do_mutual_inductive indl (recursivity_flag_of_kind finite) -let vernac_fixpoint l b = +let vernac_fixpoint l = if Dumpglob.dump () then List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_fixpoint l b + do_fixpoint l -let vernac_cofixpoint l b = +let vernac_cofixpoint l = if Dumpglob.dump () then List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_cofixpoint l b - -let vernac_scheme = Indschemes.do_scheme + do_cofixpoint l -let vernac_combined_scheme = Indschemes.do_combined_scheme +let vernac_scheme l = + if Dumpglob.dump () then + List.iter (fun (lid, s) -> + Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid; + match s with + | InductionScheme (_, r, _) + | CaseScheme (_, r, _) + | EqualityScheme r -> dump_global r) l; + Indschemes.do_scheme l + +let vernac_combined_scheme lid l = + if Dumpglob.dump () then + (Dumpglob.dump_definition lid false "def"; + List.iter (fun lid -> dump_global (Genarg.AN (Ident lid))) l); + Indschemes.do_combined_scheme lid l (**********************) (* Modules *) @@ -585,10 +678,10 @@ let vernac_end_section (loc,_) = let vernac_end_segment (_,id as lid) = check_no_pending_proofs (); match Lib.find_opening_node id with - | Lib.OpenedModule (export,_,_) -> vernac_end_module export lid - | Lib.OpenedModtype _ -> vernac_end_modtype lid + | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid + | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid | Lib.OpenedSection _ -> vernac_end_section lid - | _ -> anomaly "No more opened things" + | _ -> assert false (* Libraries *) @@ -608,13 +701,13 @@ let vernac_coercion stre ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in - Class.try_add_new_coercion_with_target ref' stre source target; + Class.try_add_new_coercion_with_target ref' stre ~source ~target; if_verbose msgnl (pr_global ref' ++ str " is now a coercion") let vernac_identity_coercion stre id qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - Class.try_add_new_identity_coercion id stre source target + Class.try_add_new_identity_coercion id stre ~source ~target (* Type classes *) @@ -625,32 +718,32 @@ let vernac_instance abst glob sup inst props pri = let vernac_context l = Classes.context l -let vernac_declare_instance glob id = - Classes.declare_instance glob id +let vernac_declare_instances glob ids = + List.iter (fun (id) -> Classes.existing_instance glob id) ids let vernac_declare_class id = Classes.declare_class id (***********) (* Solving *) + +let command_focus = Proof.new_focus_kind () +let focus_command_cond = Proof.no_cond command_focus + + let vernac_solve n tcom b = if not (refining ()) then error "Unknown command of the non proof-editing mode."; - Decl_mode.check_not_proof_mode "Unknown proof instruction"; - begin - if b then - solve_nth n (Tacinterp.hide_interp tcom (get_end_tac ())) - else solve_nth n (Tacinterp.hide_interp tcom None) - end; - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - if subtree_solved () then begin - Flags.if_verbose msgnl (str "Subgoal proved"); - make_focus 0; - reset_top_of_script () - end; - print_subgoals(); - if !pcoq <> None then (Option.get !pcoq).solve n + let p = Proof_global.give_me_the_proof () in + Proof.transaction p begin fun () -> + solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b; + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + Proof_global.maximal_unfocus command_focus p; + print_subgoals(); + if !pcoq <> None then (Option.get !pcoq).solve n + end + (* A command which should be a tactic. It has been added by Christine to patch an error in the design of the proof @@ -666,32 +759,15 @@ let vernac_set_end_tac tac = if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else () (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) -(***********************) -(* Proof Language Mode *) - -let vernac_decl_proof () = - check_not_proof_mode "Already in Proof Mode"; - if tree_solved () then - error "Nothing left to prove here." - else - begin - Decl_proof_instr.go_to_proof_mode (); - print_subgoals () - end - -let vernac_return () = - match get_current_mode () with - Mode_tactic -> - Decl_proof_instr.return_from_tactic_mode (); - print_subgoals () - | Mode_proof -> - error "\"return\" is only used after \"escape\"." - | Mode_none -> - error "There is no proof to end." - -let vernac_proof_instr instr = - Decl_proof_instr.proof_instr instr; - print_subgoals () +let vernac_set_used_variables l = + let l = List.map snd l in + if not (list_distinct l) then error "Used variables list contains duplicates"; + let vars = Environ.named_context (Global.env ()) in + List.iter (fun id -> + if not (List.exists (fun (id',_,_) -> id = id') vars) then + error ("Unknown variable: " ^ string_of_id id)) + l; + set_used_variables l (*****************************) (* Auxiliary file management *) @@ -706,7 +782,7 @@ let vernac_add_loadpath isrec pdir ldiropt = let alias = match ldiropt with | None -> Nameops.default_root_prefix | Some ldir -> ldir in - (if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias + (if isrec then Mltop.add_rec_path else Mltop.add_path) ~unix_path:pdir ~coq_root:alias let vernac_remove_loadpath path = Library.remove_load_path (System.expand_path_macros path) @@ -733,28 +809,14 @@ let vernac_chdir = function (********************) (* State management *) -let abort_refine f x = - if Pfedit.refining() then delete_all_proofs (); - f x - (* used to be: error "Must save or abort current goal first" *) - -let vernac_write_state file = abort_refine States.extern_state file - -let vernac_restore_state file = abort_refine States.intern_state file - - -(*************) -(* Resetting *) - -let vernac_reset_name id = abort_refine Lib.reset_name id +let vernac_write_state file = + Pfedit.delete_all_proofs (); + States.extern_state file -let vernac_reset_initial () = abort_refine Lib.reset_initial () +let vernac_restore_state file = + Pfedit.delete_all_proofs (); + States.intern_state file -let vernac_back n = Lib.back n - -let vernac_backto n = Lib.reset_label n - -(* see also [vernac_backtrack] which combines undoing and resetting *) (************) (* Commands *) @@ -764,6 +826,9 @@ let vernac_declare_tactic_definition (local,x,def) = let vernac_create_hintdb local id b = Auto.create_hint_db local id full_transparent_state b +let vernac_remove_hints local dbs ids = + Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids) + let vernac_hints local lb h = Auto.add_hints local lb (Auto.interp_hints h) @@ -778,11 +843,105 @@ let vernac_declare_implicits local r = function Impargs.declare_manual_implicits local (smart_global r) ~enriching:false (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps) +let vernac_declare_arguments local r l nargs flags = + let extra_scope_flag = List.mem `ExtraScopes flags in + let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let names, rest = List.hd names, List.tl names in + let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in + if List.exists ((<>) names) rest then + error "All arguments lists must declare the same names."; + if not (Util.list_distinct (List.filter ((<>) Anonymous) names)) then + error "Arguments names must be distinct."; + let sr = smart_global r in + let inf_names = + Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in + let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in + let rec check li ld ls = match li, ld, ls with + | [], [], [] -> () + | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls + | [], _::_, (Some _)::ls when extra_scope_flag -> + error "Extra notation scopes can be set on anonymous arguments only" + | [], x::_, _ -> error ("Extra argument " ^ string_of_name x ^ ".") + | l, [], _ -> error ("The following arguments are not declared: " ^ + (String.concat ", " (List.map string_of_name l)) ^ ".") + | _::li, _::ld, _::ls -> check li ld ls + | _ -> assert false in + if l <> [[]] then + List.iter2 (fun l -> check inf_names l) (names :: rest) scopes; + (* we take extra scopes apart, and we check they are consistent *) + let l, scopes = + let scopes, rest = List.hd scopes, List.tl scopes in + if List.exists (List.exists ((<>) None)) rest then + error "Notation scopes can be given only once"; + if not extra_scope_flag then l, scopes else + let l, _ = List.split (List.map (list_chop (List.length inf_names)) l) in + l, scopes in + (* we interpret _ as the inferred names *) + let l = if l = [[]] then l else + let name_anons = function + | (Anonymous, a,b,c,d), Name id -> Name id, a,b,c,d + | x, _ -> x in + List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in + let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let some_renaming_specified = + try Arguments_renaming.arguments_names sr <> names_decl + with Not_found -> false in + let some_renaming_specified, implicits = + if l = [[]] then false, [[]] else + Util.list_fold_map (fun sr il -> + let sr', impl = Util.list_fold_map (fun b -> function + | (Anonymous, _,_, true, max), Name id -> assert false + | (Name x, _,_, true, _), Anonymous -> + error ("Argument "^string_of_id x^" cannot be declared implicit.") + | (Name iid, _,_, true, max), Name id -> + b || iid <> id, Some (ExplByName id, max, false) + | (Name iid, _,_, _, _), Name id -> b || iid <> id, None + | _ -> b, None) + sr (List.combine il inf_names) in + sr || sr', Util.list_map_filter (fun x -> x) impl) + some_renaming_specified l in + if some_renaming_specified then + if not (List.mem `Rename flags) then + error "To rename arguments the \"rename\" flag must be specified." + else Arguments_renaming.rename_arguments local sr names_decl; + (* All other infos are in the first item of l *) + let l = List.hd l in + let some_implicits_specified = implicits <> [[]] in + let scopes = List.map (function + | None -> None + | Some (o, k) -> + try Some(ignore(Notation.find_scope k); k) + with e when Errors.noncritical e -> + Some (Notation.find_delimiters_scope o k)) scopes + in + let some_scopes_specified = List.exists ((<>) None) scopes in + let rargs = + Util.list_map_filter (function (n, true) -> Some n | _ -> None) + (Util.list_map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in + if some_scopes_specified || List.mem `ClearScopes flags then + vernac_arguments_scope local r scopes; + if not some_implicits_specified && List.mem `DefaultImplicits flags then + vernac_declare_implicits local r [] + else if some_implicits_specified || List.mem `ClearImplicits flags then + vernac_declare_implicits local r implicits; + if nargs >= 0 && nargs < List.fold_left max 0 rargs then + error "The \"/\" option must be placed after the last \"!\"."; + let rec narrow = function + | #Tacred.simpl_flag as x :: tl -> x :: narrow tl + | [] -> [] | _ :: tl -> narrow tl in + let flags = narrow flags in + if rargs <> [] || nargs >= 0 || flags <> [] then + match sr with + | ConstRef _ as c -> + Tacred.set_simpl_behaviour local c (rargs, nargs, flags) + | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.") + let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let t = Constrintern.interp_type Evd.empty (Global.env()) c in - let t = Detyping.detype false [] [] t in - List.iter (fun id -> Reserve.declare_reserved_type id t) idl) + let t = Detyping.detype false [] [] t in + let t = aconstr_of_glob_constr [] [] t in + Reserve.declare_reserved_type idl t) in List.iter sb_decl bl let vernac_generalizable = Implicit_quantifiers.declare_generalizable @@ -795,6 +954,7 @@ let make_silent_if_not_pcoq b = let _ = declare_bool_option { optsync = false; + optdepr = false; optname = "silent"; optkey = ["Silent"]; optread = is_silent; @@ -803,6 +963,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "implicit arguments"; optkey = ["Implicit";"Arguments"]; optread = Impargs.is_implicit_args; @@ -811,6 +972,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "strict implicit arguments"; optkey = ["Strict";"Implicit"]; optread = Impargs.is_strict_implicit_args; @@ -819,6 +981,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "strong strict implicit arguments"; optkey = ["Strongly";"Strict";"Implicit"]; optread = Impargs.is_strongly_strict_implicit_args; @@ -827,22 +990,16 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "contextual implicit arguments"; optkey = ["Contextual";"Implicit"]; optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } -(* let _ = *) -(* declare_bool_option *) -(* { optsync = true; *) -(* optname = "forceable implicit arguments"; *) -(* optkey = ["Forceable";"Implicit")); *) -(* optread = Impargs.is_forceable_implicit_args; *) -(* optwrite = Impargs.make_forceable_implicit_args } *) - let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "implicit status of reversible patterns"; optkey = ["Reversible";"Pattern";"Implicit"]; optread = Impargs.is_reversible_pattern_implicit_args; @@ -851,6 +1008,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "maximal insertion of implicit"; optkey = ["Maximal";"Implicit";"Insertion"]; optread = Impargs.is_maximal_implicit_args; @@ -859,6 +1017,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "automatic introduction of variables"; optkey = ["Automatic";"Introduction"]; optread = Flags.is_auto_intros; @@ -867,6 +1026,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "coercion printing"; optkey = ["Printing";"Coercions"]; optread = (fun () -> !Constrextern.print_coercions); @@ -875,13 +1035,16 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "printing of existential variable instances"; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Constrextern.print_evar_arguments); optwrite = (:=) Constrextern.print_evar_arguments } + let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "implicit arguments printing"; optkey = ["Printing";"Implicit"]; optread = (fun () -> !Constrextern.print_implicits); @@ -890,6 +1053,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "implicit arguments defensive printing"; optkey = ["Printing";"Implicit";"Defensive"]; optread = (fun () -> !Constrextern.print_implicits_defensive); @@ -898,6 +1062,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "projection printing using dot notation"; optkey = ["Printing";"Projections"]; optread = (fun () -> !Constrextern.print_projections); @@ -906,6 +1071,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "notations printing"; optkey = ["Printing";"Notations"]; optread = (fun () -> not !Constrextern.print_no_symbol); @@ -914,6 +1080,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "raw printing"; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); @@ -922,38 +1089,57 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; + optname = "record printing"; + optkey = ["Printing";"Records"]; + optread = (fun () -> !Flags.record_print); + optwrite = (fun b -> Flags.record_print := b) } + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; optname = "use of virtual machine inside the kernel"; optkey = ["Virtual";"Machine"]; optread = (fun () -> Vconv.use_vm ()); optwrite = (fun b -> Vconv.set_use_vm b) } let _ = - declare_bool_option + declare_int_option { optsync = true; - optname = "use of boxed definitions"; - optkey = ["Boxed";"Definitions"]; - optread = Flags.boxed_definitions; - optwrite = (fun b -> Flags.set_boxed_definitions b) } + optdepr = false; + optname = "the level of inling duging functor application"; + optkey = ["Inline";"Level"]; + optread = (fun () -> Some (Flags.get_inline_level ())); + optwrite = (fun o -> + let lev = Option.default Flags.default_inline_level o in + Flags.set_inline_level lev) } let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "use of boxed values"; optkey = ["Boxed";"Values"]; optread = (fun _ -> not (Vm.transp_values ())); optwrite = (fun b -> Vm.set_transp_values (not b)) } +(* No more undo limit in the new proof engine. + The command still exists for compatibility (e.g. with ProofGeneral) *) + let _ = declare_int_option { optsync = false; - optname = "the undo limit"; + optdepr = true; + optname = "the undo limit (OBSOLETE)"; optkey = ["Undo"]; - optread = Pfedit.get_undo; - optwrite = Pfedit.set_undo } + optread = (fun _ -> None); + optwrite = (fun _ -> ()) } let _ = declare_int_option { optsync = false; + optdepr = false; optname = "the hypotheses limit"; optkey = ["Hyps";"Limit"]; optread = Flags.print_hyps_limit; @@ -962,6 +1148,7 @@ let _ = let _ = declare_int_option { optsync = true; + optdepr = false; optname = "the printing depth"; optkey = ["Printing";"Depth"]; optread = Pp_control.get_depth_boxes; @@ -970,6 +1157,7 @@ let _ = let _ = declare_int_option { optsync = true; + optdepr = false; optname = "the printing width"; optkey = ["Printing";"Width"]; optread = Pp_control.get_margin; @@ -978,6 +1166,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "printing of universes"; optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); @@ -989,11 +1178,21 @@ let vernac_debug b = let _ = declare_bool_option { optsync = false; + optdepr = false; optname = "Ltac debug"; optkey = ["Ltac";"Debug"]; optread = (fun () -> get_debug () <> Tactic_debug.DebugOff); optwrite = vernac_debug } +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "explicitly parsing implicit arguments"; + optkey = ["Parsing";"Explicit"]; + optread = (fun () -> !Constrintern.parsing_explicit); + optwrite = (fun b -> Constrintern.parsing_explicit := b) } + let vernac_set_opacity local str = let glob_ref r = match smart_global r with @@ -1006,7 +1205,7 @@ let vernac_set_opacity local str = let vernac_set_option locality key = function | StringValue s -> set_string_option_value_gen locality key s - | IntValue n -> set_int_option_value_gen locality key (Some n) + | IntValue n -> set_int_option_value_gen locality key n | BoolValue b -> set_bool_option_value_gen locality key b let vernac_unset_option locality key = @@ -1046,21 +1245,31 @@ let get_current_context_of_args = function | None -> get_current_context () let vernac_check_may_eval redexp glopt rc = - let (evmap,env) = get_current_context_of_args glopt in - let c = interp_constr evmap env rc in - let j = Typeops.typing env c in + let module P = Pretype_errors in + let (sigma, env) = get_current_context_of_args glopt in + let sigma', c = interp_open_constr sigma env rc in + let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in + let j = + try + Evarutil.check_evars env sigma sigma' c; + Arguments_renaming.rename_typing env c + with P.PretypeError (_,_,P.UnsolvableImplicit _) + | Compat.Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) -> + Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in match redexp with | None -> if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> - let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in + Tacinterp.dump_glob_red_expr r; + let (sigma',r_interp) = interp_redexp env sigma' r in + let redfun = fst (reduction_of_red_expr r_interp) in if !pcoq <> None - then (Option.get !pcoq).print_eval redfun env evmap rc j - else msg (print_eval redfun env evmap rc j) + then (Option.get !pcoq).print_eval redfun env sigma' rc j + else msg (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = - declare_red_expr locality s (interp_redexp (Global.env()) Evd.empty r) + declare_red_expr locality s (snd (interp_redexp (Global.env()) Evd.empty r)) (* The same but avoiding the current goal context if any *) let vernac_global_check c = @@ -1095,21 +1304,26 @@ let vernac_print = function | PrintCoercionPaths (cls,clt) -> ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ()) - | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ())) - | PrintUniverses (Some s) -> dump_universes s + | PrintUniverses (b, None) -> + let univ = Global.universes () in + let univ = if b then Univ.sort_universes univ else univ in + pp (Univ.pr_universes univ) + | PrintUniverses (b, Some s) -> dump_universes b s | PrintHint r -> Auto.print_hint_ref (smart_global r) | PrintHintGoal -> Auto.print_applicable_hint () | PrintHintDbName s -> Auto.print_hint_db_by_name s | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s | PrintHintDb -> Auto.print_searchtable () | PrintScopes -> - pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr)) + pp (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) | PrintScope s -> - pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s) + pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) | PrintVisibility s -> - pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) - | PrintAbout qid -> msg (print_about qid) - | PrintImplicit qid -> msg (print_impargs qid) + pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) + | PrintAbout qid -> + msg (print_about qid) + | PrintImplicit qid -> + dump_global qid; msg (print_impargs qid) | PrintAssumptions (o,r) -> (* Prints all the axioms and section variables used by a term *) let cstr = constr_of_global (smart_global r) in @@ -1145,7 +1359,7 @@ let interp_search_about_item = function (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> - error ("Unable to interp \""^s^"\" either as a reference or + error ("Unable to interp \""^s^"\" either as a reference or \ as an identifier component") let vernac_search s r = @@ -1169,31 +1383,93 @@ let vernac_locate = function | LocateTerm (Genarg.ByNotation (_,ntn,sc)) -> ppnl (Notation.locate_notation - (Constrextern.without_symbols pr_lrawconstr) ntn sc) + (Constrextern.without_symbols pr_lglob_constr) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> print_located_module qid | LocateTactic qid -> print_located_tactic qid | LocateFile f -> locate_file f +(****************) +(* Backtracking *) + +(** NB: these commands are now forbidden in non-interactive use, + e.g. inside VernacLoad, VernacList, ... *) + +let vernac_backto lbl = + try + let lbl' = Backtrack.backto lbl in + if lbl <> lbl' then + Pp.msg_warning + (str "Actually back to state "++ Pp.int lbl' ++ str "."); + try_print_subgoals () + with Backtrack.Invalid -> error "Invalid backtrack." + +let vernac_back n = + try + let extra = Backtrack.back n in + if extra <> 0 then + Pp.msg_warning + (str "Actually back by " ++ Pp.int (extra+n) ++ str " steps."); + try_print_subgoals () + with Backtrack.Invalid -> error "Invalid backtrack." + +let vernac_reset_name id = + try + let globalized = + try + let gr = Smartlocate.global_with_alias (Ident id) in + Dumpglob.add_glob (fst id) gr; + true + with e when Errors.noncritical e -> false in + + if not globalized then begin + try begin match Lib.find_opening_node (snd id) with + | Lib.OpenedSection _ -> Dumpglob.dump_reference (fst id) + (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; + (* Might be nice to implement module cases, too.... *) + | _ -> () + end with UserError _ -> () + end; + + if Backtrack.is_active () then + (Backtrack.reset_name id; try_print_subgoals ()) + else + (* When compiling files, Reset is now allowed again + as asked by A. Chlipala. we emulate a simple reset, + that discards all proofs. *) + let lbl = Lib.label_before_name id in + Pfedit.delete_all_proofs (); + Pp.msg_warning (str "Reset command occurred in non-interactive mode."); + Lib.reset_label lbl + with Backtrack.Invalid | Not_found -> error "Invalid Reset." + + +let vernac_reset_initial () = + if Backtrack.is_active () then + Backtrack.reset_initial () + else begin + Pp.msg_warning (str "Reset command occurred in non-interactive mode."); + Lib.reset_label Lib.first_command_label + end + +(* For compatibility with ProofGeneral: *) + +let vernac_backtrack snum pnum naborts = + Backtrack.backtrack snum pnum naborts; + try_print_subgoals () + + (********************) (* Proof management *) -let vernac_goal = function - | None -> () - | Some c -> - if not (refining()) then begin - let unnamed_kind = Lemma (* Arbitrary *) in - start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->()); - print_subgoals () - end else - error "repeated Goal not permitted in refining mode." - let vernac_abort = function | None -> + Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()]; delete_current_proof (); if_verbose message "Current goal aborted"; if !pcoq <> None then (Option.get !pcoq).abort "" | Some id -> + Backtrack.mark_unreachable [snd id]; delete_proof id; let s = string_of_id (snd id) in if_verbose message ("Goal "^s^" aborted"); @@ -1201,76 +1477,85 @@ let vernac_abort = function let vernac_abort_all () = if refining() then begin + Backtrack.mark_unreachable (Pfedit.get_all_proof_names ()); delete_all_proofs (); message "Current goals aborted" end else error "No proof-editing in progress." -let vernac_restart () = restart_proof(); print_subgoals () +let vernac_restart () = + Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()]; + restart_proof(); print_subgoals () - (* Proof switching *) +let vernac_undo n = + let d = Pfedit.current_proof_depth () - n in + Backtrack.mark_unreachable ~after:d [Pfedit.get_current_proof_name ()]; + Pfedit.undo n; print_subgoals () -let vernac_suspend = suspend_proof +let vernac_undoto n = + Backtrack.mark_unreachable ~after:n [Pfedit.get_current_proof_name ()]; + Pfedit.undo_todepth n; + print_subgoals () -let vernac_resume = function - | None -> resume_last_proof () - | Some id -> resume_proof id +let vernac_focus gln = + let p = Proof_global.give_me_the_proof () in + let n = match gln with None -> 1 | Some n -> n in + if n = 0 then + Util.error "Invalid goal number: 0. Goal numbering starts with 1." + else + Proof.focus focus_command_cond () n p; print_subgoals () -let vernac_undo n = - undo n; + (* Unfocuses one step in the focus stack. *) +let vernac_unfocus () = + let p = Proof_global.give_me_the_proof () in + Proof.unfocus command_focus p; print_subgoals () + +(* Checks that a proof is fully unfocused. Raises an error if not. *) +let vernac_unfocused () = + let p = Proof_global.give_me_the_proof () in + if Proof.unfocused p then + msg (str"The proof is indeed fully unfocused.") + else + error "The proof is not fully unfocused." + + +(* BeginSubproof / EndSubproof. + BeginSubproof (vernac_subproof) focuses on the first goal, or the goal + given as argument. + EndSubproof (vernac_end_subproof) unfocuses from a BeginSubproof, provided + that the proof of the goal has been completed. +*) +let subproof_kind = Proof.new_focus_kind () +let subproof_cond = Proof.done_cond subproof_kind + +let vernac_subproof gln = + let p = Proof_global.give_me_the_proof () in + begin match gln with + | None -> Proof.focus subproof_cond () 1 p + | Some n -> Proof.focus subproof_cond () n p + end ; print_subgoals () -(* backtrack with [naborts] abort, then undo_todepth to [pnum], then - back-to state number [snum]. This allows to backtrack proofs and - state with one command (easier for proofgeneral). *) -let vernac_backtrack snum pnum naborts = - for i = 1 to naborts do vernac_abort None done; - undo_todepth pnum; - vernac_backto snum; - Pp.flush_all(); - (* there may be no proof in progress, even if no abort *) - (try print_subgoals () with UserError _ -> ()) +let vernac_end_subproof () = + let p = Proof_global.give_me_the_proof () in + Proof.unfocus subproof_kind p ; print_subgoals () -let vernac_focus gln = - check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; - match gln with - | None -> traverse_nth_goal 1; print_subgoals () - | Some n -> traverse_nth_goal n; print_subgoals () +let vernac_bullet (bullet:Proof_global.Bullet.t) = + let p = Proof_global.give_me_the_proof () in + Proof.transaction p + (fun () -> Proof_global.Bullet.put p bullet); + (* Makes the focus visible in emacs by re-printing the goal. *) + if !Flags.print_emacs then print_subgoals () - (* Reset the focus to the top of the tree *) -let vernac_unfocus () = - check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; - make_focus 0; reset_top_of_script (); print_subgoals () - -let vernac_go = function - | GoTo n -> Pfedit.traverse n;show_node() - | GoTop -> Pfedit.reset_top_of_tree ();show_node() - | GoNext -> Pfedit.traverse_next_unproven ();show_node() - | GoPrev -> Pfedit.traverse_prev_unproven ();show_node() - -let apply_subproof f occ = - let pts = get_pftreestate() in - let evc = evc_of_pftreestate pts in - let rec aux pts = function - | [] -> pts - | (n::l) -> aux (Tacmach.traverse n pts) occ in - let pts = aux pts (occ@[-1]) in - let pf = proof_of_pftreestate pts in - f evc (Global.named_context()) pf - -let explain_proof occ = - msg (apply_subproof (fun evd _ -> print_treescript evd) occ) - -let explain_tree occ = - msg (apply_subproof print_proof occ) let vernac_show = function - | ShowGoal nopt -> - if !pcoq <> None then (Option.get !pcoq).show_goal nopt - else msg (match nopt with - | None -> pr_open_subgoals () - | Some n -> pr_nth_open_subgoal n) + | ShowGoal goalref -> + if !pcoq <> None then (Option.get !pcoq).show_goal goalref + else msg (match goalref with + | OpenSubgoals -> pr_open_subgoals () + | NthGoal n -> pr_nth_open_subgoal n + | GoalId id -> pr_goal_by_id id) | ShowGoalImplicitly None -> Constrextern.with_implicits msg (pr_open_subgoals ()) | ShowGoalImplicitly (Some n) -> @@ -1285,17 +1570,15 @@ let vernac_show = function | ShowIntros all -> show_intro all | ShowMatch id -> show_match id | ShowThesis -> show_thesis () - | ExplainProof occ -> explain_proof occ - | ExplainTree occ -> explain_tree occ let vernac_check_guard () = let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts in - let (pfterm,_) = extract_open_pftreestate pts in + let pfterm = List.hd (Proof.partial_proof pts) in let message = try - Inductiveops.control_only_guard (Evd.evar_env (goal_of_proof pf)) + let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in + Inductiveops.control_only_guard (Goal.V82.env sigma gl) pfterm; (str "The condition holds up to here") with UserError(_,s) -> @@ -1325,8 +1608,8 @@ let interp c = match c with | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l - | VernacFixpoint (l,b) -> vernac_fixpoint l b - | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b + | VernacFixpoint l -> vernac_fixpoint l + | VernacCoFixpoint l -> vernac_cofixpoint l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l @@ -1354,21 +1637,13 @@ let interp c = match c with | VernacInstance (abst, glob, sup, inst, props, pri) -> vernac_instance abst glob sup inst props pri | VernacContext sup -> vernac_context sup - | VernacDeclareInstance (glob, id) -> vernac_declare_instance glob id + | VernacDeclareInstances (glob, ids) -> vernac_declare_instances glob ids | VernacDeclareClass id -> vernac_declare_class id (* Solving *) | VernacSolve (n,tac,b) -> vernac_solve n tac b | VernacSolveExistential (n,c) -> vernac_solve_existential n c - (* MMode *) - - | VernacDeclProof -> vernac_decl_proof () - | VernacReturn -> vernac_return () - | VernacProofInstr stp -> vernac_proof_instr stp - - (* /MMode *) - (* Auxiliary file and library management *) | VernacRequireFrom (exp,spec,f) -> vernac_require_from exp spec f | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias @@ -1382,7 +1657,6 @@ let interp c = match c with | VernacRestoreState s -> vernac_restore_state s (* Resetting *) - | VernacRemoveName id -> Lib.remove_name id | VernacResetName id -> vernac_reset_name id | VernacResetInitial -> vernac_reset_initial () | VernacBack n -> vernac_back n @@ -1391,9 +1665,11 @@ let interp c = match c with (* Commands *) | VernacDeclareTacticDefinition def -> vernac_declare_tactic_definition def | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b + | VernacRemoveHints (local,dbnames,ids) -> vernac_remove_hints local dbnames ids | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l + | VernacArguments (local, qid, l, narg, flags) -> vernac_declare_arguments local qid l narg flags | VernacReserve bl -> vernac_reserve bl | VernacGeneralizable (local,gen) -> vernac_generalizable local gen | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl @@ -1417,17 +1693,23 @@ let interp c = match c with | VernacAbort id -> vernac_abort id | VernacAbortAll -> vernac_abort_all () | VernacRestart -> vernac_restart () - | VernacSuspend -> vernac_suspend () - | VernacResume id -> vernac_resume id | VernacUndo n -> vernac_undo n - | VernacUndoTo n -> undo_todepth n + | VernacUndoTo n -> vernac_undoto n | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () - | VernacGo g -> vernac_go g + | VernacUnfocused -> vernac_unfocused () + | VernacBullet b -> vernac_bullet b + | VernacSubproof n -> vernac_subproof n + | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof tac -> vernac_set_end_tac tac + | VernacProof (None, None) -> print_subgoals () + | VernacProof (Some tac, None) -> vernac_set_end_tac tac ; print_subgoals () + | VernacProof (None, Some l) -> vernac_set_used_variables l ; print_subgoals () + | VernacProof (Some tac, Some l) -> + vernac_set_end_tac tac; vernac_set_used_variables l ; print_subgoals () + | VernacProofMode mn -> Proof_global.set_proof_mode mn (* Toplevel control *) | VernacToplevelControl e -> raise e |