From ba88e99d37817cd3a591b14bbceb61e28f3e3382 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 27 Apr 2017 17:26:17 +0200 Subject: Aligning on standard layout of CHANGES. --- CHANGES | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index 8cb5573b21..69271f932e 100644 --- a/CHANGES +++ b/CHANGES @@ -17,13 +17,12 @@ Tactics Most notably, the new implementation recognizes Miller patterns that were missed before because of a missing normalization step. Hopefully this should be fairly uncommon. -- "auto with real" can now discharge comparisons of literals +- Tactic "auto with real" can now discharge comparisons of literals. - The types of variables in patterns of "match" are now beta-iota-reduced after type-checking. This has an impact on the type of the variables that the tactic "refine" introduces in the context, producing types a priori closer to the expectations. - Standard Library - New file PropExtensionality.v to explicitly work in the axiomatic -- cgit v1.2.3 From e3a3b4bb17c40b6af2ef8501c405f0600cc6d65b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 22 Apr 2017 21:09:05 +0200 Subject: Typo in a comment of plugin Quote. --- plugins/quote/quote.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index fc9d70ae7d..c649cfb2c6 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -8,7 +8,7 @@ (* The `Quote' tactic *) -(* The basic idea is to automatize the inversion of interpetation functions +(* The basic idea is to automatize the inversion of interpretation functions in 2-level approach Examples are given in \texttt{theories/DEMOS/DemoQuote.v} -- cgit v1.2.3 From e3550a0acc39e235e01a727267b12a7c06f23b2c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 26 Aug 2016 14:46:33 +0200 Subject: Uniformity of style for selecting plural or not; spacing for comma. --- tactics/class_tactics.ml | 2 +- vernac/obligations.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2d6dffdd23..05eb0a9760 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1202,7 +1202,7 @@ module Search = struct Feedback.msg_debug (pr_depth info.search_depth ++ str": no match for " ++ Printer.pr_econstr_env (Goal.env gl) s concl ++ - spc () ++ str ", " ++ int (List.length poss) ++ + str ", " ++ int (List.length poss) ++ str" possibilities"); match e with | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e0520216b2..5233fab151 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1088,7 +1088,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit Defined cst) else ( let len = Array.length obls in - let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in + let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with -- cgit v1.2.3 From a05cdcb00edbf0e35190f2d724c4a8c46d6cf9a3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 15 May 2017 03:00:04 +0200 Subject: Typo in comments of constrintern. --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3f99a3c7c0..b57a046796 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -900,7 +900,7 @@ let interp_reference vars r = (**********************************************************************) (** {5 Cases } *) -(** {6 Elemtary bricks } *) +(** {6 Elementary bricks } *) let apply_scope_env env = function | [] -> {env with tmp_scope = None}, [] | sc::scl -> {env with tmp_scope = sc}, scl -- cgit v1.2.3 From 9ddfdab6a4715a08a78296bf8824d086f358bdc0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 14 May 2017 11:14:43 +0200 Subject: Dead code in coqdep. Was introduced in 5268efdef, reverted then readded in 1be9c4d. --- tools/coqdep_common.ml | 7 ------- tools/coqdep_common.mli | 3 --- 2 files changed, 10 deletions(-) diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 0064aebdae..93b25e2ede 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -544,13 +544,6 @@ let add_rec_dir_no_import add_file phys_dir log_dir = let add_rec_dir_import add_file phys_dir log_dir = add_directory true (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 true (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 = add_directory false add_caml_known phys_dir [] diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 633c474ada..10da0240dd 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -64,8 +64,5 @@ val add_rec_dir_no_import : val add_rec_dir_import : (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 -- cgit v1.2.3