From 1eb1083a4e135fba5a69c48af55333453a6a17df Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 9 Feb 2015 19:04:37 +0100 Subject: STM: is Flags.async_proofs_full then always delegate Probably a regression introduced in some code refactoring. Affects only PIDE based code. --- stm/stm.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/stm/stm.ml b/stm/stm.ml index 96a11d306d..693c673b40 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1554,6 +1554,7 @@ let async_policy () = let delegate name = let time = get_hint_bp_time name in time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio + || !Flags.async_proofs_full let collect_proof keep cur hd brkind id = prerr_endline ("Collecting proof ending at "^Stateid.to_string id); -- cgit v1.2.3 From 4261cc40270ee8abfa8ced859a8fb0b209cc78a8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 11 Feb 2015 17:59:50 +0100 Subject: Win: use .exe extension for the ocaml compiler (Close 3572) --- configure.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 559e7ea1a7..0c1d39127f 100644 --- a/configure.ml +++ b/configure.ml @@ -77,7 +77,12 @@ let read_lines_and_close fd = type err = StdErr | StdOut | DevNull +let exe = ref "" (* Will be set later on, when the suffix is known *) + let run ?(fatal=true) ?(err=StdErr) prog args = + let prog = (* Ensure prog ends with exe *) + if Str.string_match (Str.regexp ("^.*" ^ !exe ^ "$")) prog 0 + then prog else (prog ^ !exe) in let argv = Array.of_list (prog::args) in try let out_r,out_w = Unix.pipe () in @@ -431,7 +436,7 @@ let arch = match !Prefs.arch with let arch_win32 = (arch = "win32") -let exe = if arch_win32 then ".exe" else "" +let exe = exe := if arch_win32 then ".exe" else ""; !exe let dll = if os_type_win32 then ".dll" else ".so" (** * VCS -- cgit v1.2.3 From 34c7ef490d26e67ad1545dba65db7080744ffbe0 Mon Sep 17 00:00:00 2001 From: Matěj Grabovský Date: Wed, 11 Feb 2015 10:04:20 +0100 Subject: Missing space in error message --- tactics/tactics.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9265328a47..a298bba978 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -425,7 +425,7 @@ let pf_reduce_decl redfun where (id,c,ty) gl = match c with | None -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str "has no value."); + errorlabstrm "" (pr_id id ++ str " has no value."); (id,None,redfun' ty) | Some b -> let b' = if where != InHypTypeOnly then redfun' b else b in @@ -522,7 +522,7 @@ let pf_e_reduce_decl redfun where (id,c,ty) gl = match c with | None -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str "has no value."); + errorlabstrm "" (pr_id id ++ str " has no value."); let sigma, ty' = redfun sigma ty in sigma, (id,None,ty') | Some b -> @@ -565,7 +565,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env match c with | None -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str "has no value."); + errorlabstrm "" (pr_id id ++ str " has no value."); let sigma',ty' = redfun false env sigma ty in sigma', (id,None,ty') | Some b -> -- cgit v1.2.3 From b8efac9f2cadbc0f700408fcb6f8187ef6527fd9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 Feb 2015 20:04:29 +0100 Subject: Adding test for bug #3786. --- test-suite/bugs/closed/3786.v | 32 ++++++++++++++++++++++++++++++++ test-suite/bugs/opened/3786.v | 40 ---------------------------------------- 2 files changed, 32 insertions(+), 40 deletions(-) create mode 100644 test-suite/bugs/closed/3786.v delete mode 100644 test-suite/bugs/opened/3786.v diff --git a/test-suite/bugs/closed/3786.v b/test-suite/bugs/closed/3786.v new file mode 100644 index 0000000000..fd3bd7bd76 --- /dev/null +++ b/test-suite/bugs/closed/3786.v @@ -0,0 +1,32 @@ +Require Coq.Lists.List. +Require Coq.Sets.Ensembles. +Import Coq.Sets.Ensembles. +Global Set Implicit Arguments. +Delimit Scope comp_scope with comp. +Inductive Comp : Type -> Type := +| Return : forall A, A -> Comp A +| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B +| Pick : forall A, Ensemble A -> Comp A. +Notation ret := Return. +Notation "x <- y ; z" := (Bind y%comp (fun x => z%comp)) + (at level 81, right associativity, + format "'[v' x <- y ; '/' z ']'") : comp_scope. +Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop. +Open Scope comp. +Axiom elements : forall {A} (ls : list A), Ensemble A. +Axiom to_list : forall {A} (S : Ensemble A), Comp (list A). +Axiom finite_set_handle_cardinal : refine (ret 0) (ret 0). +Definition sumUniqueSpec (ls : list nat) : Comp nat. + exact (ls' <- to_list (elements ls); + List.fold_right (fun a b' => Bind b' ((fun a b => ret (a + b)) a)) (ret 0) ls'). +Defined. +Axiom admit : forall {T}, T. +Definition sumUniqueImpl (ls : list nat) +: { c : _ | refine (sumUniqueSpec ls) (ret c) }%type. +Proof. + eexists. + match goal with + | [ |- refine ?a ?b ] => let a' := eval hnf in a in change (refine a' b) + end. + try setoid_rewrite (@finite_set_handle_cardinal). +Abort. diff --git a/test-suite/bugs/opened/3786.v b/test-suite/bugs/opened/3786.v deleted file mode 100644 index 5a1241151c..0000000000 --- a/test-suite/bugs/opened/3786.v +++ /dev/null @@ -1,40 +0,0 @@ -Require Coq.Lists.List. -Require Coq.Sets.Ensembles. -Import Coq.Sets.Ensembles. -Global Set Implicit Arguments. -Delimit Scope comp_scope with comp. -Inductive Comp : Type -> Type := -| Return : forall A, A -> Comp A -| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B -| Pick : forall A, Ensemble A -> Comp A. -Notation ret := Return. -Notation "x <- y ; z" := (Bind y%comp (fun x => z%comp)) - (at level 81, right associativity, - format "'[v' x <- y ; '/' z ']'") : comp_scope. -Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop. -Open Scope comp. -Axiom elements : forall {A} (ls : list A), Ensemble A. -Axiom to_list : forall {A} (S : Ensemble A), Comp (list A). -Axiom finite_set_handle_cardinal : refine (ret 0) (ret 0). -Definition sumUniqueSpec (ls : list nat) : Comp nat. - exact (ls' <- to_list (elements ls); - List.fold_right (fun a b' => Bind b' ((fun a b => ret (a + b)) a)) (ret 0) ls'). -Defined. -Axiom admit : forall {T}, T. -Definition sumUniqueImpl (ls : list nat) -: { c : _ | refine (sumUniqueSpec ls) (ret c) }%type. -Proof. - eexists. - match goal with - | [ |- refine ?a ?b ] => let a' := eval hnf in a in refine (_ : refine a' b) - end; - try setoid_rewrite (@finite_set_handle_cardinal). - Undo. - match goal with - | [ |- refine ?a ?b ] => let a' := eval hnf in a in change (refine a' b) - end. - try setoid_rewrite (@finite_set_handle_cardinal). (* Anomaly: Uncaught exception Invalid_argument("decomp_pointwise"). -Please report. *) - instantiate (1 := admit). - admit. -Defined. -- cgit v1.2.3 From e2dca0d78482e9d1e067e4d0ff847a2b65867498 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 12 Feb 2015 07:29:52 +0100 Subject: Make clearer that "Remove Printing Let" does not influence destructuring let. --- doc/refman/RefMan-ext.tex | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 1eb40cd36d..71eb0108d3 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -560,8 +560,7 @@ The default is to not print synthesizable types. \comindex{Print Table Printing Let}} If an inductive type has just one constructor, -pattern-matching can be written using {\tt let} ... {\tt :=} -... {\tt in}~... +pattern-matching can be written using the first destructuring let syntax. \begin{quote} {\tt Add Printing Let {\ident}.} @@ -572,7 +571,10 @@ pattern-matching is written using a {\tt let} expression. \begin{quote} {\tt Remove Printing Let {\ident}.} \end{quote} -This removes {\ident} from this list. +This removes {\ident} from this list. Note that removing an inductive +type from this list has an impact only for pattern-matching written using +\texttt{match}. Pattern-matching explicitly written using a destructuring +let are not impacted. \begin{quote} {\tt Test Printing Let for {\ident}.} @@ -630,13 +632,19 @@ it is sensible to the command {\tt Reset}. This example emphasizes what the printing options offer. \begin{coq_example} +Definition snd (A B:Set) (H:A * B) := match H with + | pair x y => y + end. Test Printing Let for prod. -Print fst. +Print snd. Remove Printing Let prod. Unset Printing Synth. Unset Printing Wildcard. -Print fst. +Print snd. \end{coq_example} +\begin{coq_eval} +Reset Initial. +\end{coq_eval} % \subsection{Still not dead old notations} -- cgit v1.2.3 From c13476e65f9aa909d7fe8f0504ddc5f68e49b1f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Feb 2015 15:25:34 +0100 Subject: Tentative fix for bug #4027. --- tactics/taccoerce.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 215713d981..74e2341bd9 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -176,6 +176,12 @@ let coerce_to_evaluable_ref env v = let id = out_gen (topwit wit_var) v in if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () + else if has_type v (topwit wit_ref) then + let r = out_gen (topwit wit_ref) v in + match r with + | VarRef var -> EvalVarRef var + | ConstRef c -> EvalConstRef c + | IndRef _ | ConstructRef _ -> fail () else let ev = match Value.to_constr v with | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c)) -- cgit v1.2.3 From 1e5a7ded7b5ca5b2cca548f9a80ff8fd805e6ba1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Feb 2015 15:56:49 +0100 Subject: Fixing compilation for 3.12. --- tactics/taccoerce.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 74e2341bd9..ab71f5f2e7 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -177,6 +177,7 @@ let coerce_to_evaluable_ref env v = if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () else if has_type v (topwit wit_ref) then + let open Globnames in let r = out_gen (topwit wit_ref) v in match r with | VarRef var -> EvalVarRef var -- cgit v1.2.3 From cf4645acc78a8463fa533756efd9a8d9855d727d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Feb 2015 16:09:01 +0100 Subject: Fixing bug #4023. --- ide/coqide.ml | 5 +++-- ide/preferences.ml | 5 +---- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index fa64defabd..78fcbaf8cf 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -838,6 +838,9 @@ let refresh_editor_prefs () = sn.command#refresh_font (); (* Colors *) + Tags.set_processing_color (Tags.color_of_string current.processing_color); + Tags.set_processed_color (Tags.color_of_string current.processed_color); + Tags.set_error_color (Tags.color_of_string current.error_color); sn.script#misc#modify_base [`NORMAL, `COLOR clr]; sn.proof#misc#modify_base [`NORMAL, `COLOR clr]; sn.messages#misc#modify_base [`NORMAL, `COLOR clr]; @@ -1314,8 +1317,6 @@ let build_ui () = refresh_tabs_hook := refresh_notebook_pos; (* Color configuration *) - Tags.set_processing_color (Tags.color_of_string prefs.processing_color); - Tags.set_processed_color (Tags.color_of_string prefs.processed_color); Tags.Script.incomplete#set_property (`BACKGROUND_STIPPLE (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); diff --git a/ide/preferences.ml b/ide/preferences.ml index c850613253..25712f951b 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -503,10 +503,7 @@ let configure ?(apply=(fun () -> ())) () = current.processing_color <- Tags.string_of_color processing_button#color; current.processed_color <- Tags.string_of_color processed_button#color; current.error_color <- Tags.string_of_color error_button#color; - !refresh_editor_hook (); - Tags.set_processing_color processing_button#color; - Tags.set_processed_color processed_button#color; - Tags.set_error_color error_button#color + !refresh_editor_hook () in custom ~label box callback true in -- cgit v1.2.3 From 7f427a8ab2e08e24c303cffd2e54d4fb477f3b00 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 12 Feb 2015 15:40:10 +0100 Subject: Fixing #3997 (occur-check in the presence of primitive projections, patch from Matthieu). --- pretyping/evarsolve.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 5aa72c90ac..921609aae3 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -186,6 +186,7 @@ let noccur_evar env evd evk c = (match pi2 (Environ.lookup_rel (i-k) env) with | None -> () | Some b -> occur_rec k (lift i b)) + | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c []) | _ -> iter_constr_with_binders succ occur_rec k c in try occur_rec 0 c; true with Occur -> false -- cgit v1.2.3 From e03513b7309008a45957609739bcdaf3789f3052 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 12 Feb 2015 15:49:08 +0100 Subject: Fixing #3982 (conflict with max notation for universes). --- parsing/g_constr.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 8246df283b..3bb029a888 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -157,7 +157,7 @@ GEXTEND Gram ] ] ; universe: - [ [ "max("; ids = LIST1 ident SEP ","; ")" -> ids + [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids | id = ident -> [id] ] ] ; -- cgit v1.2.3 From 5268efdefb396267bfda0c17eb045fa2ed516b3c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 31 Jan 2015 09:09:28 +0100 Subject: Using same code for browsing physical directories in coqtop and coqdep. In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error). --- Makefile.build | 1 + Makefile.common | 2 +- checker/check.mllib | 2 ++ checker/checker.ml | 1 + dev/printers.mllib | 1 + lib/lib.mllib | 1 + lib/system.ml | 48 ++++++++++---------------------- lib/system.mli | 4 --- lib/systemdirs.ml | 70 +++++++++++++++++++++++++++++++++++++++++++++++ lib/systemdirs.mli | 41 +++++++++++++++++++++++++++ tools/coqdep.ml | 3 +- tools/coqdep_common.ml | 73 ++++++++++++++++++++++--------------------------- tools/coqdep_common.mli | 9 +++--- toplevel/coqtop.ml | 2 +- toplevel/mltop.ml | 3 +- 15 files changed, 174 insertions(+), 87 deletions(-) create mode 100644 lib/systemdirs.ml create mode 100644 lib/systemdirs.mli diff --git a/Makefile.build b/Makefile.build index 0d87d98e96..6c3834ae43 100644 --- a/Makefile.build +++ b/Makefile.build @@ -606,6 +606,7 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) # coqdep_boot. COQDEPBOOTSRC:= \ + lib/systemdirs.mli lib/systemdirs.ml \ tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ tools/coqdep_common.mli tools/coqdep_common.ml \ tools/coqdep_boot.ml diff --git a/Makefile.common b/Makefile.common index d752a5be91..f83d8b88c6 100644 --- a/Makefile.common +++ b/Makefile.common @@ -232,7 +232,7 @@ IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc -COQENVCMO:=lib/clib.cma lib/errors.cmo +COQENVCMO:=lib/clib.cma lib/errors.cmo lib/systemdirs.cmo COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo diff --git a/checker/check.mllib b/checker/check.mllib index 22df375623..8381144e89 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -33,6 +33,8 @@ Util Ephemeron Future CUnix + +Systemdirs System Profile RemoteCounter diff --git a/checker/checker.ml b/checker/checker.ml index ffe1553197..360f996499 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -10,6 +10,7 @@ open Pp open Errors open Util open System +open Systemdirs open Flags open Names open Check diff --git a/dev/printers.mllib b/dev/printers.mllib index 2f78c2e915..7f8d4aad16 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -37,6 +37,7 @@ Util Bigint Dyn CUnix +Systemdirs System Envars Aux_file diff --git a/lib/lib.mllib b/lib/lib.mllib index f3f6ad8fc7..4730af32f6 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,3 +1,4 @@ +Systemdirs Errors Bigint Dyn diff --git a/lib/system.ml b/lib/system.ml index 73095f9cd6..6c01a270e2 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -12,45 +12,27 @@ open Pp open Errors open Util open Unix +open Systemdirs -(* All subdirectories, recursively *) - -let exists_dir dir = - try let _ = closedir (opendir dir) in true with Unix_error _ -> false - -let skipped_dirnames = ref ["CVS"; "_darcs"] - -let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames - -let ok_dirname f = - not (String.is_empty f) && f.[0] != '.' && - not (String.List.mem f !skipped_dirnames) && - (match Unicode.ident_refutation f with None -> true | _ -> false) +(** Returns the list of all recursive subdirectories of [root] in + depth-first search, with sons ordered as on the file system; + warns if [root] does not exist *) let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in - let rec traverse dir rel = - let dirh = opendir dir in - try - while true do - let f = readdir dirh in - if ok_dirname f then - let file = Filename.concat dir f in - try - begin match (stat file).st_kind with - | S_DIR -> - let newrel = rel @ [f] in - add file newrel; - traverse file newrel - | _ -> () - end - with Unix_error (e,s1,s2) -> () - done - with End_of_file -> - closedir dirh + let rec traverse path rel = + let f = function + | FileDir (path,f) -> + let newrel = rel @ [f] in + add path newrel; + traverse path newrel + | _ -> () + in process_directory f path in - if exists_dir root then traverse root []; + check_unix_dir (fun s -> msg_warning (str s)) root; + if exists_dir root then traverse root [] + else msg_warning (str ("Cannot open " ^ root)); List.rev !l let rec search paths test = diff --git a/lib/system.mli b/lib/system.mli index a3d66d577a..32a84f5996 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -14,8 +14,6 @@ given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) -val exclude_search_in_dirname : string -> unit - val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool @@ -24,8 +22,6 @@ val where_in_path : val where_in_path_rex : CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list -val exists_dir : string -> bool - val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string diff --git a/lib/systemdirs.ml b/lib/systemdirs.ml new file mode 100644 index 0000000000..2275acd1b1 --- /dev/null +++ b/lib/systemdirs.ml @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* true | _ -> false)*) + +(* Check directory can be opened *) + +let exists_dir dir = + try let _ = closedir (opendir dir) in true with Unix_error _ -> false + +let check_unix_dir warn dir = + if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") && + (String.length dir > 2 && dir.[1] = ':' || + String.contains dir '\\' || + String.contains dir ';') + then warn ("assuming " ^ dir ^ + " to be a Unix path even if looking like a Win32 path.") + +let apply_subdir f path name = + (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) + (* as well as skipped files like CVS, ... *) + if name.[0] <> '.' && ok_dirname name then + let path = if path = "." then name else path//name in + match try (stat path).st_kind with Unix_error _ -> S_BLK with + | S_DIR -> f (FileDir (path,name)) + | S_REG -> f (FileRegular name) + | _ -> () + +let process_directory f path = + let dirh = opendir path in + try while true do apply_subdir f path (readdir dirh) done + with End_of_file -> closedir dirh + +let process_subdirectories f path = + let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in + process_directory f path + diff --git a/lib/systemdirs.mli b/lib/systemdirs.mli new file mode 100644 index 0000000000..5d8d7ff9eb --- /dev/null +++ b/lib/systemdirs.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string -> unix_path + +val exists_dir : unix_path -> bool + +(** [check_unix_dir warn path] calls [warn] with an appropriate + message if [path] looks does not look like a Unix path on Windows *) + +val check_unix_dir : (string -> unit) -> unix_path -> unit + +(** [exclude_search_in_dirname path] excludes [path] when processing + directories *) + +val exclude_directory : unix_path -> unit + +(** [process_directory f path] applies [f] on contents of directory + [path]; fails with Unix_error if the latter does not exists; skips + all files or dirs starting with "." *) + +val process_directory : (file_kind -> unit) -> unix_path -> unit + +(** [process_subdirectories f path] applies [f path/file file] on each + [file] of the directory [path]; fails with Unix_error if the + latter does not exists; kips all files or dirs starting with "." *) + +val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2e0cce6e53..57c9e82f22 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -9,6 +9,7 @@ open Printf open Coqdep_lexer open Coqdep_common +open Systemdirs (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns @@ -461,7 +462,7 @@ let rec parse = function | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll - | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll + | "-exclude-dir" :: r :: ll -> Systemdirs.exclude_directory r; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 2e6a15cebd..7f64949f92 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -9,6 +9,7 @@ open Printf open Coqdep_lexer open Unix +open Systemdirs (** [coqdep_boot] is a stripped-down version of [coqdep], whose behavior is the one of [coqdep -boot]. Its only dependencies @@ -27,26 +28,11 @@ let option_boot = ref false let option_mldep = ref None let norec_dirs = ref ([] : string list) -let norec_dirnames = ref ["CVS"; "_darcs"] let suffixe = ref ".vo" type dir = string option -(* Filename.concat but always with a '/' *) -let is_dir_sep s i = - match Sys.os_type with - | "Unix" -> s.[i] = '/' - | "Cygwin" | "Win32" -> - let c = s.[i] in c = '/' || c = '\\' || c = ':' - | _ -> assert false - -let (//) dirname filename = - let l = String.length dirname in - if l = 0 || is_dir_sep dirname (l-1) - then dirname ^ filename - else dirname ^ "/" ^ filename - (** [get_extension f l] checks whether [f] has one of the extensions listed in [l]. It returns [f] without its extension, alongside with the extension. When no extension match, [(f,"")] is returned *) @@ -165,6 +151,10 @@ let warning_clash file dir = eprintf "%s and %s; used the latter)\n" d2 d1 | _ -> assert false +let warning_cannot_open_dir dir = + eprintf "*** Warning: cannot open %s\n" dir; + flush stderr + let safe_assoc verbose file k = if verbose && List.mem_assoc k !clash_v then warning_clash file k; Hashtbl.find vKnown k @@ -463,42 +453,43 @@ let add_known recur phys_dir log_dir f = List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () -(* Visits all the directories under [dir], including [dir], - or just [dir] if [recur=false] *) +(* Visits all the directories under [dir], including [dir] *) -let rec add_directory recur add_file phys_dir log_dir = - let dirh = opendir phys_dir in - try - while true do - let f = readdir dirh in - (* we avoid all files and subdirs starting by '.' (e.g. .svn), - plus CVS and _darcs and any subdirs given via -exclude-dirs *) - if f.[0] <> '.' then - let phys_f = if phys_dir = "." then f else phys_dir//f in - match try (stat phys_f).st_kind with _ -> S_BLK with - | S_DIR when recur -> - if List.mem f !norec_dirnames then () - else - if List.mem phys_f !norec_dirs then () - else - add_directory recur add_file phys_f (log_dir@[f]) - | S_REG -> add_file phys_dir log_dir f - | _ -> () - done - with End_of_file -> closedir dirh +let is_not_seen_directory phys_f = + not (List.mem phys_f !norec_dirs) + +let rec add_directory add_file phys_dir log_dir = + let f = function + | FileDir (phys_f,f) -> + if is_not_seen_directory phys_f then + add_directory add_file phys_f (log_dir @ [f]) + | FileRegular f -> + add_file phys_dir log_dir f + in + Systemdirs.check_unix_dir (fun s -> eprintf "*** Warning: %s" s) phys_dir; + if exists_dir phys_dir then + process_directory f phys_dir + else + warning_cannot_open_dir phys_dir (** -Q semantic: go in subdirs but only full logical paths are known. *) let add_dir add_file phys_dir log_dir = - try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> () + try add_directory (add_file false) phys_dir log_dir with Unix_error _ -> () (** -R semantic: go in subdirs and suffixes of logical paths are known. *) let add_rec_dir add_file phys_dir log_dir = - handle_unix_error (add_directory true (add_file true) phys_dir) log_dir + add_directory (add_file true) phys_dir log_dir + +(** -R semantic but only on immediate capitalized subdirs *) + +let add_rec_uppercase_subdirs add_file phys_dir log_dir = + process_subdirectories (fun phys_dir f -> + add_directory (add_file true) phys_dir (log_dir@[String.capitalize f])) + phys_dir (** -I semantic: do not go in subdirs. *) let add_caml_dir phys_dir = - handle_unix_error (add_directory true add_caml_known phys_dir) [] - + add_directory add_caml_known phys_dir [] let rec treat_file old_dirname old_name = let name = Filename.basename old_name diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 71b96ca0ee..d6065e4c27 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -6,16 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Systemdirs + val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref val option_natdynlk : bool ref val option_mldep : string option ref val norec_dirs : string list ref -val norec_dirnames : string list ref val suffixe : string ref type dir = string option -val ( // ) : string -> string -> string val get_extension : string -> string list -> string * string val basename_noext : string -> string val mlAccu : (string * string * dir) list ref @@ -41,13 +41,12 @@ val coq_dependencies : unit -> unit val suffixes : 'a list -> 'a list list val add_known : bool -> string -> string list -> string -> unit val add_caml_known : string -> string list -> string -> unit -val add_directory : - bool -> - (string -> string list -> string -> unit) -> string -> string list -> unit val add_caml_dir : string -> unit val add_dir : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val add_rec_dir : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit +val add_rec_uppercase_subdirs : + (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val treat_file : dir -> string -> unit val error_cannot_parse : string -> int * int -> 'a diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0b9bb2f2ee..ffdd846197 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -455,7 +455,7 @@ let parse_args arglist = |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-feedback-glob" -> Dumpglob.feedback_glob () - |"-exclude-dir" -> exclude_search_in_dirname (next ()) + |"-exclude-dir" -> Systemdirs.exclude_directory (next ()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 357c5482fd..ef2e62c3b5 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -11,6 +11,7 @@ open Util open Pp open Flags open Libobject +open Systemdirs open System (* Code to hook Coq into the ML toplevel -- depends on having the @@ -155,7 +156,7 @@ let add_ml_dir s = | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () -(* For Rec Add ML Path *) +(* For Rec Add ML Path (-R) *) let add_rec_ml_dir unix_path = List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) -- cgit v1.2.3 From bff2b36cb0e2dbd02c4f181fba545a420e847767 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 1 Feb 2015 15:11:14 +0100 Subject: Capital letter in plugins. --- checker/check.mllib | 1 - checker/checker.ml | 8 +++++++- plugins/setoid_ring/newring.ml4 | 2 +- tools/coqdep.ml | 6 +++--- toplevel/coqinit.ml | 8 +++++++- 5 files changed, 18 insertions(+), 7 deletions(-) diff --git a/checker/check.mllib b/checker/check.mllib index 8381144e89..2663d8b55a 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -33,7 +33,6 @@ Util Ephemeron Future CUnix - Systemdirs System Profile diff --git a/checker/checker.ml b/checker/checker.ml index 360f996499..263b8785af 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -93,6 +93,12 @@ let add_rec_path ~unix_path ~coq_root = else msg_warning (str ("Cannot open " ^ unix_path)) +let add_rec_uppercase_subpaths ~unix_path ~coq_root = + Systemdirs.process_subdirectories (fun unix_path f -> + let id = Names.Id.of_string (String.capitalize f) in + let coq_root = DirPath.make (id :: DirPath.repr coq_root) in + add_rec_path ~unix_path ~coq_root) unix_path + (* By the option -include -I or -R of the command line *) let includes = ref [] let push_include (s, alias) = includes := (s,alias,false) :: !includes @@ -118,7 +124,7 @@ let init_load_path () = (* first standard library *) add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.DirPath.make[coq_root]); (* then plugins *) - add_rec_path ~unix_path:plugins ~coq_root:(Names.DirPath.make [coq_root]); + add_rec_uppercase_subpaths ~unix_path:plugins ~coq_root:(Names.DirPath.make[coq_root]); (* then user-contrib *) if Sys.file_exists user_contrib then add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 2f9e8509c2..f040de33cf 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -260,7 +260,7 @@ let rec dest_rel t = (****************************************************************************) (* Library linking *) -let plugin_dir = "setoid_ring" +let plugin_dir = "Setoid_ring" let cdir = ["Coq";plugin_dir] let plugin_modules = diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 57c9e82f22..49693212de 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -482,14 +482,14 @@ let coqdep () = (* NOTE: These directories are searched from last to first *) if !option_boot then begin add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "plugins" ["Coq"]; + add_rec_uppercase_subdirs add_known "plugins" ["Coq"]; add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; - add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; + add_rec_uppercase_subdirs (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin Envars.set_coqlib ~fail:Errors.error; let coqlib = Envars.coqlib () in add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; - add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; + add_rec_uppercase_subdirs add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in if Sys.file_exists user then add_dir add_coqlib_known user []; List.iter (fun s -> add_dir add_coqlib_known s []) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 03074ced70..2d3418ce02 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -71,6 +71,12 @@ let add_stdlib_path ~unix_path ~coq_root ~with_ml = if with_ml then Mltop.add_rec_ml_dir unix_path +let add_stdlib_uppercase_subpaths ~unix_path ~coq_root ~with_ml = + Systemdirs.process_subdirectories (fun unix_path f -> + let id = Names.Id.of_string (String.capitalize f) in + let coq_root = Libnames.add_dirpath_suffix coq_root id in + add_stdlib_path ~unix_path ~coq_root ~with_ml) unix_path + let add_userlib_path ~unix_path = Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; Mltop.add_rec_ml_dir unix_path @@ -101,7 +107,7 @@ let init_load_path () = (* then standard library *) add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; (* then plugins *) - add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; + add_stdlib_uppercase_subpaths ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:false; (* then user-contrib *) if Sys.file_exists user_contrib then add_userlib_path ~unix_path:user_contrib; -- cgit v1.2.3 From 9daec838c8896e7c1048b42d01eba0c71c912f00 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 12 Feb 2015 18:51:14 +0100 Subject: Revert "Capital letter in plugins." (Sorry, was not intended to be pushed) This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767. --- checker/check.mllib | 1 + checker/checker.ml | 8 +------- plugins/setoid_ring/newring.ml4 | 2 +- tools/coqdep.ml | 6 +++--- toplevel/coqinit.ml | 8 +------- 5 files changed, 7 insertions(+), 18 deletions(-) diff --git a/checker/check.mllib b/checker/check.mllib index 2663d8b55a..8381144e89 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -33,6 +33,7 @@ Util Ephemeron Future CUnix + Systemdirs System Profile diff --git a/checker/checker.ml b/checker/checker.ml index 263b8785af..360f996499 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -93,12 +93,6 @@ let add_rec_path ~unix_path ~coq_root = else msg_warning (str ("Cannot open " ^ unix_path)) -let add_rec_uppercase_subpaths ~unix_path ~coq_root = - Systemdirs.process_subdirectories (fun unix_path f -> - let id = Names.Id.of_string (String.capitalize f) in - let coq_root = DirPath.make (id :: DirPath.repr coq_root) in - add_rec_path ~unix_path ~coq_root) unix_path - (* By the option -include -I or -R of the command line *) let includes = ref [] let push_include (s, alias) = includes := (s,alias,false) :: !includes @@ -124,7 +118,7 @@ let init_load_path () = (* first standard library *) add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.DirPath.make[coq_root]); (* then plugins *) - add_rec_uppercase_subpaths ~unix_path:plugins ~coq_root:(Names.DirPath.make[coq_root]); + add_rec_path ~unix_path:plugins ~coq_root:(Names.DirPath.make [coq_root]); (* then user-contrib *) if Sys.file_exists user_contrib then add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index f040de33cf..2f9e8509c2 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -260,7 +260,7 @@ let rec dest_rel t = (****************************************************************************) (* Library linking *) -let plugin_dir = "Setoid_ring" +let plugin_dir = "setoid_ring" let cdir = ["Coq";plugin_dir] let plugin_modules = diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 49693212de..57c9e82f22 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -482,14 +482,14 @@ let coqdep () = (* NOTE: These directories are searched from last to first *) if !option_boot then begin add_rec_dir add_known "theories" ["Coq"]; - add_rec_uppercase_subdirs add_known "plugins" ["Coq"]; + add_rec_dir add_known "plugins" ["Coq"]; add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; - add_rec_uppercase_subdirs (fun _ -> add_caml_known) "plugins" ["Coq"]; + add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin Envars.set_coqlib ~fail:Errors.error; let coqlib = Envars.coqlib () in add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; - add_rec_uppercase_subdirs add_coqlib_known (coqlib//"plugins") ["Coq"]; + add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in if Sys.file_exists user then add_dir add_coqlib_known user []; List.iter (fun s -> add_dir add_coqlib_known s []) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 2d3418ce02..03074ced70 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -71,12 +71,6 @@ let add_stdlib_path ~unix_path ~coq_root ~with_ml = if with_ml then Mltop.add_rec_ml_dir unix_path -let add_stdlib_uppercase_subpaths ~unix_path ~coq_root ~with_ml = - Systemdirs.process_subdirectories (fun unix_path f -> - let id = Names.Id.of_string (String.capitalize f) in - let coq_root = Libnames.add_dirpath_suffix coq_root id in - add_stdlib_path ~unix_path ~coq_root ~with_ml) unix_path - let add_userlib_path ~unix_path = Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; Mltop.add_rec_ml_dir unix_path @@ -107,7 +101,7 @@ let init_load_path () = (* then standard library *) add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; (* then plugins *) - add_stdlib_uppercase_subpaths ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:false; + add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; (* then user-contrib *) if Sys.file_exists user_contrib then add_userlib_path ~unix_path:user_contrib; -- cgit v1.2.3 From de8888e28ad793511ba2e2969516325b0be44330 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 12 Feb 2015 18:52:09 +0100 Subject: Revert "Using same code for browsing physical directories in coqtop and coqdep." (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. --- Makefile.build | 1 - Makefile.common | 2 +- checker/check.mllib | 2 -- checker/checker.ml | 1 - dev/printers.mllib | 1 - lib/lib.mllib | 1 - lib/system.ml | 48 ++++++++++++++++++++++---------- lib/system.mli | 4 +++ lib/systemdirs.ml | 70 ----------------------------------------------- lib/systemdirs.mli | 41 --------------------------- tools/coqdep.ml | 3 +- tools/coqdep_common.ml | 73 +++++++++++++++++++++++++++---------------------- tools/coqdep_common.mli | 9 +++--- toplevel/coqtop.ml | 2 +- toplevel/mltop.ml | 3 +- 15 files changed, 87 insertions(+), 174 deletions(-) delete mode 100644 lib/systemdirs.ml delete mode 100644 lib/systemdirs.mli diff --git a/Makefile.build b/Makefile.build index 6c3834ae43..0d87d98e96 100644 --- a/Makefile.build +++ b/Makefile.build @@ -606,7 +606,6 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) # coqdep_boot. COQDEPBOOTSRC:= \ - lib/systemdirs.mli lib/systemdirs.ml \ tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ tools/coqdep_common.mli tools/coqdep_common.ml \ tools/coqdep_boot.ml diff --git a/Makefile.common b/Makefile.common index f83d8b88c6..d752a5be91 100644 --- a/Makefile.common +++ b/Makefile.common @@ -232,7 +232,7 @@ IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc -COQENVCMO:=lib/clib.cma lib/errors.cmo lib/systemdirs.cmo +COQENVCMO:=lib/clib.cma lib/errors.cmo COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo diff --git a/checker/check.mllib b/checker/check.mllib index 8381144e89..22df375623 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -33,8 +33,6 @@ Util Ephemeron Future CUnix - -Systemdirs System Profile RemoteCounter diff --git a/checker/checker.ml b/checker/checker.ml index 360f996499..ffe1553197 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -10,7 +10,6 @@ open Pp open Errors open Util open System -open Systemdirs open Flags open Names open Check diff --git a/dev/printers.mllib b/dev/printers.mllib index 7f8d4aad16..2f78c2e915 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -37,7 +37,6 @@ Util Bigint Dyn CUnix -Systemdirs System Envars Aux_file diff --git a/lib/lib.mllib b/lib/lib.mllib index 4730af32f6..f3f6ad8fc7 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,4 +1,3 @@ -Systemdirs Errors Bigint Dyn diff --git a/lib/system.ml b/lib/system.ml index 6c01a270e2..73095f9cd6 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -12,27 +12,45 @@ open Pp open Errors open Util open Unix -open Systemdirs -(** Returns the list of all recursive subdirectories of [root] in - depth-first search, with sons ordered as on the file system; - warns if [root] does not exist *) +(* All subdirectories, recursively *) + +let exists_dir dir = + try let _ = closedir (opendir dir) in true with Unix_error _ -> false + +let skipped_dirnames = ref ["CVS"; "_darcs"] + +let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames + +let ok_dirname f = + not (String.is_empty f) && f.[0] != '.' && + not (String.List.mem f !skipped_dirnames) && + (match Unicode.ident_refutation f with None -> true | _ -> false) let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in - let rec traverse path rel = - let f = function - | FileDir (path,f) -> - let newrel = rel @ [f] in - add path newrel; - traverse path newrel - | _ -> () - in process_directory f path + let rec traverse dir rel = + let dirh = opendir dir in + try + while true do + let f = readdir dirh in + if ok_dirname f then + let file = Filename.concat dir f in + try + begin match (stat file).st_kind with + | S_DIR -> + let newrel = rel @ [f] in + add file newrel; + traverse file newrel + | _ -> () + end + with Unix_error (e,s1,s2) -> () + done + with End_of_file -> + closedir dirh in - check_unix_dir (fun s -> msg_warning (str s)) root; - if exists_dir root then traverse root [] - else msg_warning (str ("Cannot open " ^ root)); + if exists_dir root then traverse root []; List.rev !l let rec search paths test = diff --git a/lib/system.mli b/lib/system.mli index 32a84f5996..a3d66d577a 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -14,6 +14,8 @@ given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) +val exclude_search_in_dirname : string -> unit + val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool @@ -22,6 +24,8 @@ val where_in_path : val where_in_path_rex : CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list +val exists_dir : string -> bool + val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string diff --git a/lib/systemdirs.ml b/lib/systemdirs.ml deleted file mode 100644 index 2275acd1b1..0000000000 --- a/lib/systemdirs.ml +++ /dev/null @@ -1,70 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true | _ -> false)*) - -(* Check directory can be opened *) - -let exists_dir dir = - try let _ = closedir (opendir dir) in true with Unix_error _ -> false - -let check_unix_dir warn dir = - if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") && - (String.length dir > 2 && dir.[1] = ':' || - String.contains dir '\\' || - String.contains dir ';') - then warn ("assuming " ^ dir ^ - " to be a Unix path even if looking like a Win32 path.") - -let apply_subdir f path name = - (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) - (* as well as skipped files like CVS, ... *) - if name.[0] <> '.' && ok_dirname name then - let path = if path = "." then name else path//name in - match try (stat path).st_kind with Unix_error _ -> S_BLK with - | S_DIR -> f (FileDir (path,name)) - | S_REG -> f (FileRegular name) - | _ -> () - -let process_directory f path = - let dirh = opendir path in - try while true do apply_subdir f path (readdir dirh) done - with End_of_file -> closedir dirh - -let process_subdirectories f path = - let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in - process_directory f path - diff --git a/lib/systemdirs.mli b/lib/systemdirs.mli deleted file mode 100644 index 5d8d7ff9eb..0000000000 --- a/lib/systemdirs.mli +++ /dev/null @@ -1,41 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string -> unix_path - -val exists_dir : unix_path -> bool - -(** [check_unix_dir warn path] calls [warn] with an appropriate - message if [path] looks does not look like a Unix path on Windows *) - -val check_unix_dir : (string -> unit) -> unix_path -> unit - -(** [exclude_search_in_dirname path] excludes [path] when processing - directories *) - -val exclude_directory : unix_path -> unit - -(** [process_directory f path] applies [f] on contents of directory - [path]; fails with Unix_error if the latter does not exists; skips - all files or dirs starting with "." *) - -val process_directory : (file_kind -> unit) -> unix_path -> unit - -(** [process_subdirectories f path] applies [f path/file file] on each - [file] of the directory [path]; fails with Unix_error if the - latter does not exists; kips all files or dirs starting with "." *) - -val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 57c9e82f22..2e0cce6e53 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -9,7 +9,6 @@ open Printf open Coqdep_lexer open Coqdep_common -open Systemdirs (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns @@ -462,7 +461,7 @@ let rec parse = function | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll - | "-exclude-dir" :: r :: ll -> Systemdirs.exclude_directory r; parse ll + | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 7f64949f92..2e6a15cebd 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -9,7 +9,6 @@ open Printf open Coqdep_lexer open Unix -open Systemdirs (** [coqdep_boot] is a stripped-down version of [coqdep], whose behavior is the one of [coqdep -boot]. Its only dependencies @@ -28,11 +27,26 @@ let option_boot = ref false let option_mldep = ref None let norec_dirs = ref ([] : string list) +let norec_dirnames = ref ["CVS"; "_darcs"] let suffixe = ref ".vo" type dir = string option +(* Filename.concat but always with a '/' *) +let is_dir_sep s i = + match Sys.os_type with + | "Unix" -> s.[i] = '/' + | "Cygwin" | "Win32" -> + let c = s.[i] in c = '/' || c = '\\' || c = ':' + | _ -> assert false + +let (//) dirname filename = + let l = String.length dirname in + if l = 0 || is_dir_sep dirname (l-1) + then dirname ^ filename + else dirname ^ "/" ^ filename + (** [get_extension f l] checks whether [f] has one of the extensions listed in [l]. It returns [f] without its extension, alongside with the extension. When no extension match, [(f,"")] is returned *) @@ -151,10 +165,6 @@ let warning_clash file dir = eprintf "%s and %s; used the latter)\n" d2 d1 | _ -> assert false -let warning_cannot_open_dir dir = - eprintf "*** Warning: cannot open %s\n" dir; - flush stderr - let safe_assoc verbose file k = if verbose && List.mem_assoc k !clash_v then warning_clash file k; Hashtbl.find vKnown k @@ -453,43 +463,42 @@ let add_known recur phys_dir log_dir f = List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () -(* Visits all the directories under [dir], including [dir] *) - -let is_not_seen_directory phys_f = - not (List.mem phys_f !norec_dirs) +(* Visits all the directories under [dir], including [dir], + or just [dir] if [recur=false] *) -let rec add_directory add_file phys_dir log_dir = - let f = function - | FileDir (phys_f,f) -> - if is_not_seen_directory phys_f then - add_directory add_file phys_f (log_dir @ [f]) - | FileRegular f -> - add_file phys_dir log_dir f - in - Systemdirs.check_unix_dir (fun s -> eprintf "*** Warning: %s" s) phys_dir; - if exists_dir phys_dir then - process_directory f phys_dir - else - warning_cannot_open_dir phys_dir +let rec add_directory recur add_file phys_dir log_dir = + let dirh = opendir phys_dir in + try + while true do + let f = readdir dirh in + (* we avoid all files and subdirs starting by '.' (e.g. .svn), + plus CVS and _darcs and any subdirs given via -exclude-dirs *) + if f.[0] <> '.' then + let phys_f = if phys_dir = "." then f else phys_dir//f in + match try (stat phys_f).st_kind with _ -> S_BLK with + | S_DIR when recur -> + if List.mem f !norec_dirnames then () + else + if List.mem phys_f !norec_dirs then () + else + add_directory recur add_file phys_f (log_dir@[f]) + | S_REG -> add_file phys_dir log_dir f + | _ -> () + done + with End_of_file -> closedir dirh (** -Q semantic: go in subdirs but only full logical paths are known. *) let add_dir add_file phys_dir log_dir = - try add_directory (add_file false) phys_dir log_dir with Unix_error _ -> () + try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> () (** -R semantic: go in subdirs and suffixes of logical paths are known. *) let add_rec_dir add_file phys_dir log_dir = - add_directory (add_file true) phys_dir log_dir - -(** -R semantic but only on immediate capitalized subdirs *) - -let add_rec_uppercase_subdirs add_file phys_dir log_dir = - process_subdirectories (fun phys_dir f -> - add_directory (add_file true) phys_dir (log_dir@[String.capitalize f])) - phys_dir + handle_unix_error (add_directory true (add_file true) phys_dir) log_dir (** -I semantic: do not go in subdirs. *) let add_caml_dir phys_dir = - add_directory add_caml_known phys_dir [] + handle_unix_error (add_directory true add_caml_known phys_dir) [] + let rec treat_file old_dirname old_name = let name = Filename.basename old_name diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index d6065e4c27..71b96ca0ee 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -6,16 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Systemdirs - val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref val option_natdynlk : bool ref val option_mldep : string option ref val norec_dirs : string list ref +val norec_dirnames : string list ref val suffixe : string ref type dir = string option +val ( // ) : string -> string -> string val get_extension : string -> string list -> string * string val basename_noext : string -> string val mlAccu : (string * string * dir) list ref @@ -41,12 +41,13 @@ val coq_dependencies : unit -> unit val suffixes : 'a list -> 'a list list val add_known : bool -> string -> string list -> string -> unit val add_caml_known : string -> string list -> string -> unit +val add_directory : + bool -> + (string -> string list -> string -> unit) -> string -> string list -> unit val add_caml_dir : string -> unit val add_dir : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val add_rec_dir : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit -val add_rec_uppercase_subdirs : - (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val treat_file : dir -> string -> unit val error_cannot_parse : string -> int * int -> 'a diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ffdd846197..0b9bb2f2ee 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -455,7 +455,7 @@ let parse_args arglist = |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-feedback-glob" -> Dumpglob.feedback_glob () - |"-exclude-dir" -> Systemdirs.exclude_directory (next ()) + |"-exclude-dir" -> exclude_search_in_dirname (next ()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index ef2e62c3b5..357c5482fd 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -11,7 +11,6 @@ open Util open Pp open Flags open Libobject -open Systemdirs open System (* Code to hook Coq into the ML toplevel -- depends on having the @@ -156,7 +155,7 @@ let add_ml_dir s = | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () -(* For Rec Add ML Path (-R) *) +(* For Rec Add ML Path *) let add_rec_ml_dir unix_path = List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) -- cgit v1.2.3 From e9b239881bc32dd15ac53b9463708030c95a9e0c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Feb 2015 18:54:10 +0100 Subject: Focussing on message view in CoqIDE when a message is pushed. Also fixes bug #4030. --- ide/session.ml | 16 ++++++++++++---- ide/wg_MessageView.ml | 24 +++++++++++++++++++++++- ide/wg_MessageView.mli | 8 ++++++++ 3 files changed, 43 insertions(+), 5 deletions(-) diff --git a/ide/session.ml b/ide/session.ml index 2936321128..072ae61c68 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -465,7 +465,7 @@ let build_layout (sn:session) = message_frame#misc#show (); detachable#show); detachable#button#misc#hide (); - lbl in + detachable, lbl in let session_tab = GPack.hbox ~homogeneous:false () in let img = GMisc.image ~icon_size:`SMALL_TOOLBAR ~packing:session_tab#pack () in @@ -496,9 +496,17 @@ let build_layout (sn:session) = sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false); script_scroll#add sn.script#coerce; proof_scroll#add sn.proof#coerce; - ignore(add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce); - let label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in - ignore(add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce); + let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce in + let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in + let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in + (** When a message is received, focus on the message pane *) + let _ = + sn.messages#connect#pushed ~callback:(fun _ _ -> + let num = message_frame#page_num detach#coerce in + if 0 <= num then message_frame#goto_page num + ) + in + (** When an error occurs, paint the error label in red *) let txt = label#text in let red s = "" ^ s ^ "" in sn.errpage#on_update ~callback:(fun l -> diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 9acda53fc3..09f1d44535 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -6,9 +6,25 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +class type message_view_signals = +object + inherit GObj.misc_signals + inherit GUtil.add_ml_signals + method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id +end + +class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals = +object + val after = false + inherit GObj.misc_signals obj + inherit GUtil.add_ml_signals obj [pushed#disconnect] + method pushed ~callback = pushed#connect ~after ~callback:(fun (lvl, s) -> callback lvl s) +end + class type message_view = object inherit GObj.widget + method connect : message_view_signals method clear : unit method add : string -> unit method set : string -> unit @@ -38,6 +54,11 @@ let message_view () : message_view = object (self) inherit GObj.widget box#as_widget + val push = new GUtil.signal () + + method connect = + new message_view_signals_impl box#as_widget push + method clear = buffer#set_text "" @@ -49,7 +70,8 @@ let message_view () : message_view = in if msg <> "" then begin buffer#insert ~tags msg; - buffer#insert ~tags "\n" + buffer#insert ~tags "\n"; + push#call (level, msg) end method add msg = self#push Pp.Notice msg diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index cd3f00c97d..4dcd7306ba 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -6,9 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +class type message_view_signals = +object + inherit GObj.misc_signals + inherit GUtil.add_ml_signals + method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id +end + class type message_view = object inherit GObj.widget + method connect : message_view_signals method clear : unit method add : string -> unit method set : string -> unit -- cgit v1.2.3 From 154bb6a5134c35caea187b83334c098dbadb4e48 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Feb 2015 19:43:08 +0100 Subject: Fixing bug #3261. --- ide/coqide.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index 78fcbaf8cf..1d76ceada4 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -591,10 +591,12 @@ let get_current_word term = if term.script#buffer#has_selection then let (start, stop) = term.script#buffer#selection_bounds in term.script#buffer#get_text ~slice:true ~start ~stop () - (** Otherwise try to recover the clipboard *) - else match Ideutils.cb#text with - | Some t -> t - | None -> "" + (** Otherwise try to find the word around the cursor *) + else + let it = term.script#buffer#get_iter_at_mark `INSERT in + let start = find_word_start it in + let stop = find_word_end start in + term.script#buffer#get_text ~slice:true ~start ~stop () let print_branch c l = Format.fprintf c " | @[%a@]=> _@\n" -- cgit v1.2.3 From 7d06e602bea9e7a2c98e1c6badab3a667714b5c8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Feb 2015 22:33:22 +0100 Subject: Fix typos about .vio files (thanks Arthur for spotting them) --- CHANGES | 2 +- doc/refman/RefMan-ext.tex | 2 +- toplevel/usage.ml | 1 + 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index a8411a2126..ca31ca2398 100644 --- a/CHANGES +++ b/CHANGES @@ -292,7 +292,7 @@ Tools added to the load path. (Same behavior as with coq/user-contrib.) - coqdep accepts a -dumpgraph option generating a dot file. - Makefiles generated through coq_makefile have three new targets "quick" - "checkproof" and "vio2vo", allowing respectively to asynchronously compile + "checkproofs" and "vio2vo", allowing respectively to asynchronously compile the files without playing the proof scripts, asynchronously checking that the quickly generated proofs are correct and generating the object files from the quickly generated proofs. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 71eb0108d3..11b4f26145 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1059,7 +1059,7 @@ Please note that the questions described here have been subject to redesign in Coq v8.5. Former versions of Coq use the same terminology to describe slightly different things. -Compiled files (\texttt{.vo} and \texttt{.vi}) store sub-libraries. In +Compiled files (\texttt{.vo} and \texttt{.vio}) store sub-libraries. In order to refer to them inside {\Coq}, a translation from file-system names to {\Coq} names is needed. In this translation, names in the file system are called {\em physical} paths while {\Coq} names are diff --git a/toplevel/usage.ml b/toplevel/usage.ml index d4d4456994..e9b5e8f84a 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -47,6 +47,7 @@ let print_usage_channel co command = \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 -quick quickly compile .v files to .vio files (skip proofs)\ \n\ \n -where print Coq's standard library location and exit\ \n -config print Coq's configuration information and exit\ -- cgit v1.2.3 From 43471abd4e61e7528fdaa2c576e7cb825a203c13 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 12 Feb 2015 21:43:03 +0100 Subject: Fix bug #2775: Correct handling of universes in leminv. --- tactics/leminv.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index f00ecf8feb..9a64b03fd1 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -210,6 +210,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = end in let avoid = ref [] in let { sigma=sigma } = Proof.V82.subgoals pf in + let sigma = Evd.nf_constraints sigma in let rec fill_holes c = match kind_of_term c with | Evar (e,args) -> @@ -222,13 +223,13 @@ let inversion_scheme env sigma t sort dep_option inv_op = in let c = fill_holes pfterm in (* warning: side-effect on ownSign *) - let invProof = it_mkNamedLambda_or_LetIn c !ownSign - in - invProof + let invProof = it_mkNamedLambda_or_LetIn c !ownSign in + let p = Evarutil.nf_evars_universes sigma invProof in + p, Evd.universe_context sigma let add_inversion_lemma name env sigma t sort dep inv_op = - let invProof = inversion_scheme env sigma t sort dep inv_op in - let entry = definition_entry ~poly:true (*FIXME*) invProof in + let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in + let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () @@ -236,7 +237,8 @@ let add_inversion_lemma name env sigma t sort dep inv_op = * inv_op = InvNoThining (derives de semi inversion lemma) *) let add_inversion_lemma_exn na com comsort bool tac = - let env = Global.env () and evd = ref Evd.empty in + let env = Global.env () in + let evd = ref (Evd.from_env env) in let c = Constrintern.interp_type_evars env evd com in let sigma, sort = Pretyping.interp_sort !evd comsort in try -- cgit v1.2.3 From 5c603ebd99e4e8e7abb8b2036a6ffac5b19f66cf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 12 Feb 2015 22:41:40 +0100 Subject: Univs: fix bug #3978: carry around the universe context used to typecheck with definitions and thread it accordingly when typechecking module expressions. --- interp/modintern.ml | 4 +++- kernel/declarations.mli | 2 +- kernel/mod_typing.ml | 27 +++++++++++++++------------ kernel/modops.ml | 4 ++-- plugins/extraction/extract_env.ml | 2 +- 5 files changed, 22 insertions(+), 17 deletions(-) diff --git a/interp/modintern.ml b/interp/modintern.ml index fdc6e609bc..bf0b2f9800 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -61,7 +61,9 @@ let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> WithMod (fqid,lookup_module qid) | CWith_Definition ((_,fqid),c) -> - WithDef (fqid,fst (interp_constr env Evd.empty c)) (*FIXME*) + let c, ectx = interp_constr env (Evd.from_env env) c in + let ctx = Univ.ContextSet.to_context (Evd.evar_universe_context_set ectx) in + WithDef (fqid,(c,ctx)) let loc_of_module = function | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc diff --git a/kernel/declarations.mli b/kernel/declarations.mli index bec521227b..cef920c6a5 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -202,7 +202,7 @@ type ('ty,'a) functorize = type with_declaration = | WithMod of Id.t list * module_path - | WithDef of Id.t list * constr + | WithDef of Id.t list * constr Univ.in_universe_context type module_alg_expr = | MEident of module_path diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 97c1d1fdfa..99d353aae6 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -54,7 +54,7 @@ let rec rebuild_mp mp l = let (+++) = Univ.Constraint.union -let rec check_with_def env struc (idl,c) mp equiv = +let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let lab,idl = match idl with | [] -> assert false | id::idl -> Label.of_id id, idl @@ -74,30 +74,33 @@ let rec check_with_def env struc (idl,c) mp equiv = as long as they have the right type *) let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in let env' = Environ.add_constraints ccst env' in + let newus, cst = Univ.UContext.dest ctx in + let env' = Environ.add_constraints cst env' in let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in let typ = Typeops.type_of_constant_type env' cb.const_type in - let cst = Reduction.infer_conv_leq env' (Environ.universes env') + let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in - j.uj_val,cst + j.uj_val,cst' +++ cst | Def cs -> - let cst = Reduction.infer_conv env' (Environ.universes env') c + let cst' = Reduction.infer_conv env' (Environ.universes env') c (Mod_subst.force_constr cs) in let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *) - if cb.const_polymorphic then cst - else ccst +++ cst + if cb.const_polymorphic then cst' +++ cst + else cst' +++ cst in c, cst in let def = Def (Mod_subst.from_val c') in + let ctx' = Univ.UContext.make (newus, cst) in let cb' = { cb with const_body = def; - const_body_code = Cemitcodes.from_val (compile_constant_body env' def) } - (* const_universes = Future.from_val cst } *) + const_body_code = Cemitcodes.from_val (compile_constant_body env' def); + const_universes = ctx' } in - before@(lab,SFBconst(cb'))::after, c', cst + before@(lab,SFBconst(cb'))::after, c', ctx' else (* Definition inside a sub-module *) let mb = match spec with @@ -108,7 +111,7 @@ let rec check_with_def env struc (idl,c) mp equiv = | Abstract -> let struc = Modops.destr_nofunctor mb.mod_type in let struc',c',cst = - check_with_def env' struc (idl,c) (MPdot(mp,lab)) mb.mod_delta + check_with_def env' struc (idl,(c,ctx)) (MPdot(mp,lab)) mb.mod_delta in let mb' = { mb with mod_type = NoFunctor struc'; @@ -204,8 +207,8 @@ let check_with env mp (sign,alg,reso,cst) = function |WithDef(idl,c) -> let struc = destr_nofunctor sign in let struc',c',cst' = check_with_def env struc (idl,c) mp reso in - let alg' = mk_alg_with alg (WithDef (idl,c')) in - (NoFunctor struc'),alg',reso, cst+++cst' + let alg' = mk_alg_with alg (WithDef (idl,(c',cst'))) in + (NoFunctor struc'),alg',reso, cst+++(Univ.UContext.constraints cst') |WithMod(idl,mp1) as wd -> let struc = destr_nofunctor sign in let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in diff --git a/kernel/modops.ml b/kernel/modops.ml index 392e667b8e..83be03ffd8 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -177,9 +177,9 @@ let subst_with_body sub = function |WithMod(id,mp) as orig -> let mp' = subst_mp sub mp in if mp==mp' then orig else WithMod(id,mp') - |WithDef(id,c) as orig -> + |WithDef(id,(c,ctx)) as orig -> let c' = subst_mps sub c in - if c==c' then orig else WithDef(id,c') + if c==c' then orig else WithDef(id,(c',ctx)) let rec subst_structure sub do_delta sign = let subst_body ((l,body) as orig) = match body with diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 42e69d342e..90ee6d0ef1 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -235,7 +235,7 @@ let rec extract_structure_spec env mp = function and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with | MEident mp -> Visit.add_mp_all mp; MTident mp - | MEwith(me',WithDef(idl,c))-> + | MEwith(me',WithDef(idl,(c,ctx)))-> let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in let mt = extract_mexpr_spec env mp1 (me_struct,me') in (match extract_with_type env' c with (* cb may contain some kn *) -- cgit v1.2.3 From 8c5bfa0f00b80979473bba26c1b9a1410667e032 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 12 Feb 2015 22:49:35 +0100 Subject: Univs: fix bug #4031: wrong folding of sigma in change. --- tactics/tactics.ml | 8 ++++++-- test-suite/bugs/closed/4031.v | 14 ++++++++++++++ 2 files changed, 20 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/4031.v diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a298bba978..04df3b8cda 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -569,8 +569,12 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env let sigma',ty' = redfun false env sigma ty in sigma', (id,None,ty') | Some b -> - let sigma',b' = if where != InHypTypeOnly then redfun true env sigma b else sigma, b in - let sigma',ty' = if where != InHypValueOnly then redfun false env sigma ty else sigma', ty in + let sigma',b' = + if where != InHypTypeOnly then redfun true env sigma b else sigma, b + in + let sigma',ty' = + if where != InHypValueOnly then redfun false env sigma' ty else sigma', ty + in sigma', (id,Some b',ty') let e_change_in_hyp redfun (id,where) = diff --git a/test-suite/bugs/closed/4031.v b/test-suite/bugs/closed/4031.v new file mode 100644 index 0000000000..2b8641ebb0 --- /dev/null +++ b/test-suite/bugs/closed/4031.v @@ -0,0 +1,14 @@ +Definition something (P:Type) (e:P) := e. + +Inductive myunit : Set := mytt. + (* Proof below works when definition is in Type, + however builtin types such as unit are in Set. *) + +Lemma demo_hide_generic : + let x := mytt in x = x. +Proof. + intros. + change mytt with (@something _ mytt) in x. + subst x. (* Proof works if this line is removed *) + reflexivity. +Qed. \ No newline at end of file -- cgit v1.2.3 From 1e1a2f1803c57cc1697e294a7610b76a95661687 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 12 Feb 2015 22:59:41 +0100 Subject: COMPATIBILITY: add note about the change of behavior of Instance foo := {| |}. Add test-suite files for closed bugs. --- COMPATIBILITY | 7 +++++++ test-suite/bugs/closed/2775.v | 6 ++++++ test-suite/bugs/closed/3978.v | 27 +++++++++++++++++++++++++++ 3 files changed, 40 insertions(+) create mode 100644 test-suite/bugs/closed/2775.v create mode 100644 test-suite/bugs/closed/3978.v diff --git a/COMPATIBILITY b/COMPATIBILITY index 2ce29346c5..3b4e8987c9 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -26,6 +26,13 @@ Universe Polymorphism. (e.g. induction). Extra "Transparent" might have to be added to revert opacity of constants. +Type classes. + +- When writing an Instance foo : Class A := {| proj := t |} (note the + vertical bars), support for typechecking the projections using the + type information and switching to proof mode is no longer available. + Use { } (without the vertical bars) instead. + Potential sources of incompatibilities between Coq V8.3 and V8.4 ---------------------------------------------------------------- diff --git a/test-suite/bugs/closed/2775.v b/test-suite/bugs/closed/2775.v new file mode 100644 index 0000000000..f1f384bdf7 --- /dev/null +++ b/test-suite/bugs/closed/2775.v @@ -0,0 +1,6 @@ +Inductive typ : forall (T:Type), list T -> Type -> Prop := + | Get : forall (T:Type) (l:list T), typ T l T. + + +Derive Inversion inv with +(forall (X: Type) (y: list nat), typ nat y X) Sort Prop. diff --git a/test-suite/bugs/closed/3978.v b/test-suite/bugs/closed/3978.v new file mode 100644 index 0000000000..26e021e719 --- /dev/null +++ b/test-suite/bugs/closed/3978.v @@ -0,0 +1,27 @@ +Require Import Structures.OrderedType. +Require Import Structures.OrderedTypeEx. + +Module Type M. Parameter X : Type. + +Declare Module Export XOrd : OrderedType + with Definition t := X + with Definition eq := @Logic.eq X. +End M. + +Module M' : M. + Definition X := nat. + + Module XOrd := Nat_as_OT. +End M'. + +Module Type MyOt. + Parameter t : Type. + Parameter eq : t -> t -> Prop. +End MyOt. + +Module Type M2. Parameter X : Type. + +Declare Module Export XOrd : MyOt + with Definition t := X + with Definition eq := @Logic.eq X. +End M2. -- cgit v1.2.3 From 69212fa135879b8df4cf3347a6bee0af769a3ee7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Feb 2015 22:07:32 +0100 Subject: Tentative fix for CoqIDE randomly dropping deletions. We make the deletion callback not to regenerate a task id, as the insertion callback does. I can't find a particular reason for this dissymetry, and it was indeed causing trouble. --- ide/session.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/ide/session.ml b/ide/session.ml index 072ae61c68..47b747dae7 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -160,7 +160,6 @@ let set_buffer_handlers end end in let delete_cb ~start ~stop = Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset); - cur_action := new_action_id (); let min_iter, max_iter = if start#compare stop < 0 then start, stop else stop, start in let text_mark = add_mark min_iter in -- cgit v1.2.3 From dd0f375656aee2b5eb74380cc3081ef7d8ebe0a4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 12 Feb 2015 23:16:49 +0100 Subject: Add test-suite files for closed bugs. --- test-suite/bugs/closed/2590.v | 19 +++++++++++++++++++ test-suite/bugs/closed/3560.v | 15 +++++++++++++++ test-suite/bugs/closed/3783.v | 32 ++++++++++++++++++++++++++++++++ 3 files changed, 66 insertions(+) create mode 100644 test-suite/bugs/closed/2590.v create mode 100644 test-suite/bugs/closed/3560.v create mode 100644 test-suite/bugs/closed/3783.v diff --git a/test-suite/bugs/closed/2590.v b/test-suite/bugs/closed/2590.v new file mode 100644 index 0000000000..e594e96936 --- /dev/null +++ b/test-suite/bugs/closed/2590.v @@ -0,0 +1,19 @@ +Require Import Relation_Definitions RelationClasses Setoid SetoidClass. + +Section Bug. + + Context {A : Type} (R : relation A). + Hypothesis pre : PreOrder R. + Context `{SA : Setoid A}. + + Goal True. + set (SA' := SA). + assert ( forall SA0 : Setoid A, + @PartialOrder A (@equiv A SA0) (@setoid_equiv A SA0) R pre ). + rename SA into SA0. + intro SA. + admit. + admit. +Qed. +End Bug. + diff --git a/test-suite/bugs/closed/3560.v b/test-suite/bugs/closed/3560.v new file mode 100644 index 0000000000..65ce4fb6b0 --- /dev/null +++ b/test-suite/bugs/closed/3560.v @@ -0,0 +1,15 @@ + +(* File reduced by coq-bug-finder from original input, then from 6236 lines to 1049 lines, then from 920 lines to 209 lines, then from 179 lines to 30 lines *) +(* coqc version trunk (August 2014) compiled on Aug 31 2014 10:12:32 with OCaml 4.01.0 + coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (437b91a3ffd7327975a129b95b24d3f66ad7f3e4) *) + +Set Primitive Projections. +Set Implicit Arguments. +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Notation "x * y" := (prod x y) : type_scope. +Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv : forall P, P equiv_fun }. +Goal forall (A B : Type) (C : Type), Equiv (A -> B -> C) (A * B -> C). +Proof. + intros. + exists (fun u => fun x => u (fst x) (snd x)). +Abort. \ No newline at end of file diff --git a/test-suite/bugs/closed/3783.v b/test-suite/bugs/closed/3783.v new file mode 100644 index 0000000000..33ca9651a5 --- /dev/null +++ b/test-suite/bugs/closed/3783.v @@ -0,0 +1,32 @@ +Fixpoint exp (n : nat) (T : Set) + := match n with + | 0 => T + | S n' => exp n' (T * T) + end. +Definition big := Eval compute in exp 13 nat. +Module NonPrim. + Unset Primitive Projections. + Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }. + Definition x : sigT (fun x => x). + Proof. + exists big; admit. + Defined. + Goal True. + pose ((fun y => y = y) (projT1 _ x)) as y. + Time cbv beta in y. (* 0s *) + admit. + Defined. +End NonPrim. +Module Prim. + Set Primitive Projections. + Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }. + Definition x : sigT (fun x => x). + Proof. + exists big; admit. + Defined. + Goal True. + pose ((fun y => y = y) (projT1 _ x)) as y. + Timeout 1 cbv beta in y. (* takes around 2s. Grows with the value passed to [exp] above *) + admit. + Defined. +End Prim. \ No newline at end of file -- cgit v1.2.3 From e096b248265ebd6df17fdff18e3967dbd367edc5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 12 Feb 2015 23:24:51 +0100 Subject: Fixed test-suite file, that should always work. --- test-suite/bugs/closed/3881.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 test-suite/bugs/closed/3881.v diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v new file mode 100644 index 0000000000..7c3cc6b791 --- /dev/null +++ b/test-suite/bugs/closed/3881.v @@ -0,0 +1,35 @@ +(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *) +(* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *) +Generalizable All Variables. +Require Import Coq.Init.Notations. +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Axiom admit : forall {T}, T. +Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity). +Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *) +Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope. +Arguments eq_refl {_ _}. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end. +Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : forall x, f (equiv_inv x) = x }. +Arguments eisretr {A B} f {_} _. +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'"). +Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (g o f) | 1000 := admit. +Definition isequiv_homotopic {A B} (f : A -> B) (g : A -> B) `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g := admit. +Global Instance isequiv_inverse {A B} (f : A -> B) {feq : IsEquiv f} : IsEquiv f^-1 | 10000 := admit. +Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} `{IsEquiv A B f} `{IsEquiv A C (g o f)} : IsEquiv g. +Proof. + pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H + (fun b => ap g (eisretr f b))) as k. + revert k. + let x := match goal with |- let k := ?x in _ => constr:x end in + intro k; clear k; + pose (x _). + pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _ + (fun b => ap g (eisretr f b))). + Undo. + apply (@isequiv_homotopic _ _ ((g o f) o f^-1) g _ + (fun b => ap g (eisretr f b))). +Qed. + \ No newline at end of file -- cgit v1.2.3 From 7c9938cfbd0cf9093f90b0ee7b856105528c2a87 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 13 Feb 2015 00:53:44 +0100 Subject: Trying to fix bug #3930. Instead of setting the last modified part of the text to be the insert point, we register all modifications to the buffer between to user actions and take the last modified point to be the least offset of all those modifications. --- ide/session.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ide/session.ml b/ide/session.ml index 47b747dae7..dc79fa7905 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -133,6 +133,11 @@ let set_buffer_handlers try ignore(buffer#get_mark (`NAME "stop_of_input")) with GText.No_such_mark _ -> assert false in let get_insert () = buffer#get_iter_at_mark `INSERT in + let update_prev it = + let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in + if it#offset < prev#offset then + buffer#move_mark (`NAME "prev_insert") ~where:it + in let debug_edit_zone () = if false (*!Minilib.debug*) then begin buffer#remove_tag Tags.Script.edit_zone ~start:buffer#start_iter ~stop:buffer#end_iter; @@ -147,6 +152,7 @@ let set_buffer_handlers let insert_cb it s = if String.length s = 0 then () else begin Minilib.log ("insert_cb " ^ string_of_int it#offset); let text_mark = add_mark it in + let () = update_prev it in if it#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" else if it#has_tag Tags.Script.read_only then @@ -162,6 +168,7 @@ let set_buffer_handlers Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset); let min_iter, max_iter = if start#compare stop < 0 then start, stop else stop, start in + let () = update_prev min_iter in let text_mark = add_mark min_iter in let rec aux min_iter = if min_iter#equal max_iter then () -- cgit v1.2.3 From 8f73830d46d985906deadae3059db75772281516 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 13 Feb 2015 11:14:54 +0100 Subject: Selection of the current word in CoqIDE looks at all buffers. --- ide/coqide.ml | 15 ++++++++++++--- ide/wg_ProofView.ml | 4 ++++ ide/wg_ProofView.mli | 1 + 3 files changed, 17 insertions(+), 3 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index 1d76ceada4..5aac8f2a18 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -588,9 +588,18 @@ let get_current_word term = | Some p -> p | None -> (** Then look at the current selected word *) - if term.script#buffer#has_selection then - let (start, stop) = term.script#buffer#selection_bounds in - term.script#buffer#get_text ~slice:true ~start ~stop () + let buf1 = term.script#buffer in + let buf2 = term.proof#buffer in + let buf3 = term.messages#buffer in + if buf1#has_selection then + let (start, stop) = buf1#selection_bounds in + buf1#get_text ~slice:true ~start ~stop () + else if buf2#has_selection then + let (start, stop) = buf2#selection_bounds in + buf2#get_text ~slice:true ~start ~stop () + else if buf3#has_selection then + let (start, stop) = buf3#selection_bounds in + buf3#get_text ~slice:true ~start ~stop () (** Otherwise try to find the word around the cursor *) else let it = term.script#buffer#get_iter_at_mark `INSERT in diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 7e7a311ed0..a33f2c591c 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -9,6 +9,7 @@ class type proof_view = object inherit GObj.widget + method buffer : GText.buffer method refresh : unit -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit @@ -176,6 +177,7 @@ let proof_view () = ~highlight_matching_brackets:true ~tag_table:Tags.Proof.table () in + let text_buffer = new GText.buffer buffer#as_buffer in let view = GSourceView2.source_view ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD () in @@ -186,6 +188,8 @@ let proof_view () = val mutable goals = None val mutable evars = None + method buffer = text_buffer + method clear () = buffer#set_text "" method set_goals gls = goals <- gls diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index 1fbf9900ca..c5e042ea52 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -9,6 +9,7 @@ class type proof_view = object inherit GObj.widget + method buffer : GText.buffer method refresh : unit -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit -- cgit v1.2.3 From dc9b65741dae1b2bf58394e26c9155dad2bf7591 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 13 Feb 2015 11:30:54 +0100 Subject: Fix test-suite file to finish --- test-suite/bugs/closed/3309.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v index fcebdec728..9e12b990b7 100644 --- a/test-suite/bugs/closed/3309.v +++ b/test-suite/bugs/closed/3309.v @@ -315,12 +315,14 @@ Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) : hrel (@setq intros; exact (@quotrel _ _). Defined. +(* Unset Kernel Term Sharing. *) + Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit. Definition ispartlbinopabmonoidfracrel_type : Type := forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ), @abmonoidfracrel X A ( ( admit + z ) )admit. -Axiom ispartlbinopabmonoidfracrel : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in +Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in ispartlbinopabmonoidfracrel_type in exact t)$. -- cgit v1.2.3 From dcb23edad4debc0f4856580910cb5eba00077006 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 13 Feb 2015 14:36:18 +0100 Subject: Better error message for nested module application. Fixes #3809. --- toplevel/himsg.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 9341f2f70a..5429e6608d 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -879,7 +879,9 @@ let explain_label_already_declared l = str ("The label "^Label.to_string l^" is already declared.") let explain_application_to_not_path _ = - str "Application of modules is restricted to paths." + strbrk "A module cannot be applied to another module application or " ++ + strbrk "with-expression; you must give a name to the intermediate result " ++ + strbrk "module first." let explain_not_a_functor () = str "Application of a non-functor." -- cgit v1.2.3