diff options
| -rw-r--r-- | .travis.yml | 3 | ||||
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 13 | ||||
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | plugins/quote/quote.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | theories/Structures/DecidableType.v | 4 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 7 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 3 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 |
10 files changed, 20 insertions, 21 deletions
diff --git a/.travis.yml b/.travis.yml index adaae54872..5604551879 100644 --- a/.travis.yml +++ b/.travis.yml @@ -53,7 +53,6 @@ matrix: allow_failures: - env: TEST_TARGET="ci-geocoq" - - env: TEST_TARGET="ci-vst" # Full Coq test-suite with two compilers # [TODO: use yaml refs and avoid duplication for packages list] @@ -83,7 +82,7 @@ matrix: - imagemagick - env: - TEST_TARGET="test-suite" - - COMPILER="4.04.0" + - COMPILER="4.04.1" - CAMLP5_VER="6.17" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="lablgtk-extras hevea" @@ -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 diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index c2f52e23bc..0346c4a555 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1242,7 +1242,7 @@ This will automatically print the same trace as {\tt Info \num} at each tactic c The current value for the {\tt Info Level} option can be checked using the {\tt Test Info Level} command. -\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}} +\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}\optindex{Ltac Batch Debug}} The {\ltac} interpreter comes with a step-by-step debugger. The debugger can be activated using the command @@ -1273,6 +1273,17 @@ r $n$: & advance $n$ steps further\\ r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\ \end{tabular} +A non-interactive mode for the debugger is available via the command + +\begin{quote} +{\tt Set Ltac Batch Debug.} +\end{quote} + +This option has the effect of presenting a newline at every prompt, +when the debugger is on. The debug log thus created, which does not +require user input to generate when this option is set, can then be +run through external tools such as \texttt{diff}. + \subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}} It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug. diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 405d63dfe7..1162b6e153 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -915,7 +915,7 @@ let raw_cases_pattern_expr_loc = function | RCPatAtom (loc,_) -> loc | RCPatOr (loc,_) -> loc -(** {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 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} 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/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index f85222dfb4..d811f04ef6 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -86,7 +86,7 @@ Module KeyDecidableType(D:DecidableType). Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. - intros; apply InA_eqA with p; auto with *. + intros; apply InA_eqA with p; auto using eqk_equiv. Qed. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). @@ -109,7 +109,7 @@ Module KeyDecidableType(D:DecidableType). Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. 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 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 |