diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r-- | toplevel/vernacentries.ml | 680 |
1 files changed, 354 insertions, 326 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 385afbec..c4286900 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 12343 2009-09-17 17:02:03Z glondu $ i*) +(*i $Id$ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -36,6 +36,7 @@ open Topconstr open Pretyping open Redexpr open Syntax_def +open Lemmas (* Pcoq hooks *) @@ -44,7 +45,7 @@ type pcoq_hook = { solve : int -> unit; abort : string -> unit; search : searchable -> dir_path list * bool -> unit; - print_name : reference -> unit; + print_name : reference Genarg.or_by_notation -> unit; print_check : Environ.env -> Environ.unsafe_judgment -> unit; print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> Environ.unsafe_judgment -> unit; @@ -59,7 +60,7 @@ let set_pcoq_hook f = pcoq := Some f let cl_of_qualid = function | FunClass -> Classops.CL_FUN | SortClass -> Classops.CL_SORT - | RefClass r -> Class.class_of_global (global_with_alias r) + | RefClass r -> Class.class_of_global (Smartlocate.smart_global r) (*******************) (* "Show" commands *) @@ -72,7 +73,7 @@ let show_proof () = 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" -> " ++ + prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++ pr_ltype ty ++ fnl ()) meta_types ++ str"Proof: " ++ pr_lconstr (Evarutil.nf_evar evc pfterm)) @@ -90,7 +91,7 @@ let show_node () = str" " ++ hov 0 (prlist_with_sep pr_fnl pr_goal (List.map goal_of_proof spfl))))) - + let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts @@ -101,9 +102,9 @@ let show_thesis () = msgnl (anomaly "TODO" ) let show_top_evars () = - let pfts = get_pftreestate () in - let gls = top_goal_of_pftreestate pfts in - let sigma = project gls in + let pfts = get_pftreestate () in + let gls = top_goal_of_pftreestate pfts in + let sigma = project gls in msg (pr_evars_int 1 (Evarutil.non_instantiated sigma)) let show_prooftree () = @@ -119,40 +120,40 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () let show_intro all = let pf = get_pftreestate() in let gl = nth_goal_of_pftreestate 1 pf in - let l,_= Sign.decompose_prod_assum (strip_outer_cast (pf_concl gl)) in - if all - then - let lid = Tactics.find_intro_names l gl in + let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in + if all + then + let lid = Tactics.find_intro_names l gl in msgnl (hov 0 (prlist_with_sep spc pr_id lid)) - else - try + else + try let n = list_last l in 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" +let id_of_name = function + | Names.Anonymous -> id_of_string "x" | Names.Name x -> x (* Building of match expression *) (* From ide/coq.ml *) -let make_cases s = +let make_cases s = let qualified_name = Libnames.qualid_of_string s in let glob_ref = Nametab.locate qualified_name in match glob_ref with - | Libnames.IndRef i -> + | Libnames.IndRef i -> let {Declarations.mind_nparams = np} - , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } + , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } = Global.lookup_inductive i in - Util.array_fold_right2 - (fun n t l -> + 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 - let rec rename avoid = function + let rec rename avoid = function | [] -> [] - | (n,_)::l -> - let n' = Termops.next_global_ident_away true (id_of_name n) avoid in + | (n,_)::l -> + let n' = Namegen.next_ident_away_in_goal (id_of_name 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) @@ -160,18 +161,18 @@ let make_cases s = | _ -> raise Not_found -let show_match id = +let show_match id = try let s = string_of_id (snd id) in - let patterns = make_cases s in - let cases = - List.fold_left - (fun acc x -> + 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 ^ ")" + | x::l -> + "| (" ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ ")" ^ " => \n" ^ acc) "end" patterns in msg (str ("match # with\n" ^ cases)) @@ -196,7 +197,7 @@ let print_modules () = and loaded = Library.loaded_libraries () in let loaded_opened = list_intersect loaded opened and only_loaded = list_subtract loaded opened in - str"Loaded and imported library files: " ++ + str"Loaded and imported library files: " ++ pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++ str"Loaded and not imported library files: " ++ pr_vertical_list pr_dirpath only_loaded @@ -213,7 +214,7 @@ let print_module r = with Not_found -> msgnl (str"Unknown Module " ++ pr_qualid qid) -let print_modtype r = +let print_modtype r = let (loc,qid) = qualid_of_reference r in try let kn = Nametab.locate_modtype qid in @@ -226,7 +227,7 @@ let dump_universes s = try Univ.dump_universes output (Global.universes ()); close_out output; - msgnl (str ("Universes written to file \""^s^"\".")) + msgnl (str ("Universes written to file \""^s^"\".")) with e -> close_out output; raise e @@ -252,7 +253,7 @@ let msg_notfound_library loc qid = function strbrk "Cannot find a physical path bound to logical path " ++ pr_dirpath dir ++ str".") | Library.LibNotFound -> - msgnl (hov 0 + msgnl (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")) | e -> assert false @@ -261,22 +262,31 @@ let print_located_library r = try msg_found_library (Library.locate_qualified_library false qid) with e -> msg_notfound_library loc qid e -let print_located_module r = +let print_located_module r = let (loc,qid) = qualid_of_reference r in let msg = - try + try let dir = Nametab.full_name_module qid in str "Module " ++ pr_dirpath dir with Not_found -> (if fst (repr_qualid qid) = empty_dirpath then str "No module is referred to by basename " - else + else str "No module is referred to by name ") ++ pr_qualid qid - in msgnl msg + in msgnl msg -let global_with_alias r = - let gr = global_with_alias r in - Dumpglob.add_glob (loc_of_reference r) gr; +let print_located_tactic r = + let (loc,qid) = qualid_of_reference r in + msgnl + (try + str "Ltac " ++ + pr_path (Nametab.path_of_tactic (Nametab.locate_tactic qid)) + with Not_found -> + str "No Ltac definition is referred to by " ++ pr_qualid qid) + +let smart_global r = + let gr = Smartlocate.smart_global r in + Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr; gr (**********) @@ -286,13 +296,13 @@ let vernac_syntax_extension = Metasyntax.add_syntax_extension let vernac_delimiters = Metasyntax.add_delimiters -let vernac_bind_scope sc cll = +let vernac_bind_scope sc cll = List.iter (fun cl -> Metasyntax.add_class_scope sc (cl_of_qualid cl)) cll let vernac_open_close_scope = Notation.open_close_scope let vernac_arguments_scope local r scl = - Notation.declare_arguments_scope local (global_with_alias r) scl + Notation.declare_arguments_scope local (smart_global r) scl let vernac_infix = Metasyntax.add_infix @@ -306,28 +316,26 @@ let start_proof_and_print k l hook = print_subgoals (); if !pcoq <> None then (Option.get !pcoq).start_proof () -let vernac_definition (local,_,_ as k) (loc,id as lid) def hook = - Dumpglob.dump_definition lid false "def"; +let vernac_definition (local,boxed,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 | ProveBody (bl,t) -> (* local binders, typ *) - if Lib.is_modtype () then - errorlabstrm "Vernacentries.VernacDefinition" - (str "Proof editing mode not supported in module types") - else - let hook _ _ = () in - start_proof_and_print (local,DefinitionBody Definition) - [Some lid, (bl,t)] hook + let hook _ _ = () in + start_proof_and_print (local,DefinitionBody Definition) + [Some lid, (bl,t,None)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None - | Some r -> - let (evc,env)= Command.get_current_context () in + | Some r -> + let (evc,env)= get_current_context () in Some (interp_redexp env evc r) in - declare_definition id k bl red_option c typ_opt hook) - + let ce,imps = interp_definition boxed bl red_option c typ_opt in + declare_definition id (local,k) ce imps hook) + let vernac_start_proof kind l lettop hook = if Dumpglob.dump () then - List.iter (fun (id, _) -> + List.iter (fun (id, _) -> match id with | Some lid -> Dumpglob.dump_definition lid false "prf" | None -> ()) l; @@ -335,9 +343,6 @@ let vernac_start_proof kind l lettop hook = if lettop then errorlabstrm "Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode."); - if Lib.is_modtype () then - errorlabstrm "Vernacentries.StartProof" - (str "Proof editing mode not supported in module types."); start_proof_and_print (Global, Proof kind) l hook let vernac_end_proof = function @@ -361,95 +366,90 @@ let vernac_exact_proof c = else errorlabstrm "Vernacentries.ExactProof" (strbrk "Command 'Proof ...' can only be used at the beginning of the proof.") - + let vernac_assumption kind l nl= + if Pfedit.refining () then + errorlabstrm "" + (str "Cannot declare an assumption while in proof editing mode."); let global = fst kind = Global in - List.iter (fun (is_coe,(idl,c)) -> + List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then - List.iter (fun lid -> - if global then Dumpglob.dump_definition lid false "ax" + List.iter (fun lid -> + if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl; - declare_assumption idl is_coe kind [] c false [] nl) l + let t,imps = interp_assumption [] c in + declare_assumptions idl is_coe kind t imps false nl) l -let vernac_record k finite struc binders sort nameopt cfs = - let const = match nameopt with +let vernac_record k finite infer struc binders sort nameopt cfs = + let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) | Some (_,id as lid) -> Dumpglob.dump_definition lid false "constr"; id in - let sigma = Evd.empty in - let env = Global.env() in - let s = Option.map (fun x -> - let s = Reductionops.whd_betadeltaiota env sigma (interp_constr sigma env x) in - match kind_of_term s with - | Sort s -> s - | _ -> user_err_loc - (constr_loc x,"definition_structure", str "Sort expected.")) sort - in if Dumpglob.dump () then ( Dumpglob.dump_definition (snd struc) false "rec"; List.iter (fun ((_, x), _) -> match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); - ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,s)) - -let vernac_inductive finite indl = + ignore(Record.definition_structure (k,finite,infer,struc,binders,cfs,const,sort)) + +let vernac_inductive finite infer indl = if Dumpglob.dump () then List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> - match cstrs with - | Constructors cstrs -> - Dumpglob.dump_definition lid false "ind"; - List.iter (fun (_, (lid, _)) -> - Dumpglob.dump_definition lid false "constr") cstrs - | _ -> () (* dumping is done by vernac_record (called below) *) ) - indl; + match cstrs with + | Constructors cstrs -> + Dumpglob.dump_definition lid false "ind"; + List.iter (fun (_, (lid, _)) -> + Dumpglob.dump_definition lid false "constr") cstrs + | _ -> () (* dumping is done by vernac_record (called below) *) ) + indl; match indl with - | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] -> + | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> vernac_record (match b with Class true -> Class false | _ -> b) - finite id bl c oc fs - | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> - let f = + finite infer id bl c oc fs + | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> + let f = let (coe, ((loc, id), ce)) = l in - ((coe, AssumExpr ((loc, Name id), ce)), None) - in vernac_record (Class true) finite id bl c None [f] - | [ ( id , bl , c , Class true, _), _ ] -> + ((coe, AssumExpr ((loc, Name id), ce)), []) + 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" | [ ( id , bl , c , Class false, Constructors _), _ ] -> Util.error "Inductive classes not supported" - | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> + | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> Util.error "where clause not supported for (co)inductive records" - | _ -> let unpack = function + | _ -> let unpack = function | ( (_, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn | _ -> Util.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in - Command.build_mutual indl (recursivity_flag_of_kind finite) + do_mutual_inductive indl (recursivity_flag_of_kind finite) -let vernac_fixpoint l b = +let vernac_fixpoint l b = if Dumpglob.dump () then List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - build_recursive l b + do_fixpoint l b let vernac_cofixpoint l b = if Dumpglob.dump () then List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - build_corecursive l b + do_cofixpoint l b -let vernac_scheme = build_scheme +let vernac_scheme = Indschemes.do_scheme -let vernac_combined_scheme = build_combined_scheme +let vernac_combined_scheme = Indschemes.do_combined_scheme (**********************) (* Modules *) let vernac_import export refl = - let import ref = + let import ref = Library.import_module export (qualid_of_reference ref) in List.iter import refl; Lib.add_frozen_state () -let vernac_declare_module export (loc, id) binders_ast mty_ast_o = +let vernac_declare_module export (loc, id) binders_ast mty_ast = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then @@ -461,21 +461,22 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o = "Remove the \"Export\" and \"Import\" keywords from every functor " ^ "argument.") else (idl,ty)) binders_ast in - let mp = Declaremods.declare_module + let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast (Some mty_ast_o) None - in + Modintern.interp_modexpr_or_modtype + id binders_ast (Enforce mty_ast) [] + in Dumpglob.dump_moddef loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is declared"); Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export -let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = +let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections."; - match mexpr_ast_o with - | None -> + match mexpr_ast_l with + | [] -> check_no_pending_proofs (); let binders_ast,argsexport = List.fold_right @@ -483,17 +484,17 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast ([],[]) in let mp = Declaremods.start_module Modintern.interp_modtype export - id binders_ast mty_ast_o + id binders_ast mty_ast_o in Dumpglob.dump_moddef loc mp "mod"; - if_verbose message + if_verbose message ("Interactive Module "^ string_of_id id ^" started") ; List.iter (fun (export,id) -> Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport - | Some _ -> + | _::_ -> let binders_ast = List.map (fun (export,idl,ty) -> if export <> None then @@ -501,46 +502,48 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = " the definition is interactive. Remove the \"Export\" and " ^ "\"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = Declaremods.declare_module + let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast mty_ast_o mexpr_ast_o + Modintern.interp_modexpr_or_modtype + id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef loc mp "mod"; - if_verbose message + if_verbose message ("Module "^ string_of_id id ^" is defined"); Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export -let vernac_end_module export (loc,id) = - let mp = Declaremods.end_module id in - Dumpglob.dump_modref loc mp "mod"; - if_verbose message ("Module "^ string_of_id id ^" is defined") ; - Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export - +let vernac_end_module export (loc,id as lid) = + let mp = Declaremods.end_module () in + Dumpglob.dump_modref loc mp "mod"; + if_verbose message ("Module "^ string_of_id id ^" is defined") ; + Option.iter (fun export -> vernac_import export [Ident lid]) export -let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = +let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections."; - - match mty_ast_o with - | None -> + + match mty_ast_l with + | [] -> check_no_pending_proofs (); - let binders_ast,argsexport = - List.fold_right + let binders_ast,argsexport = + List.fold_right (fun (export,idl,ty) (args,argsexport) -> - (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast + (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast ([],[]) in - let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in + + let mp = Declaremods.start_modtype + Modintern.interp_modtype id binders_ast mty_sign in Dumpglob.dump_moddef loc mp "modtype"; - if_verbose message + if_verbose message ("Interactive Module Type "^ string_of_id id ^" started"); List.iter (fun (export,id) -> Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport - - | Some base_mty -> + + | _ :: _ -> let binders_ast = List.map (fun (export,idl,ty) -> if export <> None then @@ -548,70 +551,66 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = " the definition is interactive. Remove the \"Export\" " ^ "and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = Declaremods.declare_modtype Modintern.interp_modtype - id binders_ast base_mty in + let mp = Declaremods.declare_modtype Modintern.interp_modtype + Modintern.interp_modexpr_or_modtype + id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef loc mp "modtype"; - if_verbose message + if_verbose message ("Module Type "^ string_of_id id ^" is defined") - let vernac_end_modtype (loc,id) = - let mp = Declaremods.end_modtype id in - Dumpglob.dump_modref loc mp "modtype"; - if_verbose message - ("Module Type "^ string_of_id id ^" is defined") - -let vernac_include = function - | CIMTE mty_ast -> - Declaremods.declare_include Modintern.interp_modtype mty_ast false - | CIME mexpr_ast -> - Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true - - - + let mp = Declaremods.end_modtype () in + Dumpglob.dump_modref loc mp "modtype"; + if_verbose message ("Module Type "^ string_of_id id ^" is defined") + +let vernac_include l = + Declaremods.declare_include Modintern.interp_modexpr_or_modtype l + (**********************) (* Gallina extensions *) - (* Sections *) +(* Sections *) let vernac_begin_section (_, id as lid) = check_no_pending_proofs (); Dumpglob.dump_definition lid true "sec"; Lib.open_section id -let vernac_end_section (loc, id) = - - Dumpglob.dump_reference loc - (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; - Lib.close_section id +let vernac_end_section (loc,_) = + Dumpglob.dump_reference loc + (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; + Lib.close_section () -let vernac_end_segment lid = +(* Dispatcher of the "End" command *) + +let vernac_end_segment (_,id as lid) = check_no_pending_proofs (); - let o = try Lib.what_is_opened () with - Not_found -> error "There is nothing to end." in - match o with - | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export lid - | _,Lib.OpenedModtype _ -> vernac_end_modtype lid - | _,Lib.OpenedSection _ -> vernac_end_section lid - | _ -> anomaly "No more opened things" + match Lib.find_opening_node id with + | Lib.OpenedModule (export,_,_) -> vernac_end_module export lid + | Lib.OpenedModtype _ -> vernac_end_modtype lid + | Lib.OpenedSection _ -> vernac_end_section lid + | _ -> anomaly "No more opened things" + +(* Libraries *) let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in - if Dumpglob.dump () then begin - let modrefl = Flags.silently (List.map Library.try_locate_qualified_library) qidl in - List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl) - end; - Library.require_library qidl import + let modrefl = Flags.silently (List.map Library.try_locate_qualified_library) qidl in + if Dumpglob.dump () then + List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl); + Library.require_library_from_dirpath modrefl import + +(* Coercions and canonical structures *) let vernac_canonical r = - Recordops.declare_canonical_structure (global_with_alias r) + Recordops.declare_canonical_structure (smart_global r) let vernac_coercion stre ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - let ref' = global_with_alias ref in + let ref' = smart_global ref in Class.try_add_new_coercion_with_target ref' stre source target; - if_verbose message ((string_of_reference ref) ^ " is now a coercion") + 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 @@ -619,18 +618,20 @@ let vernac_identity_coercion stre id qids qidt = Class.try_add_new_identity_coercion id stre source target (* Type classes *) - -let vernac_instance glob sup inst props pri = + +let vernac_instance abst glob sup inst props pri = Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~global:glob sup inst props pri) + ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri) let vernac_context l = List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l; Classes.context l -let vernac_declare_instance id = - Dumpglob.dump_definition id false "inst"; - Classes.declare_instance false id +let vernac_declare_instance glob id = + Classes.declare_instance glob id + +let vernac_declare_class id = + Classes.declare_class id (***********) (* Solving *) @@ -639,12 +640,12 @@ let vernac_solve n tcom b = error "Unknown command of the non proof-editing mode."; Decl_mode.check_not_proof_mode "Unknown proof instruction"; begin - if b then + 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 *) + (* 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; @@ -656,9 +657,9 @@ let vernac_solve n tcom b = (* A command which should be a tactic. It has been added by Christine to patch an error in the design of the proof machine, and enables to instantiate existential variables when - there are no more goals to solve. It cannot be a tactic since + there are no more goals to solve. It cannot be a tactic since all tactics fail if there are no further goals to prove. *) - + let vernac_solve_existential = instantiate_nth_evar_com let vernac_set_end_tac tac = @@ -670,9 +671,9 @@ let vernac_set_end_tac tac = (***********************) (* Proof Language Mode *) -let vernac_decl_proof () = +let vernac_decl_proof () = check_not_proof_mode "Already in Proof Mode"; - if tree_solved () then + if tree_solved () then error "Nothing left to prove here." else begin @@ -680,17 +681,17 @@ let vernac_decl_proof () = print_subgoals () end -let vernac_return () = +let vernac_return () = match get_current_mode () with Mode_tactic -> Decl_proof_instr.return_from_tactic_mode (); print_subgoals () - | Mode_proof -> + | Mode_proof -> error "\"return\" is only used after \"escape\"." - | Mode_none -> - error "There is no proof to end." + | Mode_none -> + error "There is no proof to end." -let vernac_proof_instr instr = +let vernac_proof_instr instr = Decl_proof_instr.proof_instr instr; print_subgoals () @@ -718,8 +719,8 @@ let vernac_add_ml_path isrec path = (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (System.expand_path_macros path) -let vernac_declare_ml_module l = - Mltop.declare_ml_modules (List.map System.expand_path_macros l) +let vernac_declare_ml_module local l = + Mltop.declare_ml_modules local (List.map System.expand_path_macros l) let vernac_chdir = function | None -> message (Sys.getcwd()) @@ -759,71 +760,77 @@ let vernac_backto n = Lib.reset_label n (************) (* Commands *) -let vernac_declare_tactic_definition = Tacinterp.add_tacdef +let vernac_declare_tactic_definition (local,x,def) = + Tacinterp.add_tacdef local x def -let vernac_create_hintdb local id b = +let vernac_create_hintdb local id b = Auto.create_hint_db local id full_transparent_state b -let vernac_hints = Auto.add_hints +let vernac_hints local lb h = + Auto.add_hints local lb (Auto.interp_hints h) let vernac_syntactic_definition lid = Dumpglob.dump_definition lid false "syndef"; - Command.syntax_definition (snd lid) - + Metasyntax.add_syntactic_definition (snd lid) + let vernac_declare_implicits local r = function | Some imps -> - Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false - (List.map (fun (ex,b,f) -> ex, (b,f)) imps) - | None -> - Impargs.declare_implicits local (global_with_alias r) + Impargs.declare_manual_implicits local (smart_global r) ~enriching:false + (List.map (fun (ex,b,f) -> ex, (b,true,f)) imps) + | None -> + Impargs.declare_implicits local (smart_global r) -let vernac_reserve 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 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) + in List.iter sb_decl bl + +let vernac_generalizable = Implicit_quantifiers.declare_generalizable let make_silent_if_not_pcoq b = - if !pcoq <> None then + if !pcoq <> None then error "Turning on/off silent flag is not supported in Pcoq mode." else make_silent b let _ = - declare_bool_option + declare_bool_option { optsync = false; optname = "silent"; - optkey = (PrimaryTable "Silent"); + optkey = ["Silent"]; optread = is_silent; optwrite = make_silent_if_not_pcoq } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "implicit arguments"; - optkey = (SecondaryTable ("Implicit","Arguments")); + optkey = ["Implicit";"Arguments"]; optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "strict implicit arguments"; - optkey = (SecondaryTable ("Strict","Implicit")); + optkey = ["Strict";"Implicit"]; optread = Impargs.is_strict_implicit_args; optwrite = Impargs.make_strict_implicit_args } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "strong strict implicit arguments"; - optkey = (TertiaryTable ("Strongly","Strict","Implicit")); + optkey = ["Strongly";"Strict";"Implicit"]; optread = Impargs.is_strongly_strict_implicit_args; optwrite = Impargs.make_strongly_strict_implicit_args } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "contextual implicit arguments"; - optkey = (SecondaryTable ("Contextual","Implicit")); + optkey = ["Contextual";"Implicit"]; optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } @@ -831,159 +838,167 @@ let _ = (* declare_bool_option *) (* { optsync = true; *) (* optname = "forceable implicit arguments"; *) -(* optkey = (SecondaryTable ("Forceable","Implicit")); *) +(* optkey = ["Forceable";"Implicit")); *) (* optread = Impargs.is_forceable_implicit_args; *) (* optwrite = Impargs.make_forceable_implicit_args } *) let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "implicit status of reversible patterns"; - optkey = (TertiaryTable ("Reversible","Pattern","Implicit")); + optkey = ["Reversible";"Pattern";"Implicit"]; optread = Impargs.is_reversible_pattern_implicit_args; optwrite = Impargs.make_reversible_pattern_implicit_args } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "maximal insertion of implicit"; - optkey = (TertiaryTable ("Maximal","Implicit","Insertion")); + optkey = ["Maximal";"Implicit";"Insertion"]; optread = Impargs.is_maximal_implicit_args; optwrite = Impargs.make_maximal_implicit_args } let _ = - declare_bool_option + declare_bool_option + { optsync = true; + optname = "automatic introduction of variables"; + optkey = ["Automatic";"Introduction"]; + optread = Flags.is_auto_intros; + optwrite = make_auto_intros } + +let _ = + declare_bool_option { optsync = true; optname = "coercion printing"; - optkey = (SecondaryTable ("Printing","Coercions")); + optkey = ["Printing";"Coercions"]; optread = (fun () -> !Constrextern.print_coercions); optwrite = (fun b -> Constrextern.print_coercions := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "printing of existential variable instances"; - optkey = (TertiaryTable ("Printing","Existential","Instances")); + optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Constrextern.print_evar_arguments); optwrite = (:=) Constrextern.print_evar_arguments } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "implicit arguments printing"; - optkey = (SecondaryTable ("Printing","Implicit")); + optkey = ["Printing";"Implicit"]; optread = (fun () -> !Constrextern.print_implicits); optwrite = (fun b -> Constrextern.print_implicits := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "implicit arguments defensive printing"; - optkey = (TertiaryTable ("Printing","Implicit","Defensive")); + optkey = ["Printing";"Implicit";"Defensive"]; optread = (fun () -> !Constrextern.print_implicits_defensive); optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "projection printing using dot notation"; - optkey = (SecondaryTable ("Printing","Projections")); + optkey = ["Printing";"Projections"]; optread = (fun () -> !Constrextern.print_projections); optwrite = (fun b -> Constrextern.print_projections := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "notations printing"; - optkey = (SecondaryTable ("Printing","Notations")); + optkey = ["Printing";"Notations"]; optread = (fun () -> not !Constrextern.print_no_symbol); optwrite = (fun b -> Constrextern.print_no_symbol := not b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "raw printing"; - optkey = (SecondaryTable ("Printing","All")); + optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "use of virtual machine inside the kernel"; - optkey = (SecondaryTable ("Virtual","Machine")); + optkey = ["Virtual";"Machine"]; optread = (fun () -> Vconv.use_vm ()); optwrite = (fun b -> Vconv.set_use_vm b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "use of boxed definitions"; - optkey = (SecondaryTable ("Boxed","Definitions")); + optkey = ["Boxed";"Definitions"]; optread = Flags.boxed_definitions; - optwrite = (fun b -> Flags.set_boxed_definitions b) } + optwrite = (fun b -> Flags.set_boxed_definitions b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "use of boxed values"; - optkey = (SecondaryTable ("Boxed","Values")); + optkey = ["Boxed";"Values"]; optread = (fun _ -> not (Vm.transp_values ())); - optwrite = (fun b -> Vm.set_transp_values (not b)) } + optwrite = (fun b -> Vm.set_transp_values (not b)) } let _ = declare_int_option - { optsync=false; - optkey=PrimaryTable("Undo"); - optname="the undo limit"; - optread=Pfedit.get_undo; - optwrite=Pfedit.set_undo } + { optsync = false; + optname = "the undo limit"; + optkey = ["Undo"]; + optread = Pfedit.get_undo; + optwrite = Pfedit.set_undo } let _ = declare_int_option - { optsync=false; - optkey=SecondaryTable("Hyps","Limit"); - optname="the hypotheses limit"; - optread=Flags.print_hyps_limit; - optwrite=Flags.set_print_hyps_limit } + { optsync = false; + optname = "the hypotheses limit"; + optkey = ["Hyps";"Limit"]; + optread = Flags.print_hyps_limit; + optwrite = Flags.set_print_hyps_limit } let _ = declare_int_option - { optsync=true; - optkey=SecondaryTable("Printing","Depth"); - optname="the printing depth"; - optread=Pp_control.get_depth_boxes; - optwrite=Pp_control.set_depth_boxes } + { optsync = true; + optname = "the printing depth"; + optkey = ["Printing";"Depth"]; + optread = Pp_control.get_depth_boxes; + optwrite = Pp_control.set_depth_boxes } let _ = declare_int_option - { optsync=true; - optkey=SecondaryTable("Printing","Width"); - optname="the printing width"; - optread=Pp_control.get_margin; - optwrite=Pp_control.set_margin } + { optsync = true; + optname = "the printing width"; + optkey = ["Printing";"Width"]; + optread = Pp_control.get_margin; + optwrite = Pp_control.set_margin } let _ = declare_bool_option - { optsync=true; - optkey=SecondaryTable("Printing","Universes"); - optname="printing of universes"; - optread=(fun () -> !Constrextern.print_universes); - optwrite=(fun b -> Constrextern.print_universes:=b) } + { optsync = true; + optname = "printing of universes"; + optkey = ["Printing";"Universes"]; + optread = (fun () -> !Constrextern.print_universes); + optwrite = (fun b -> Constrextern.print_universes:=b) } let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) let _ = declare_bool_option - { optsync=false; - optkey=SecondaryTable("Ltac","Debug"); - optname="Ltac debug"; - optread=(fun () -> get_debug () <> Tactic_debug.DebugOff); - optwrite=vernac_debug } + { optsync = false; + optname = "Ltac debug"; + optkey = ["Ltac";"Debug"]; + optread = (fun () -> get_debug () <> Tactic_debug.DebugOff); + optwrite = vernac_debug } let vernac_set_opacity local str = let glob_ref r = - match global_with_alias r with + match smart_global r with | ConstRef sp -> EvalConstRef sp | VarRef id -> EvalVarRef id | _ -> error @@ -991,15 +1006,15 @@ let vernac_set_opacity local str = let str = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) str in Redexpr.set_strategy local str -let vernac_set_option key = function - | StringValue s -> set_string_option_value key s - | IntValue n -> set_int_option_value key (Some n) - | BoolValue b -> set_bool_option_value key b +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) + | BoolValue b -> set_bool_option_value_gen locality key b -let vernac_unset_option key = - try set_bool_option_value key false +let vernac_unset_option locality key = + try set_bool_option_value_gen locality key false with _ -> - set_int_option_value key None + set_int_option_value_gen locality key None let vernac_add_option key lv = let f = function @@ -1048,6 +1063,9 @@ let vernac_check_may_eval redexp glopt rc = then (Option.get !pcoq).print_eval redfun env evmap rc j else msg (print_eval redfun env evmap rc j) +let vernac_declare_reduction locality s r = + declare_red_expr locality s (interp_redexp (Global.env()) Evd.empty r) + (* The same but avoiding the current goal context if any *) let vernac_global_check c = let evmap = Evd.empty in @@ -1069,14 +1087,13 @@ let vernac_print = function | PrintModuleType qid -> print_modtype qid | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () - | PrintName qid -> + | PrintName qid -> if !pcoq <> None then (Option.get !pcoq).print_name qid else msg (print_name qid) - | PrintOpaqueName qid -> msg (print_opaque_name qid) | PrintGraph -> ppnl (Prettyp.print_graph()) | PrintClasses -> ppnl (Prettyp.print_classes()) | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses()) - | PrintInstances c -> ppnl (Prettyp.print_instances (global c)) + | PrintInstances c -> ppnl (Prettyp.print_instances (smart_global c)) | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid))) | PrintCoercions -> ppnl (Prettyp.print_coercions()) | PrintCoercionPaths (cls,clt) -> @@ -1084,7 +1101,7 @@ let vernac_print = function | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ()) | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ())) | PrintUniverses (Some s) -> dump_universes s - | PrintHint r -> Auto.print_hint_ref (global_with_alias r) + | 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 @@ -1099,7 +1116,7 @@ let vernac_print = function | PrintImplicit qid -> msg (print_impargs qid) (*spiwack: prints all the axioms and section variables used by a term *) | PrintAssumptions (o,r) -> - let cstr = constr_of_global (global_with_alias r) in + let cstr = constr_of_global (smart_global r) in let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ()) ~add_opaque:o cstr (Global.env ()) in msg (Printer.pr_assumptionset (Global.env ()) nassumptions) @@ -1107,7 +1124,7 @@ let vernac_print = function let global_module r = let (loc,qid) = qualid_of_reference r in try Nametab.full_name_module qid - with Not_found -> + with Not_found -> user_err_loc (loc, "global_module", str "Module/section " ++ pr_qualid qid ++ str " not found.") @@ -1126,12 +1143,12 @@ let interp_search_about_item = function | SearchString (s,None) when is_ident s -> GlobSearchString s | SearchString (s,sc) -> - try + try let ref = Notation.interp_notation_as_global_reference dummy_loc (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) - with UserError _ -> + with UserError _ -> error ("Unable to interp \""^s^"\" either as a reference or as an identifier component") @@ -1140,24 +1157,27 @@ let vernac_search s r = if !pcoq <> None then (Option.get !pcoq).search s r else match s with | SearchPattern c -> - let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in - Search.search_pattern pat r + let (_,c) = interp_open_constr_patvar Evd.empty (Global.env()) c in + Search.search_pattern c r | SearchRewrite c -> - let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in + let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in Search.search_rewrite pat r - | SearchHead ref -> - Search.search_by_head (global_with_alias ref) r + | SearchHead c -> + let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in + Search.search_by_head pat r | SearchAbout sl -> Search.search_about (List.map (on_snd interp_search_about_item) sl) r let vernac_locate = function - | LocateTerm qid -> msgnl (print_located_qualid qid) + | LocateTerm (Genarg.AN qid) -> msgnl (print_located_qualid qid) + | LocateTerm (Genarg.ByNotation (_,ntn,sc)) -> + ppnl + (Notation.locate_notation + (Constrextern.without_symbols pr_lrawconstr) 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 - | LocateNotation ntn -> - ppnl (Notation.locate_notation (Constrextern.without_symbols pr_lrawconstr) - (Metasyntax.standardize_locatable_notation ntn)) (********************) (* Proof management *) @@ -1169,7 +1189,7 @@ let vernac_goal = function let unnamed_kind = Lemma (* Arbitrary *) in start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->()); print_subgoals () - end else + end else error "repeated Goal not permitted in refining mode." let vernac_abort = function @@ -1214,14 +1234,14 @@ let vernac_backtrack snum pnum naborts = Pp.flush_all(); (* there may be no proof in progress, even if no abort *) (try print_subgoals () with UserError _ -> ()) - + let vernac_focus gln = check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; - match gln with + match gln with | None -> traverse_nth_goal 1; print_subgoals () | Some n -> traverse_nth_goal n; 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."; @@ -1238,7 +1258,7 @@ let apply_subproof f occ = let evc = evc_of_pftreestate pts in let rec aux pts = function | [] -> pts - | (n::l) -> aux (Tacmach.traverse n pts) occ in + | (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 @@ -1277,19 +1297,20 @@ let vernac_check_guard () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts in let (pfterm,_) = extract_open_pftreestate pts in - let message = - try + let message = + try Inductiveops.control_only_guard (Evd.evar_env (goal_of_proof pf)) - pfterm; + pfterm; (str "The condition holds up to here") - with UserError(_,s) -> + with UserError(_,s) -> (str ("Condition violated: ") ++s) - in + in msgnl message let interp c = match c with (* Control (done in vernac) *) - | (VernacTime _ | VernacList _ | VernacLoad _) -> assert false + | (VernacTime _|VernacList _|VernacLoad _|VernacTimeout _|VernacFail _) -> + assert false (* Syntax *) | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e) @@ -1307,21 +1328,21 @@ let interp c = match c with | VernacEndProof e -> vernac_end_proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl - | VernacInductive (finite,l) -> vernac_inductive finite l + | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l | VernacFixpoint (l,b) -> vernac_fixpoint l b | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l (* Modules *) - | VernacDeclareModule (export,lid,bl,mtyo) -> + | VernacDeclareModule (export,lid,bl,mtyo) -> vernac_declare_module export lid bl mtyo - | VernacDefineModule (export,lid,bl,mtyo,mexpro) -> - vernac_define_module export lid bl mtyo mexpro - | VernacDeclareModuleType (lid,bl,mtyo) -> - vernac_declare_module_type lid bl mtyo - | VernacInclude (in_ast) -> - vernac_include in_ast + | VernacDefineModule (export,lid,bl,mtys,mexprl) -> + vernac_define_module export lid bl mtys mexprl + | VernacDeclareModuleType (lid,bl,mtys,mtyo) -> + vernac_declare_module_type lid bl mtys mtyo + | VernacInclude in_asts -> + vernac_include in_asts (* Gallina extensions *) | VernacBeginSection lid -> vernac_begin_section lid @@ -1334,9 +1355,11 @@ let interp c = match c with | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t (* Type classes *) - | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri + | VernacInstance (abst, glob, sup, inst, props, pri) -> + vernac_instance abst glob sup inst props pri | VernacContext sup -> vernac_context sup - | VernacDeclareInstance id -> vernac_declare_instance id + | VernacDeclareInstance (glob, id) -> vernac_declare_instance glob id + | VernacDeclareClass id -> vernac_declare_class id (* Solving *) | VernacSolve (n,tac,b) -> vernac_solve n tac b @@ -1346,7 +1369,7 @@ let interp c = match c with | VernacDeclProof -> vernac_decl_proof () | VernacReturn -> vernac_return () - | VernacProofInstr stp -> vernac_proof_instr stp + | VernacProofInstr stp -> vernac_proof_instr stp (* /MMode *) @@ -1355,7 +1378,7 @@ let interp c = match c with | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias | VernacRemoveLoadPath s -> vernac_remove_loadpath s | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s - | VernacDeclareMLModule l -> vernac_declare_ml_module l + | VernacDeclareMLModule (local, l) -> vernac_declare_ml_module local l | VernacChdir s -> vernac_chdir s (* State management *) @@ -1370,20 +1393,22 @@ let interp c = match c with | VernacBackTo n -> vernac_backto n (* Commands *) - | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l + | VernacDeclareTacticDefinition def -> vernac_declare_tactic_definition def | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b | 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 - | VernacReserve (idl,c) -> vernac_reserve idl c + | VernacReserve bl -> vernac_reserve bl + | VernacGeneralizable (local,gen) -> vernac_generalizable local gen | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl - | VernacSetOption (key,v) -> vernac_set_option key v - | VernacUnsetOption key -> vernac_unset_option key + | VernacSetOption (locality,key,v) -> vernac_set_option locality key v + | VernacUnsetOption (locality,key) -> vernac_unset_option locality key | VernacRemoveOption (key,v) -> vernac_remove_option key v | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c + | VernacDeclareReduction (b,s,r) -> vernac_declare_reduction b s r | VernacGlobalCheck c -> vernac_global_check c | VernacPrint p -> vernac_print p | VernacSearch (s,r) -> vernac_search s r @@ -1392,7 +1417,7 @@ let interp c = match c with | VernacNop -> () (* Proof management *) - | VernacGoal t -> vernac_start_proof Theorem [None,([],t)] false (fun _ _->()) + | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] false (fun _ _->()) | VernacAbort id -> vernac_abort id | VernacAbortAll -> vernac_abort_all () | VernacRestart -> vernac_restart () @@ -1412,3 +1437,6 @@ let interp c = match c with (* Extensions *) | VernacExtend (opn,args) -> Vernacinterp.call (opn,args) + +let interp c = interp c ; check_locality () + |