diff options
44 files changed, 257 insertions, 224 deletions
@@ -58,6 +58,11 @@ Tools - Flag -no-native-compiler was removed and became the default for coqc. If precompilation of files for native conversion test is desired, use -native-compiler. +- The -compile command-line option now takes the full path of the considered + file, including the ".v" extension, and outputs a warning if such an extension + is lacking. +- The -require command-line option now takes a logical path of a given library + rather than a physical path. Changes from V8.5beta1 to V8.5beta2 =================================== diff --git a/Makefile.build b/Makefile.build index 018937fc6d..d8c8ba4e83 100644 --- a/Makefile.build +++ b/Makefile.build @@ -588,7 +588,7 @@ pluginsbyte: $(PLUGINS) theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d $(SHOW)'COQC -noinit $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) theories/Init/$* -noinit -R theories Coq + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml $(OCAML) $< $(TOTARGET) @@ -1032,7 +1032,7 @@ plugins/%_mod.ml: plugins/%.mllib %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQC) $* + $(HIDE)$(BOOTCOQC) $< ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 6335dfd324..0f1823a021 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -157,16 +157,16 @@ Add physical path {\em directory} to the {\ocaml} loadpath. Load \Coq~compiled file {\em file}{\tt .vo} -\item[{\tt -require} {\em file}]\ +\item[{\tt -require} {\em path}]\ - Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt - Require} {\em file}). + Load \Coq~compiled library {\em path} and import it (equivalent to {\tt + Require Import} {\em path}). -\item[{\tt -compile} {\em file},{\tt -compile-verbose} {\em file}, {\tt -batch}]\ +\item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ {\tt coqtop} options only used internally by {\tt coqc}. - This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} without/with a + This compiles file {\em file.v} into {\em file}{\tt .vo} without/with a copy of the contents of the file on standard input. This option implies options {\tt -batch} (exit just after arguments parsing). It is only available for {\tt coqtop}. diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 836944ab1c..e09feeb8eb 100644 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -208,7 +208,7 @@ Definition two : nat := S one. Actually \Coq~ allows several possible syntaxes: \begin{coq_example} -Definition three : nat := S two. +Definition three := S two : nat. \end{coq_example} Here is a way to define the doubling function, which expects an diff --git a/ide/preferences.ml b/ide/preferences.ml index 313d97086f..23426cad65 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -292,7 +292,7 @@ let attach_modifiers (pref : string preference) prefix = pref#connect#changed cb let modifier_for_navigation = - new preference ~name:["modifier_for_navigation"] ~init:"<Control><Alt>" ~repr:Repr.(string) + new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string) let modifier_for_templates = new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index f7ae30e7af..ba14f65d9e 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -122,7 +122,7 @@ let add_kn_delta_resolver kn kn' = let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2 -(** Extending a [substitution] *) +(** Extending a [substitution] without sequential composition *) let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index fc2b0441ca..cd9fa79216 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -68,8 +68,9 @@ val empty_subst : substitution val is_empty_subst : substitution -> bool -(** add_* add [arg2/arg1]\{arg3\} to the substitution with no - sequential composition *) +(** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential + composition. Most often this is not what you want. For sequential + composition, try [join (map_mbid mp delta) subs] **) val add_mbid : MBId.t -> module_path -> delta_resolver -> substitution -> substitution val add_mp : diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 907ad2a1d4..55e767321b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -81,8 +81,7 @@ open Declarations These fields could be deduced from [revstruct], but they allow faster name freshness checks. - [univ] and [future_cst] : current and future universe constraints - - [engagement] : are we Set-impredicative? - - [type_in_type] : does the universe hierarchy collapse? + - [engagement] : are we Set-impredicative? does the universe hierarchy collapse? - [required] : names and digests of Require'd libraries since big-bang. This field will only grow - [loads] : list of libraries Require'd inside the current module. @@ -122,7 +121,6 @@ type safe_environment = univ : Univ.constraints; future_cst : Univ.constraints Future.computation list; engagement : engagement option; - type_in_type : bool; required : vodigest DPMap.t; loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list; @@ -152,7 +150,6 @@ let empty_environment = future_cst = []; univ = Univ.Constraint.empty; engagement = None; - type_in_type = false; required = DPMap.empty; loads = []; local_retroknowledge = []; diff --git a/lib/envars.ml b/lib/envars.ml index 315d28cebd..bafe2401bb 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -39,25 +39,12 @@ let path_to_list p = let user_path () = path_to_list (Sys.getenv "PATH") (* may raise Not_found *) - (* Duplicated from system.ml to minimize dependencies *) -let file_exists_respecting_case f = - if Coq_config.arch = "Darwin" then - (* ensure that the file exists with expected case on the - case-insensitive but case-preserving default MacOS file system *) - let rec aux f = - let bf = Filename.basename f in - let df = Filename.dirname f in - String.equal df "." || String.equal df "/" || - aux df && Array.exists (String.equal bf) (Sys.readdir df) - in aux f - else Sys.file_exists f - let rec which l f = match l with | [] -> raise Not_found | p :: tl -> - if file_exists_respecting_case (p / f) then + if Sys.file_exists (p / f) then p else which tl f @@ -115,7 +102,7 @@ let _ = If the check fails, then [oth ()] is evaluated. *) let check_file_else ~dir ~file oth = let path = if Coq_config.local then coqroot else coqroot / dir in - if file_exists_respecting_case (path / file) then path else oth () + if Sys.file_exists (path / file) then path else oth () let guess_coqlib fail = let prelude = "theories/Init/Prelude.vo" in @@ -147,7 +134,7 @@ let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in let make_search_path path = let paths = path_to_list path in - let valid_paths = List.filter file_exists_respecting_case paths in + let valid_paths = List.filter Sys.file_exists paths in List.rev valid_paths in make_search_path coqpath diff --git a/lib/system.ml b/lib/system.ml index 26bf780101..e4a60eccb7 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -94,18 +94,6 @@ let all_subdirs ~unix_path:root = else msg_warning (str ("Cannot open " ^ root)); List.rev !l -let file_exists_respecting_case f = - if Coq_config.arch = "Darwin" then - (* ensure that the file exists with expected case on the - case-insensitive but case-preserving default MacOS file system *) - let rec aux f = - let bf = Filename.basename f in - let df = Filename.dirname f in - (String.equal df "." || String.equal df "/" || aux df) - && Array.exists (String.equal bf) (Sys.readdir df) - in aux f - else Sys.file_exists f - let rec search paths test = match paths with | [] -> [] @@ -130,7 +118,7 @@ let where_in_path ?(warn=true) path filename = in check_and_warn (search path (fun lpe -> let f = Filename.concat lpe filename in - if file_exists_respecting_case f then [lpe,f] else [])) + if Sys.file_exists f then [lpe,f] else [])) let where_in_path_rex path rex = search path (fun lpe -> @@ -146,7 +134,7 @@ let where_in_path_rex path rex = let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then - if file_exists_respecting_case filename then + if Sys.file_exists filename then let root = Filename.dirname filename in root, filename else diff --git a/lib/system.mli b/lib/system.mli index eb29b69701..6ed4503266 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -59,8 +59,6 @@ val where_in_path_rex : val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string -val file_exists_respecting_case : string -> bool - (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] diff --git a/library/declare.ml b/library/declare.ml index c3181e4c75..8438380c9c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -28,9 +28,9 @@ open Decl_kinds (** flag for internal message display *) type internal_flag = - | KernelVerbose (* kernel action, a message is displayed *) - | KernelSilent (* kernel action, no message is displayed *) - | UserVerbose (* user action, a message is displayed *) + | UserAutomaticRequest (* kernel action, a message is displayed *) + | InternalTacticRequest (* kernel action, no message is displayed *) + | UserIndividualRequest (* user action, a message is displayed *) (** Declaration of section variables and local definitions *) @@ -253,7 +253,7 @@ let declare_sideff env fix_exn se = if Constant.equal c c' then Some (x,kn) else None) inds_consts) knl)) -let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = let cd = (* We deal with side effects *) match cd with | Entries.DefinitionEntry de -> @@ -283,7 +283,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff let kn = declare_constant_common id cst in kn -let declare_definition ?(internal=UserVerbose) +let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = let cb = diff --git a/library/declare.mli b/library/declare.mli index d8a00db0cf..76538a6248 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -43,9 +43,9 @@ type constant_declaration = constant_entry * logical_kind *) type internal_flag = - | KernelVerbose - | KernelSilent - | UserVerbose + | UserAutomaticRequest + | InternalTacticRequest + | UserIndividualRequest (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> diff --git a/library/library.ml b/library/library.ml index f7ca4e9760..a09f91b15a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,18 +488,8 @@ let rec_intern_library libs mref = let _, libs = intern_library libs mref None in libs -let check_library_short_name f dir = function - | Some id when not (Id.equal id (snd (split_dirpath dir))) -> - errorlabstrm "check_library_short_name" - (str "The file " ++ str f ++ str " contains library" ++ spc () ++ - pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ - pr_id id) - | _ -> () - -let rec_intern_by_filename_only id f = +let rec_intern_by_filename_only f = let m = try intern_from_file f with Sys_error s -> error s in - (* Only the base name is expected to match *) - check_library_short_name f m.library_name id; (* We check no other file containing same library is loaded *) if library_is_loaded m.library_name then begin @@ -518,12 +508,12 @@ let native_name_from_filename f = let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name -let rec_intern_library_from_file idopt f = +let rec_intern_library_from_file f = (* A name is specified, we have to check it contains library id *) let paths = Loadpath.get_paths () in let _, f = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in - rec_intern_by_filename_only idopt f + rec_intern_by_filename_only f (**********************************************************************) (*s [require_library] loads and possibly opens a library. This is a @@ -600,8 +590,8 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library_from_file idopt file export = - let modref,needed = rec_intern_library_from_file idopt file in +let require_library_from_file file export = + let modref,needed = rec_intern_library_from_file file in let needed = List.rev_map snd needed in if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); @@ -678,22 +668,22 @@ let check_module_name s = | c -> err c let start_library f = - let paths = Loadpath.get_paths () in - let _, longf = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let () = if not (Sys.file_exists f) then + errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f)) + in let ldir0 = try - let lp = Loadpath.find_load_path (Filename.dirname longf) in + let lp = Loadpath.find_load_path (Filename.dirname f) in Loadpath.logical lp with Not_found -> Nameops.default_root_prefix in - let file = Filename.basename f in + let file = Filename.chop_extension (Filename.basename f) in let id = Id.of_string file in check_module_name file; check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in Declaremods.start_library ldir; - ldir,longf + ldir let load_library_todo f = let paths = Loadpath.get_paths () in diff --git a/library/library.mli b/library/library.mli index 967a54e4c8..3d96f9a751 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,10 +22,9 @@ open Libnames (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit -val require_library_from_file : - Id.t option -> CUnix.physical_path -> bool option -> unit +val require_library_from_file : CUnix.physical_path -> bool option -> unit -(** {6 ... } *) +(** {6 Start the compilation of a library } *) (** Segments of a library *) type seg_sum @@ -39,10 +38,12 @@ type seg_proofs = Term.constr Future.computation array an export otherwise just a simple import *) val import_module : bool -> qualid located list -> unit -(** {6 Start the compilation of a library } *) -val start_library : string -> DirPath.t * string +(** Start the compilation of a file as a library. The argument must be an + existing file on the system, and the returned path is the associated + absolute logical path of the library. *) +val start_library : CUnix.physical_path -> DirPath.t -(** {6 End the compilation of a library and save it to a ".vo" file } *) +(** End the compilation of a library and save it to a ".vo" file *) val save_library_to : ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit diff --git a/library/nametab.ml b/library/nametab.ml index 6af1e686b0..5b6d7cd982 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -524,7 +524,8 @@ let shortest_qualid_of_tactic kn = let pr_global_env env ref = try str (string_of_qualid (shortest_qualid_of_global env ref)) - with Not_found as e -> prerr_endline "pr_global_env not found"; raise e + with Not_found as e -> + if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e let global_inductive r = match global r with diff --git a/man/coqide.1 b/man/coqide.1 index 3fa7f0e418..cfd9c3b4a2 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -67,11 +67,11 @@ Load Coq file Load Coq object file .IR f .vo. .TP -.BI \-require\ f -Load Coq object file -.IR f .vo -and import it (Require -.IR f .). +.BI \-require\ path +Load Coq library +.IR path +and import it (Require Import +.IR path .). .TP .BI \-compile\ f Compile Coq file diff --git a/man/coqtop.1 b/man/coqtop.1 index 1bc4629d0f..e079bee39b 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -78,13 +78,13 @@ load Coq object file .I filename.vo .TP -.BI \-require \ filename -load Coq object file -.I filename.vo -and import it (Require Import filename.) +.BI \-require \ path +load Coq library +.I path +and import it (Require Import path.) .TP -.BI \-compile \ filename +.BI \-compile \ filename.v compile Coq file .I filename.v (implies @@ -92,7 +92,7 @@ compile Coq file ) .TP -.BI \-compile\-verbose \ filename +.BI \-compile\-verbose \ filename.v verbosely compile Coq file .I filename.v (implies diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 28fb8cbe36..8bd57290b0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -276,6 +276,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with match kind_of_term c with | Case (ci,p,c,cl) when eq_constr c (mkRel (List.index Name.equal na (fst (snd e)))) + && not (Int.equal (Array.length cl) 0) && (* don't contract if p dependent *) computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> let clauses = build_tree na isgoal e ci cl in diff --git a/printing/printer.ml b/printing/printer.ml index 33b95c2f56..18e4902255 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -742,7 +742,8 @@ module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) let pr_assumptionset env s = - if ContextObjectMap.is_empty s then + if ContextObjectMap.is_empty s && + engagement env = (PredicativeSet, StratifiedType) then str "Closed under the global context" else let safe_pr_constant env kn = @@ -788,6 +789,16 @@ let pr_assumptionset env s = let (vars, axioms, opaque, trans) = ContextObjectMap.fold fold s ([], [], [], []) in + let theory = + if is_impredicative_set env then + [str "Set is impredicative"] + else [] + in + let theory = + if type_in_type env then + str "Type hierarchy is collapsed (logic is inconsistent)" :: theory + else theory + in let opt_list title = function | [] -> None | l -> @@ -801,6 +812,7 @@ let pr_assumptionset env s = opt_list (str "Section Variables:") vars; opt_list (str "Axioms:") axioms; opt_list (str "Opaque constants:") opaque; + opt_list (str "Theory:") theory; ] in prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 5e8221b811..fae8716d9d 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -146,12 +146,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in - let ce = Term_typing.handle_entry_side_effects env ce in + let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in let (cb, ctx), se = Future.force ce.const_entry_body in assert(Declareops.side_effects_is_empty se); assert(Univ.ContextSet.is_empty ctx); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 5e0fb4dd36..4aa3c3bfd2 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -153,7 +153,7 @@ val build_constant_by_tactic : types -> unit Proofview.tactic -> Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> +val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context diff --git a/proofs/proof.ml b/proofs/proof.ml index a7077d9110..c7aa5bad97 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -173,6 +173,12 @@ let is_done p = (* spiwack: for compatibility with <= 8.2 proof engine *) let has_unresolved_evar p = Proofview.V82.has_unresolved_evar p.proofview +let has_shelved_goals p = not (CList.is_empty (p.shelf)) +let has_given_up_goals p = not (CList.is_empty (p.given_up)) + +let is_complete p = + is_done p && not (has_unresolved_evar p) && + not (has_shelved_goals p) && not (has_given_up_goals p) (* Returns the list of partial proofs to initial goals *) let partial_proof p = Proofview.partial_proof p.entry p.proofview @@ -305,9 +311,9 @@ end let return p = if not (is_done p) then raise UnfinishedProof - else if not (CList.is_empty (p.shelf)) then + else if has_shelved_goals p then raise HasShelvedGoals - else if not (CList.is_empty (p.given_up)) then + else if has_given_up_goals p then raise HasGivenUpGoals else if has_unresolved_evar p then (* spiwack: for compatibility with <= 8.3 proof engine *) diff --git a/proofs/proof.mli b/proofs/proof.mli index a2e10d8133..a0ed0654db 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -75,6 +75,9 @@ val initial_euctx : proof -> Evd.evar_universe_context to be considered (this does not require that all evars have been solved). *) val is_done : proof -> bool +(* Like is_done, but this time it really means done (i.e. nothing left to do) *) +val is_complete : proof -> bool + (* Returns the list of partial proofs to initial goals. *) val partial_proof : proof -> Term.constr list diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 10e7b758da..21009d1204 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -344,7 +344,7 @@ type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.ev let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in if allow_partial then begin - if Proof.is_done proof then begin + if Proof.is_complete proof then begin msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++ str" is complete, no need to end it with Admitted"); end; diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index e1c9c2de59..e6a8cbe3ad 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -21,7 +21,7 @@ open Ind_tables (* Induction/recursion schemes *) -let optimize_non_type_induction_scheme kind dep sort ind = +let optimize_non_type_induction_scheme kind dep sort _ ind = let env = Global.env () in let sigma = Evd.from_env env in if check_scheme kind ind then @@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" @@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 8643fe10f0..f7d3ad5d0a 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -191,7 +191,7 @@ let build_sym_scheme env ind = let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" - (fun ind -> + (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in (c, ctx), Declareops.no_seff) @@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind = let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" - (fun ind -> + (fun _ ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind) (**********************************************************************) @@ -650,7 +650,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme (**********************************************************************) let rew_l2r_dep_scheme_kind = declare_individual_scheme_object "_rew_r_dep" - (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType) + (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType) (**********************************************************************) (* Dependent rewrite from right-to-left in conclusion *) @@ -660,7 +660,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +670,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +680,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -693,7 +693,7 @@ let rew_l2r_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" - (fun ind -> fix_r2l_forward_rew_scheme + (fun _ ind -> fix_r2l_forward_rew_scheme (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) (**********************************************************************) @@ -704,7 +704,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) (* End of rewriting schemes *) @@ -780,6 +780,6 @@ let build_congr env (eq,refl,ctx) ind = in c, Evd.evar_universe_context_of ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" - (fun ind -> + (fun _ ind -> (* May fail if equality is not defined *) build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e4240cb5cc..af0870bc92 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -320,7 +320,7 @@ let project_hint pri l2r r = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in let ctx = Evd.universe_context_set sigma in - let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in + let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) let add_hints_iff l2r lc n bl = diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index aa057a3e86..c64a1226ab 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1542,7 +1542,7 @@ let newfail n s = let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = let open Proofview.Notations in - let treat sigma (res, is_hyp) = + let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") | Some None -> Proofview.tclUNIT () @@ -1550,7 +1550,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in let gls = List.rev (Evd.fold_undefined fold undef []) in - match is_hyp, prf with + match clause, prf with | Some id, Some p -> let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in Proofview.Unsafe.tclEVARS undef <*> @@ -1582,17 +1582,25 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let ty, is_hyp = - match clause with - | Some id -> Environ.named_type id env, Some id - | None -> concl, None + let ty = match clause with + | None -> concl + | Some id -> Environ.named_type id env + in + let env = match clause with + | None -> env + | Some id -> + (** Only consider variables not depending on [id] *) + let ctx = Environ.named_context env in + let filter decl = not (occur_var_in_decl env id decl) in + let nctx = List.filter filter ctx in + Environ.reset_with_named_context (Environ.val_of_named_context nctx) env in try let res = - cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp + cl_rewrite_clause_aux ?abs strat env [] sigma ty clause in let sigma = match origsigma with None -> sigma | Some sigma -> sigma in - treat sigma (res, is_hyp) <*> + treat sigma res <*> (** For compatibility *) beta <*> opt_beta <*> Proofview.shelve_unifiable with @@ -1888,7 +1896,7 @@ let add_morphism_infer glob m n = let instance = build_morphism_signature m in let evd = Evd.empty (*FIXME *) in if Lib.is_modtype () then - let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry (None,poly,(instance,Univ.UContext.empty),None), Decl_kinds.IsAssumption Decl_kinds.Logical) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index fea7ab72e4..b5dc2dc8be 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4510,7 +4510,7 @@ let abstract_subproof id gk tac = let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in (** ppedrot: seems legit to have abstracted subproofs as local*) - let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in diff --git a/test-suite/Makefile b/test-suite/Makefile index d2466250ab..39c36d5414 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -208,7 +208,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$*" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be prepared" ; \ @@ -238,7 +238,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$*" $(call get_coq_prog_args,"$<") -async-proofs on \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ -async-proofs-private-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \ $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ @@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v # Additionnal dependencies for module tests $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo modules/%.vo: modules/%.v - $(HIDE)$(coqtop) -R modules Mods -compile $(<:.v=) + $(HIDE)$(coqtop) -R modules Mods -compile $< ####################################################################### # Miscellaneous tests diff --git a/test-suite/bugs/closed/3948.v b/test-suite/bugs/closed/3948.v new file mode 100644 index 0000000000..56b1e3ffb4 --- /dev/null +++ b/test-suite/bugs/closed/3948.v @@ -0,0 +1,24 @@ +Module Type S. +Parameter t : Type. +End S. + +Module Bar(X : S). +Definition elt := X.t. +Axiom fold : elt. +End Bar. + +Module Make (Z: S) := Bar(Z). + +Declare Module Y : S. + +Module Type Interface. +Parameter constant : unit. +End Interface. + +Module DepMap : Interface. +Module Dom := Make(Y). +Definition constant : unit := + let _ := @Dom.fold in tt. +End DepMap. + +Print Assumptions DepMap.constant. diff --git a/tools/coqc.ml b/tools/coqc.ml index 5710b97f2a..e7239da682 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -30,13 +30,8 @@ let verbose = ref false let rec make_compilation_args = function | [] -> [] | file :: fl -> - let file_noext = - if Filename.check_suffix file ".v" then - Filename.chop_suffix file ".v" - else file - in (if !verbose then "-compile-verbose" else "-compile") - :: file_noext :: (make_compilation_args fl) + :: file :: (make_compilation_args fl) (* compilation of files [files] with command [command] and args [args] *) diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 4d8ba0f789..a6bd968efc 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -55,7 +55,7 @@ let rec fields_of_functor f subs mp0 args = function match args with | [] -> assert false (* we should only encounter applied functors *) | mpa :: args -> - let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in + let subs = join (map_mbid mbid mpa empty_delta_resolver (*TODO*)) subs in fields_of_functor f subs mp0 args e let rec lookup_module_in_impl mp = @@ -64,11 +64,11 @@ let rec lookup_module_in_impl mp = (* The module we search might not be exported by its englobing module(s). We access the upper layer, and then do a manual search *) match mp with - | MPfile _ | MPbound _ -> - raise Not_found (* should have been found by [lookup_module] *) - | MPdot (mp',lab') -> - let fields = memoize_fields_of_mp mp' in - search_mod_label lab' fields + | MPfile _ -> raise Not_found (* can happen if mp is an open module *) + | MPbound _ -> assert false + | MPdot (mp',lab') -> + let fields = memoize_fields_of_mp mp' in + search_mod_label lab' fields and memoize_fields_of_mp mp = try MPmap.find mp !modcache diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index d1452fca21..4122487e23 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -111,7 +111,7 @@ let check_bool_is_defined () = let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let build_beq_scheme kn = +let build_beq_scheme mode kn = check_bool_is_defined (); (* fetching global env *) let env = Global.env() in @@ -188,7 +188,7 @@ let build_beq_scheme kn = else begin try let eq, eff = - let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in + let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in mkConst c, eff in let eqa, eff = let eqa, effs = List.split (List.map aux a) in @@ -330,7 +330,7 @@ let destruct_ind c = so from Ai we can find the the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) -let do_replace_lb lb_scheme_key aavoid narg p q = +let do_replace_lb mode lb_scheme_key aavoid narg p q = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -360,7 +360,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = let u,v = destruct_ind type_of_pq in let lb_type_of_p = try - let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in + let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in Proofview.tclUNIT (mkConst c, eff) with Not_found -> (* spiwack: the format of this error message should probably @@ -388,7 +388,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = end (* used in the bool -> leib side *) -let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = +let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -551,7 +551,7 @@ let compute_bl_goal ind lnamesparrec nparrec = (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) ))), eff -let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec = +let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -608,7 +608,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). if eq_gr (IndRef indeq) Coqlib.glob_eq then Tacticals.New.tclTHEN - (do_replace_bl bl_scheme_key ind + (do_replace_bl mode bl_scheme_key ind (!avoid) nparrec (ca.(2)) (ca.(1))) @@ -625,7 +625,12 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let make_bl_scheme mind = +let side_effect_of_mode = function + | Declare.UserAutomaticRequest -> false + | Declare.InternalTacticRequest -> true + | Declare.UserIndividualRequest -> false + +let make_bl_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -637,8 +642,9 @@ let make_bl_scheme mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal - (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal + (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -688,7 +694,7 @@ let compute_lb_goal ind lnamesparrec nparrec = (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) ))), eff -let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = +let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -732,7 +738,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = | App(c,ca) -> (match (kind_of_term ca.(1)) with | App(c',ca') -> let n = Array.length ca' in - do_replace_lb lb_scheme_key + do_replace_lb mode lb_scheme_key (!avoid) nparrec ca'.(n-2) ca'.(n-1) @@ -747,7 +753,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") -let make_lb_scheme mind = +let make_lb_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -759,8 +765,9 @@ let make_lb_scheme mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal - (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal + (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx (* FIXME *)), eff @@ -919,7 +926,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ] end -let make_eq_decidability mind = +let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then raise DecidabilityMutualNotSupported; @@ -930,7 +937,8 @@ let make_eq_decidability mind = let ctx = Evd.empty_evar_universe_context (* FIXME *)in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 33891ad94c..7fe79d948b 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -186,7 +186,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in Evarutil.check_evars env Evd.empty !evars termtype; let ctx = Evd.universe_context !evars in - let cst = Declare.declare_constant ~internal:Declare.KernelSilent id + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (Entries.ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in instance_hook k None global imps ?hook (ConstRef cst); id @@ -363,7 +363,7 @@ let context poly l = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then let uctx = Univ.ContextSet.to_context uctx in let decl = (ParameterEntry (None,poly,(t,uctx),None), IsAssumption Logical) in - let cst = Declare.declare_constant ~internal:Declare.KernelSilent id decl in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr t with | Some (rels, ((tc,_), args) as _cl) -> add_instance (Typeclasses.new_instance tc None false (*FIXME*) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 3c87533a93..4010806a7c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -171,7 +171,7 @@ let load_vernacular () = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj let load_vernac_obj () = - List.iter (fun f -> Library.require_library_from_file None f None) + List.iter (fun f -> Library.require_library_from_file f None) (List.rev !load_vernacular_obj) let require_prelude () = @@ -185,9 +185,9 @@ let require_prelude () = let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = - if !load_init then silently require_prelude (); - List.iter (fun s -> Library.require_library_from_file None s (Some false)) - (List.rev !require_list) + let () = if !load_init then silently require_prelude () in + let map dir = Qualid (Loc.ghost, qualid_of_string dir) in + Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list) let compile_list = ref ([] : (bool * string) list) diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 0d39466ede..218c47b28d 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -28,11 +28,10 @@ open Pp (**********************************************************************) (* Registering schemes in the environment *) - type mutual_scheme_object_function = - mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects type 'a scheme_kind = string @@ -114,8 +113,8 @@ let is_visible_name id = let compute_name internal id = match internal with - | KernelVerbose | UserVerbose -> id - | KernelSilent -> + | UserAutomaticRequest | UserIndividualRequest -> id + | InternalTacticRequest -> Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name let define internal id c p univs = @@ -136,37 +135,36 @@ let define internal id c p univs = } in let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in let () = match internal with - | KernelSilent -> () + | InternalTacticRequest -> () | _-> definition_message id in kn -let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = - let (c, ctx), eff = f ind in +let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = + let (c, ctx), eff = f mode ind in let mib = Global.lookup_mind mind in let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define internal id c mib.mind_polymorphic ctx in + let const = define mode id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; const, Declareops.cons_side_effects (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff -let define_individual_scheme kind internal names (mind,i as ind) = +let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with | _,MutualSchemeFunction f -> assert false | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f internal names ind + define_individual_scheme_base kind s f mode names ind -let define_mutual_scheme_base kind suff f internal names mind = - let (cl, ctx), eff = f mind in +let define_mutual_scheme_base kind suff f mode names mind = + let (cl, ctx), eff = f mode mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in - let consts = Array.map2 (fun id cl -> - define internal id cl mib.mind_polymorphic ctx) ids cl in + define mode id cl mib.mind_polymorphic ctx) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, @@ -175,11 +173,11 @@ let define_mutual_scheme_base kind suff f internal names mind = kind (Global.safe_env()) (Array.to_list schemes)) eff -let define_mutual_scheme kind internal names mind = +let define_mutual_scheme kind mode names mind = match Hashtbl.find scheme_object_table kind with | _,IndividualSchemeFunction _ -> assert false | s,MutualSchemeFunction f -> - define_mutual_scheme_base kind s f internal names mind + define_mutual_scheme_base kind s f mode names mind let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in @@ -188,14 +186,14 @@ let find_scheme_on_env_too kind ind = kind (Global.safe_env()) [ind, s]) Declareops.no_seff -let find_scheme kind (mind,i as ind) = +let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = try find_scheme_on_env_too kind ind with Not_found -> match Hashtbl.find scheme_object_table kind with | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f KernelSilent None ind + define_individual_scheme_base kind s f mode None ind | s,MutualSchemeFunction f -> - let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in + let ca, eff = define_mutual_scheme_base kind s f mode [] mind in ca.(i), eff let check_scheme kind ind = diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 98eaac0928..d0844dd946 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -8,6 +8,7 @@ open Term open Names +open Declare (** This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand *) @@ -19,9 +20,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects (** Main functions to register a scheme builder *) @@ -32,21 +33,17 @@ val declare_individual_scheme_object : string -> ?aux:string -> individual_scheme_object_function -> individual scheme_kind -(* -val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit -*) - (** Force generation of a (mutually) scheme with possibly user-level names *) val define_individual_scheme : individual scheme_kind -> - Declare.internal_flag (** internal *) -> + internal_flag (** internal *) -> Id.t option -> inductive -> constant * Declareops.side_effects -val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) -> +val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 286d164c42..452d5fbe50 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -146,8 +146,8 @@ let declare_beq_scheme_gen internal names kn = let alarm what internal msg = let debug = false in match internal with - | KernelVerbose - | KernelSilent -> + | UserAutomaticRequest + | InternalTacticRequest -> (if debug then msg_warning (hov 0 msg ++ fnl () ++ what ++ str " not defined.")) @@ -195,13 +195,13 @@ let beq_scheme_msg mind = (List.init (Array.length mib.mind_packets) (fun i -> (mind,i))) let declare_beq_scheme_with l kn = - try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn + try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserIndividualRequest l kn let try_declare_beq_scheme kn = (* TODO: handle Fix, eventually handle proof-irrelevance; improve decidability by depending on decidability for the parameters rather than on the bl and lb properties *) - try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn + try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserAutomaticRequest [] kn let declare_beq_scheme = declare_beq_scheme_with [] @@ -215,7 +215,7 @@ let declare_one_case_analysis_scheme ind = induction scheme, the other ones share the same code with the apropriate type *) if Sorts.List.mem InType kelim then - ignore (define_individual_scheme dep KernelVerbose None ind) + ignore (define_individual_scheme dep UserAutomaticRequest None ind) (* Induction/recursion schemes *) @@ -238,7 +238,7 @@ let declare_one_induction_scheme ind = List.map_filter (fun (sort,kind) -> if Sorts.List.mem sort kelim then Some kind else None) (if from_prop then kinds_from_prop else kinds_from_type) in - List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind)) + List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind)) elims let declare_induction_schemes kn = @@ -261,11 +261,11 @@ let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *) let declare_eq_decidability_scheme_with l kn = try_declare_scheme (eq_dec_scheme_msg (kn,0)) - declare_eq_decidability_gen UserVerbose l kn + declare_eq_decidability_gen UserIndividualRequest l kn let try_declare_eq_decidability kn = try_declare_scheme (eq_dec_scheme_msg (kn,0)) - declare_eq_decidability_gen KernelVerbose [] kn + declare_eq_decidability_gen UserAutomaticRequest [] kn let declare_eq_decidability = declare_eq_decidability_scheme_with [] @@ -274,17 +274,17 @@ let ignore_error f x = let declare_rewriting_schemes ind = if Hipattern.is_inductive_equality ind then begin - ignore (define_individual_scheme rew_r2l_scheme_kind KernelVerbose None ind); - ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelVerbose None ind); + ignore (define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind); + ignore (define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind); ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind - KernelVerbose None ind); + UserAutomaticRequest None ind); (* These ones expect the equality to be symmetric; the first one also *) (* needs eq *) - ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelVerbose None) ind; + ignore_error (define_individual_scheme rew_l2r_scheme_kind UserAutomaticRequest None) ind; ignore_error - (define_individual_scheme rew_l2r_dep_scheme_kind KernelVerbose None) ind; + (define_individual_scheme rew_l2r_dep_scheme_kind UserAutomaticRequest None) ind; ignore_error - (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelVerbose None) ind + (define_individual_scheme rew_l2r_forward_dep_scheme_kind UserAutomaticRequest None) ind end let declare_congr_scheme ind = @@ -293,7 +293,7 @@ let declare_congr_scheme ind = try Coqlib.check_required_library Coqlib.logic_module_name; true with e when Errors.noncritical e -> false then - ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind) + ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind) else msg_warning (strbrk "Cannot build congruence scheme because eq is not found") end @@ -301,7 +301,7 @@ let declare_congr_scheme ind = let declare_sym_scheme ind = if Hipattern.is_inductive_equality ind then (* Expect the equality to be symmetric *) - ignore_error (define_individual_scheme sym_scheme_kind KernelVerbose None) ind + ignore_error (define_individual_scheme sym_scheme_kind UserAutomaticRequest None) ind (* Scheme command *) @@ -372,7 +372,7 @@ let do_mutual_induction_scheme lnamedepindsort = let decltype = Retyping.get_type_of env0 sigma decl in (* let decltype = refresh_universes decltype in *) let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in - let cst = define fi UserVerbose sigma proof_output (Some decltype) in + let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in @@ -470,7 +470,7 @@ let do_combined_scheme name schemes = in let body,typ = build_combined_scheme (Global.env ()) csts in let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in - ignore (define (snd name) UserVerbose Evd.empty proof_output (Some typ)); + ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ)); fixpoint_message None [snd name] (**********************************************************************) diff --git a/toplevel/record.ml b/toplevel/record.ml index 484fd081df..e214f9ca71 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -298,7 +298,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field const_entry_inline_code = false; const_entry_feedback = None } in let k = (DefinitionEntry entry,IsDefinition kind) in - let kn = declare_constant ~internal:KernelSilent fid k in + let kn = declare_constant ~internal:InternalTacticRequest fid k in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in applist (mkConstU (kn,u),proj_args) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 1144ffb940..2921364069 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -42,9 +42,9 @@ let print_usage_channel co command = \n -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.)\ \n -lv f (idem)\ \n -load-vernac-object f load Coq object file f.vo\ -\n -require f load Coq object file f.vo and import it (Require f.)\ -\n -compile f compile Coq file f.v (implies -batch)\ -\n -compile-verbose f verbosely compile Coq file f.v (implies -batch)\ +\n -require path load Coq library path and import it (Require Import path.)\ +\n -compile f.v compile Coq file f.v (implies -batch)\ +\n -compile-verbose f.v verbosely compile Coq file f.v (implies -batch)\ \n -quick quickly compile .v files to .vio files (skip proofs)\ \n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ \n into fi.vo\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 266d8f9b4f..14d2bcea41 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -294,7 +294,15 @@ let load_vernac verb file = if !Flags.beautify_file then close_out !chan_beautify; raise_with_file file (disable_drop e, info) -(* Compile a vernac file (f is assumed without .v suffix) *) +let ensure_v f = + if Filename.check_suffix f ".v" then f + else begin + msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \ + expanded to \"" ++ str f ++ str ".v\""); + f ^ ".v" + end + +(* Compile a vernac file *) let compile verbosely f = let check_pending_proofs () = let pfs = Pfedit.get_all_proof_names () in @@ -302,7 +310,8 @@ let compile verbosely f = (msg_error (str "There are pending proofs"); flush_all (); exit 1) in match !Flags.compilation_mode with | BuildVo -> - let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in + let long_f_dot_v = ensure_v f in + let ldir = Flags.verbosely Library.start_library long_f_dot_v in Stm.set_compilation_hints long_f_dot_v; Aux_file.start_aux_file_for long_f_dot_v; Dumpglob.start_dump_glob long_f_dot_v; @@ -318,7 +327,8 @@ let compile verbosely f = Aux_file.stop_aux_file (); Dumpglob.end_dump_glob () | BuildVio -> - let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in + let long_f_dot_v = ensure_v f in + let ldir = Flags.verbosely Library.start_library long_f_dot_v in Dumpglob.noglob (); Stm.set_compilation_hints long_f_dot_v; let _ = load_vernac verbosely long_f_dot_v in diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 4b1cd7a013..c6d87596dc 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -16,6 +16,9 @@ val show_prooftree : unit -> unit val show_node : unit -> unit +val vernac_require : + Libnames.reference option -> bool option -> Libnames.reference list -> unit + (** This function can be used by any command that want to observe terms in the context of the current goal *) val get_current_context_of_args : int option -> Evd.evar_map * Environ.env |