From fd47b2d2638518fe62ce9c63557d2dab219d9558 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 30 Jun 2016 19:41:53 +0200 Subject: Goal selectors now use the keyword [only]. This fixes some parsing problems when doing things like [let n := 2 in idtac n]. See bug #4877. --- ltac/g_ltac.ml4 | 14 ++++++++------ test-suite/bugs/closed/4877.v | 12 ++++++++++++ test-suite/success/goal_selector.v | 8 ++++---- 3 files changed, 24 insertions(+), 10 deletions(-) create mode 100644 test-suite/bugs/closed/4877.v diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index b5494a7cbb..fbeb89a634 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -45,7 +45,6 @@ let new_entry name = let e = Gram.entry_create name in e -let selector = new_entry "vernac:selector" let toplevel_selector = new_entry "vernac:toplevel_selector" let tacdef_body = new_entry "tactic:tacdef_body" @@ -79,7 +78,7 @@ let warn_deprecated_appcontext = GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg - tactic_mode constr_may_eval constr_eval selector toplevel_selector; + tactic_mode constr_may_eval constr_eval toplevel_selector; tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> @@ -316,13 +315,16 @@ GEXTEND Gram l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ] ; + selector_body: + [ [ l = range_selector_or_nth -> l + | test_bracket_ident; "["; id = ident; "]" -> SelectId id ] ] + ; selector: - [ [ l = range_selector_or_nth; ":" -> l - | IDENT "all" ; ":" -> SelectAll ] ] + [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ] ; toplevel_selector: - [ [ s = selector -> s - | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id ] ] + [ [ sel = selector_body; ":" -> sel + | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ] diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v new file mode 100644 index 0000000000..7e3c78dc2e --- /dev/null +++ b/test-suite/bugs/closed/4877.v @@ -0,0 +1,12 @@ +Ltac induction_last := + let v := match goal with + | |- forall x y, _ = _ -> _ => 1 + | |- forall x y, _ -> _ = _ -> _ => 2 + | |- forall x y, _ -> _ -> _ = _ -> _ => 3 + end in + induction v. + +Goal forall n m : nat, True -> n = m -> m = n. + induction_last. + reflexivity. +Qed. \ No newline at end of file diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 91fb54d9a1..8681405175 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -34,7 +34,7 @@ Qed. Goal True -> True. Proof. - intros y; 1-2 : repeat idtac. + intros y; only 1-2 : repeat idtac. 1-1:match goal with y : _ |- _ => let x := y in idtac x end. Fail 1-1:let x := y in idtac x. 1:let x := y in idtac x. @@ -44,12 +44,12 @@ Qed. Goal True /\ (True /\ True). Proof. dup. - - split; 2: (split; exact I). + - split; only 2: (split; exact I). exact I. - - split; 2: split; exact I. + - split; only 2: split; exact I. Qed. Goal True -> exists (x : Prop), x. Proof. - intro H; eexists ?[x]. [x]: exact True. 1: assumption. + intro H; eexists ?[x]; only [x]: exact True. 1: assumption. Qed. -- cgit v1.2.3 From 4b61c0693d453dd0026792185354d68ba1db9022 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 30 Jun 2016 19:42:55 +0200 Subject: Update the documentation for goal selectors. --- doc/refman/RefMan-ltac.tex | 26 ++++++++++++++++++-------- doc/refman/RefMan-tac.tex | 8 ++++---- 2 files changed, 22 insertions(+), 12 deletions(-) diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 5ba3c308a6..0433a0f2e4 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -26,6 +26,7 @@ problems. \def\tacarg{\nterm{tacarg}} \def\cpattern{\nterm{cpattern}} \def\selector{\textrm{\textsl{selector}}} +\def\toplevelselector{\textrm{\textsl{toplevel\_selector}}} The syntax of the tactic language is given Figures~\ref{ltac} and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of @@ -105,7 +106,7 @@ is understood as & | & {\tt exactly\_once} {\tacexprpref}\\ & | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ & | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\ -& | & {\selector} {\tt :} {\tacexprpref}\\ +& | & {\tt only} {\selector} {\tt :} {\tacexprpref}\\ & | & {\tacexprinf} \\ \\ {\tacexprinf} & ::= & @@ -209,11 +210,14 @@ is understood as \\ \selector & ::= & [{\ident}]\\ -& $|$ & {\tt all}\\ -& $|$ & {\tt par}\\ & $|$ & {\integer}\\ & $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}} - {\tt ,} + {\tt ,}\\ +\\ +\toplevelselector & ::= & + \selector\\ +& $|$ & {\tt all}\\ +& $|$ & {\tt par} \end{tabular} \end{centerframe} \caption{Syntax of the tactic language (continued)} @@ -374,7 +378,12 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$. We can restrict the application of a tactic to a subset of the currently focused goals with: \begin{quote} -{\selector} {\tt :} {\tacexpr} + {\toplevelselector} {\tt :} {\tacexpr} +\end{quote} +We can also use selectors as a tactical, which allows to use them nested in +a tactic expression, by using the keyword {\tt only}: +\begin{quote} + {\tt only} {\selector} {\tt :} {\tacexpr} \end{quote} When selecting several goals, the tactic {\tacexpr} is applied globally to all selected goals. @@ -396,11 +405,12 @@ all selected goals. of goals described by the given ranges. You can write a single $n$ as a shortcut for $n$-$n$ when specifying multiple ranges. - \item {\tt all: } {\tacexpr} + \item {\tt all:} {\tacexpr} In this variant, {\tacexpr} is applied to all focused goals. + {\tt all:} can only be used at the toplevel of a tactic expression. - \item {\tt par: } {\tacexpr} + \item {\tt par:} {\tacexpr} In this variant, {\tacexpr} is applied to all focused goals in parallel. The number of workers can be controlled via the @@ -409,7 +419,7 @@ all selected goals. on goals containing no existential variables and {\tacexpr} must either solve the goal completely or do nothing (i.e. it cannot make some progress). - {\tt par: } can only be used at the top level of a tactic expression. + {\tt par:} can only be used at the toplevel of a tactic expression. \end{Variants} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2d9cc12fd7..0e4435cf39 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -46,13 +46,13 @@ goal selector (see Section \ref{ltac:selector}). If no selector is specified, the default selector (see Section \ref{default-selector}) is used. -\newcommand{\selector}{\nterm{selector}} +\newcommand{\toplevelselector}{\nterm{toplevel\_selector}} \begin{tabular}{lcl} -{\commandtac} & ::= & {\selector} {\tt :} {\tac} {\tt .}\\ +{\commandtac} & ::= & {\toplevelselector} {\tt :} {\tac} {\tt .}\\ & $|$ & {\tac} {\tt .} \end{tabular} -\subsection[\tt Set Default Goal Selector ``\selector''.] - {\tt Set Default Goal Selector ``\selector''. +\subsection[\tt Set Default Goal Selector ``\toplevelselector''.] + {\tt Set Default Goal Selector ``\toplevelselector''. \optindex{Default Goal Selector} \label{default-selector}} After using this command, the default selector -- used when no selector -- cgit v1.2.3 From 411973d14a95b043f93ed6d0ca628a6a98e3c221 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 18 Aug 2016 22:32:59 +0200 Subject: [checker] Fix/fine tune printing. In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct access to the console, recommending instead to provide information to the user by means of the `Feedback.msg_*` facilities. However, we introduced a display bug in the checker printer as it is special and doesn't use the Pp facilities (likely for trust reasons), spotted by @herbelin This patch fixes this bug and performs a couple more of fine tunings in the input. However, it could be desirable to port the `checker/printer.ml` to `Pp` and use the feedback mechanism; this would allow IDEs to use the checker in a more convenient way, at the cost of trusting `Pp` (which is already a bit trusted currently) A start of that idea can be found at: https://github.com/ejgallego/coq/tree/fix_checker_printing --- checker/check.ml | 11 ++++++----- checker/check_stat.ml | 3 +-- checker/checker.ml | 5 ++++- checker/print.ml | 6 ++++-- 4 files changed, 15 insertions(+), 10 deletions(-) diff --git a/checker/check.ml b/checker/check.ml index 863cf7b2cd..8b299bf2a2 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -11,6 +11,8 @@ open CErrors open Util open Names +let chk_pp = Pp.pp_with Format.std_formatter + let pr_dirpath dp = str (DirPath.to_string dp) let default_root_prefix = DirPath.empty let split_dirpath d = @@ -118,7 +120,6 @@ let check_one_lib admit (dir,m) = (Flags.if_verbose Feedback.msg_notice (str "Checking library: " ++ pr_dirpath dir); Safe_typing.import file md m.library_extra_univs dig); - Flags.if_verbose Feedback.msg_notice (fnl()); register_loaded_library m (*************************************************************************) @@ -298,7 +299,7 @@ let name_clash_message dir mdir f = let depgraph = ref LibraryMap.empty let intern_from_file (dir, f) = - Flags.if_verbose Feedback.msg_notice(str"[intern "++str f++str" ..."); + Flags.if_verbose chk_pp (str"[intern "++str f++str" ..."); let (sd,md,table,opaque_csts,digest) = try let ch = System.with_magic_number_check raw_intern_library f in @@ -322,7 +323,7 @@ let intern_from_file (dir, f) = errorlabstrm "intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin - Feedback.msg_notice(str " (was a vio file) "); + chk_pp (str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then errorlabstrm "intern_from_file" (str "The file "++str f++str " is still a .vio")) @@ -333,12 +334,12 @@ let intern_from_file (dir, f) = Validate.validate !Flags.debug Values.v_libsum sd; Validate.validate !Flags.debug Values.v_lib md; Validate.validate !Flags.debug Values.v_opaques table; - Flags.if_verbose Feedback.msg_notice (str" done]"); + Flags.if_verbose chk_pp (str" done]" ++ fnl ()); let digest = if opaque_csts <> None then Cic.Dviovo (digest,udg) else (Cic.Dvo digest) in sd,md,table,opaque_csts,digest - with e -> Flags.if_verbose Feedback.msg_notice (str" failed!]"); raise e in + with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; opaque_tables := LibraryMap.add sd.md_name table !opaque_tables; Option.iter (fun (opaque_csts,_,_) -> diff --git a/checker/check_stat.ml b/checker/check_stat.ml index f196746a57..741f532848 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -57,8 +57,7 @@ let print_context env = (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_ax csts) ++ - fnl())); + str "* " ++ hov 0 (pr_ax csts))); end let stats () = diff --git a/checker/checker.ml b/checker/checker.ml index 0c411ae44d..a7c45b8247 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -16,6 +16,8 @@ open Check let () = at_exit flush_all +let chk_pp = Pp.pp_with Format.std_formatter + let fatal_error info anomaly = flush_all (); Feedback.msg_error info; flush_all (); exit (if anomaly then 129 else 1) @@ -282,7 +284,8 @@ let rec explain_exn = function Format.printf "@\nis not convertible with@\n"; Print.print_pure_constr a; Format.printf "@\n====== universes ====@\n"; - Feedback.msg_notice (Univ.pr_universes + chk_pp + (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" diff --git a/checker/print.ml b/checker/print.ml index c0d1ac3688..7ef752b002 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -10,7 +10,9 @@ open Format open Cic open Names -let print_instance i = Feedback.msg_notice (Univ.Instance.pr i) +let chk_pp = Pp.pp_with Format.std_formatter + +let print_instance i = chk_pp (Univ.Instance.pr i) let print_pure_constr csr = let rec term_display c = match c with @@ -108,7 +110,7 @@ let print_pure_constr csr = and sort_display = function | Prop(Pos) -> print_string "Set" | Prop(Null) -> print_string "Prop" - | Type u -> print_string "Type("; Feedback.msg_notice (Univ.pr_uni u); print_string ")" + | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")" and name_display = function | Name id -> print_string (Id.to_string id) -- cgit v1.2.3 From b0a79d8c37267d2ba950dafb7094374910214eb3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 16 Sep 2016 12:16:52 -0700 Subject: Doc: [Reset Ltac Profile] is not synchronized --- doc/refman/RefMan-ltac.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 1d89c17f47..822f8a2227 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1279,7 +1279,7 @@ Prints a profile for all tactics that start with {\qstring}. Append a period (.) \begin{quote} {\tt Reset Ltac Profile}. \end{quote} -Resets the profile, that is, deletes all accumulated information +Resets the profile, that is, deletes all accumulated information. Note that backtracking across a {\tt Reset Ltac Profile} will not restore the information. \begin{coq_eval} Reset Initial. -- cgit v1.2.3 From 2008e95eb33ccfdd191afc0d3f692772c077b7a4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 17 Sep 2016 13:05:11 -0700 Subject: Fix indentation of -profile-ltac in -help --- toplevel/usage.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8f77aea440..de41f7b190 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -82,7 +82,7 @@ let print_usage_channel co command = \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ \n -time display the time taken by each command\ -\n -profile-ltac display the time taken by each (sub)tactic\ +\n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ -- cgit v1.2.3 From 4e93587fd83bab4ad5c158aa6b3c194e8a7a5551 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 27 Sep 2016 15:21:37 +0200 Subject: Fixing #4887 (confusion between using and with in documentation of firstorder). --- doc/refman/RefMan-tac.tex | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fa595d9159..5eb8cedd95 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4343,22 +4343,23 @@ vernacular command and printed using {\nobreak {\tt Print Firstorder Tries to solve the goal with {\tac} when no logical rule may apply. - \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ } - \tacindex{firstorder with} - - Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search - environment. - \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ } \tacindex{firstorder using} - Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$ - to the proof-search environment. If {\qualid}$_i$ refers to an inductive - type, it is the collection of its constructors which is added as hints. + Adds lemmas {\qualid}$_1$ \dots\ {\qualid}$_n$ to the proof-search + environment. If {\qualid}$_i$ refers to an inductive type, it is + the collection of its constructors which are added to the + proof-search environment. -\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$} + \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ } + \tacindex{firstorder with} - This combines the effects of the {\tt using} and {\tt with} options. + Adds lemmas from {\tt auto} hint bases \ident$_1$ \dots\ \ident$_n$ + to the proof-search environment. + +\item \texttt{firstorder {\tac} using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$} + + This combines the effects of the different variants of \texttt{firstorder}. \end{Variants} -- cgit v1.2.3 From 751fa3aa8aed28946b45d8932514913c86ce8f5a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 27 Sep 2016 15:26:37 +0200 Subject: Add fixed test-suite file for bug #4527 --- test-suite/bugs/closed/4527.v | 267 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 267 insertions(+) create mode 100644 test-suite/bugs/closed/4527.v diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v new file mode 100644 index 0000000000..4ca6fe78cd --- /dev/null +++ b/test-suite/bugs/closed/4527.v @@ -0,0 +1,267 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) +(* File reduced by coq-bug-finder from original input, then from 1199 lines to +430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, +then from 269 lines to 255 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml +4.01.0 + coqtop version 8.5 (January 2016) *) +Inductive False := . +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Init.Datatypes. + +Import Coq.Init.Notations. + +Global Set Universe Polymorphism. + +Notation "A -> B" := (forall (_ : A), B) : type_scope. + +Inductive True : Type := + I : True. +Module Export Datatypes. + +Set Implicit Arguments. +Notation nat := Coq.Init.Datatypes.nat. +Notation S := Coq.Init.Datatypes.S. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. + +Notation "x * y" := (prod x y) : type_scope. + +Open Scope nat_scope. + +End Datatypes. +Module Export Specif. + +Set Implicit Arguments. + +Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P +proj1_sig }. + +Notation sigT := sig (only parsing). + +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. + +Notation projT1 := proj1_sig (only parsing). +Notation projT2 := proj2_sig (only parsing). + +End Specif. +Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in +Type@{i}. + +Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in + let ge := ((fun x => x) : Type1@{j} -> +Type@{i}) in Type@{i}. + +Notation idmap := (fun x => x). +Delimit Scope function_scope with function. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Open Scope fibration_scope. +Open Scope function_scope. + +Notation pr1 := projT1. +Notation pr2 := projT2. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left +associativity) : function_scope. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope. + +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : +type_scope. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. + +Arguments eisretr {A B}%type_scope f%function_scope {_} _. +Arguments eissect {A B}%type_scope f%function_scope {_} _. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : +function_scope. + +Inductive Unit : Type1 := + tt : Unit. + +Local Open Scope path_scope. + +Section EquivInverse. + + Context {A B : Type} (f : A -> B) {feq : IsEquiv f}. + + Theorem other_adj (b : B) : eissect f (f^-1 b) = ap f^-1 (eisretr f b). +admit. +Defined. + + Global Instance isequiv_inverse : IsEquiv f^-1 | 10000 + := BuildIsEquiv B A f^-1 f (eissect f) (eisretr f) other_adj. +End EquivInverse. + +Section Adjointify. + + Context {A B : Type} (f : A -> B) (g : B -> A). + Context (isretr : Sect g f) (issect : Sect f g). + + Let issect' := fun x => + ap g (ap f (issect x)^) @ ap g (isretr (f x)) @ issect x. + + Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a). +admit. +Defined. + + Definition isequiv_adjointify : IsEquiv f + := BuildIsEquiv A B f g isretr issect' is_adjoint'. + +End Adjointify. + + Definition ExtensionAlong {A B : Type} (f : A -> B) + (P : B -> Type) (d : forall x:A, P (f x)) + := { s : forall y:B, P y & forall x:A, s (f x) = d x }. + + Fixpoint ExtendableAlong@{i j k l} + (n : nat) {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := match n with + | 0 => Unit@{l} + | S n => (forall (g : forall a, C (f a)), + ExtensionAlong@{i j k l l} f C g) * + forall (h k : forall b, C b), + ExtendableAlong n f (fun b => h b = k b) + end. + + Definition ooExtendableAlong@{i j k l} + {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := forall n, ExtendableAlong@{i j k l} n f C. + +Module Type ReflectiveSubuniverses. + + Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + + let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In@{u a j} O U. + + Parameter extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : +Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). + +End ReflectiveSubuniverses. + +Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). +Export Os. + +Existing Class In. + + Coercion O_reflector : ReflectiveSubuniverse >-> Funclass. + +Arguments inO_equiv_inO {O} T {U} {_} f {_}. +Global Existing Instance O_inO. + +Section ORecursion. + Context {O : ReflectiveSubuniverse}. + + Definition O_indpaths {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o to O P == h o to O P) + : g == h + := (fst (snd (extendable_to_O O 2) g h) p).1. + + Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) + : O_indpaths g h p (to O P x) = p x + := (fst (snd (extendable_to_O O 2) g h) p).2 x. + +End ORecursion. + +Section Reflective_Subuniverse. + Universes Ou Oa. + Context (O : ReflectiveSubuniverse@{Ou Oa}). + + Definition inO_isequiv_to_O (T:Type) + : IsEquiv (to O T) -> In O T + := fun _ => inO_equiv_inO (O T) (to O T)^-1. + + Definition inO_to_O_retract (T:Type) (mu : O T -> T) + : Sect (to O T) mu -> In O T. + Proof. + unfold Sect; intros H. + apply inO_isequiv_to_O. + apply isequiv_adjointify with (g:=mu). + - + refine (O_indpaths (to O T o mu) idmap _). + intros x; exact (ap (to O T) (H x)). + - + exact H. + Defined. + + Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : +S) : In@{Ou Oa i} O (x=y). + Proof. + simple refine (inO_to_O_retract@{i j} _ _ _); intro u. + - + assert (p : (fun _ : O (x=y) => x) == (fun _=> y)). + { + refine (O_indpaths _ _ _); simpl. + intro v; exact v. +} + exact (p u). + - + hnf. + rewrite O_indpaths_beta; reflexivity. + Qed. + Check inO_paths@{Type Type}. -- cgit v1.2.3 From e8b9ee76af721c32b2d5cfcdae4ecbf47b341545 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 27 Sep 2016 17:16:39 +0200 Subject: Fix #5061: Warnings flag has no discernible value The default value of the warnings flag was printed as an empty string, now replaced by "default". --- lib/cWarnings.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 78fa84f333..720f54606c 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -21,7 +21,7 @@ let warnings : (string, t) Hashtbl.t = Hashtbl.create 97 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97 let current_loc = ref Loc.ghost -let flags = ref "" +let flags = ref "default" let set_current_loc = (:=) current_loc -- cgit v1.2.3 From 72c1fefcfb3f0dff02005034685f6b58ff84b3cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 27 Sep 2016 18:28:48 +0200 Subject: Fix bug #4553: CoqIDE gives warnings about deprecated GTK features. --- ide/coqide.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index d1a799a773..450bfcdfb1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -937,7 +937,6 @@ let emit_to_focus window sgn = let build_ui () = let w = GWindow.window ~wm_class:"CoqIde" ~wm_name:"CoqIde" - ~allow_grow:true ~allow_shrink:true ~width:window_width#get ~height:window_height#get ~title:"CoqIde" () in -- cgit v1.2.3 From 405acea72a67c31ec8554c1f76d51518a5df769a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 Sep 2016 15:38:33 +0200 Subject: Remove incorrect assertion in cbn (bug #4822). This assertion checked that two arguments in the same position were equal, but in fact, since one might have already been reduced, they are only convertible (which is too costly to check in an assertion). --- pretyping/reductionops.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4ccbc81b47..332d4e0b26 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -166,9 +166,6 @@ module Cst_stack = struct let empty = [] let is_empty = CList.is_empty - let sanity x y = - assert(Term.eq_constr x y) - let drop_useless = function | _ :: ((_,_,[])::_ as q) -> q | l -> l @@ -177,9 +174,9 @@ module Cst_stack = struct let append2cst = function | (c,params,[]) -> (c, h::params, []) | (c,params,((i,t)::q)) when i = pred (Array.length t) -> - let () = sanity h t.(i) in (c, params, q) + (c, params, q) | (c,params,(i,t)::q) -> - let () = sanity h t.(i) in (c, params, (succ i,t)::q) + (c, params, (succ i,t)::q) in drop_useless (List.map append2cst cst_l) -- cgit v1.2.3 From 8e0f29cb69f06b64d74b18b09fb6a717034f1140 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 22 Aug 2016 08:32:59 +0200 Subject: Typeclass backtracking example by J. Leivant --- test-suite/success/bteauto.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 590f6e191f..bb1cf06541 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -46,6 +46,25 @@ Module Backtracking. Qed. Unset Typeclasses Debug. + + Module Leivant. + Axiom A : Type. + Existing Class A. + Axioms a b c d e: A. + + Ltac get_value H := eval cbv delta [H] in H. + + Goal True. + Fail refine (let H := _ : A in _); let v := get_value H in idtac v; fail. + Admitted. + + Goal exists x:A, x=a. + unshelve evar (t : A). all:cycle 1. + refine (@ex_intro _ _ t _). + all:cycle 1. + all:(typeclasses eauto + reflexivity). + Qed. + End Leivant. End Backtracking. -- cgit v1.2.3 From dfadb394640b3d09eb6134b73d0f3e931bd70af1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 28 Sep 2016 15:29:58 +0200 Subject: Warning about similar notations now up to alpha-conversion. This allows to define on purpose the very same notation in different files, as currently the notations for *, +, - in Nat.v and Peano.v (with the first one using variables n and m and the second one using the default variables used by Infix, namely x and y). This makes also the "notation-overridden" warning less enigmatic facing two notations which are the same up to the choice of names. --- interp/notation.ml | 8 +++----- interp/notation_ops.ml | 50 ++++++++++++++++++++++++------------------------- interp/notation_ops.mli | 2 +- 3 files changed, 29 insertions(+), 31 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index 0798d385d4..d301ed21db 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -553,15 +553,13 @@ let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false - -let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) = - Id.equal id1 id2 && +let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) = pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && ntpe_eq tp1 tp2 let interpretation_eq (vars1, t1) (vars2, t2) = - List.equal vars_eq vars1 vars2 && - Notation_ops.eq_notation_constr t1 t2 + List.equal var_attributes_eq vars1 vars2 && + Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2 let exists_notation_in_scope scopt ntn r = let scope = match scopt with Some s -> s | None -> default_scope in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 1f29a2948f..cc81a00919 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -47,62 +47,62 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GHole _ | GSort _ | GLetIn _), _ -> false -let rec eq_notation_constr t1 t2 = match t1, t2 with +let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NRef gr1, NRef gr2 -> eq_gr gr1 gr2 -| NVar id1, NVar id2 -> Id.equal id1 id2 +| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2) | NApp (t1, a1), NApp (t2, a2) -> - eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2 + (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2 | NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) | NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> - Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 && b1 == b2 + Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 && b1 == b2 | NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 | NProd (na1, t1, u1), NProd (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 | NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> - Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 + Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 | NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) let eqpat (p1, t1) (p2, t2) = List.equal cases_pattern_eq p1 p2 && - eq_notation_constr t1 t2 + (eq_notation_constr vars) t1 t2 in let eqf (t1, (na1, o1)) (t2, (na2, o2)) = let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in - eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 + (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 in - Option.equal eq_notation_constr o1 o2 && + Option.equal (eq_notation_constr vars) o1 o2 && List.equal eqf r1 r2 && List.equal eqpat p1 p2 | NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> List.equal Name.equal nas1 nas2 && Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 | NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> - eq_notation_constr t1 t2 && + (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr u1 u2 && - eq_notation_constr r1 r2 + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) u1 u2 && + (eq_notation_constr vars) r1 r2 | NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) let eq (na1, o1, t1) (na2, o2, t2) = Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr t1 t2 + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) t1 t2 in Array.equal Id.equal ids1 ids2 && Array.equal (List.equal eq) ts1 ts2 && - Array.equal eq_notation_constr us1 us2 && - Array.equal eq_notation_constr rs1 rs2 + Array.equal (eq_notation_constr vars) us1 us2 && + Array.equal (eq_notation_constr vars) rs1 rs2 | NSort s1, NSort s2 -> Miscops.glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> - eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2 + (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ | NRec _ | NSort _ | NCast _), _ -> false diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 854e222e30..4ebd3ddd80 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -12,7 +12,7 @@ open Glob_term (** {5 Utilities about [notation_constr]} *) -val eq_notation_constr : notation_constr -> notation_constr -> bool +val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool (** Substitution of kernel names in interpretation data *) -- cgit v1.2.3 From 9b1c4576d89014d686bc10f13455a52de8d793bf Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 28 Sep 2016 16:46:32 +0200 Subject: Make error message more helpful. CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.--- ide/ide_slave.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 1f933fb8a5..239fc587ce 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -98,7 +98,7 @@ let coqide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then - msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + msg_warning (strbrk"This will not work. Use CoqIDE view menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then msg_warning (strbrk "Rather use CoqIDE navigation instead"); if is_query ast then -- cgit v1.2.3 From d907342e31930eb2b8af7c9cc12bd0ddc7c00709 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 Sep 2016 17:00:09 +0200 Subject: Do not stop propagation of signals when Coq is busy (bug #3941). When inserting a character in an already processed buffer, a message is sent to Coq so that the proof is backtracked and the character is inserted. If a second character is inserted while Coq is still busy with the first message, the action is canceled, but the signal is no longer dropped so that the second character is properly inserted. --- ide/session.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/ide/session.ml b/ide/session.ml index e998337604..fc6340d283 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -108,10 +108,10 @@ let set_buffer_handlers let id = ref 0 in fun () -> incr id; !id in let running_action = ref None in - let cancel_signal reason = + let cancel_signal ?(stop_emit=true) reason = Minilib.log ("user_action cancelled: "^reason); action_was_cancelled := true; - GtkSignal.stop_emit () in + if stop_emit then GtkSignal.stop_emit () in let del_mark () = try buffer#delete_mark (`NAME "target") with GText.No_such_mark _ -> () in @@ -124,7 +124,7 @@ let set_buffer_handlers fun () -> (* If Coq is busy due to the current action, we don't cancel *) match !running_action with | Some aid when aid = action -> () - | _ -> cancel_signal "Coq busy" in + | _ -> cancel_signal ~stop_emit:false "Coq busy" in Coq.try_grab coqtop action fallback in let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in -- cgit v1.2.3 From 875f235dd0413faa34f7d46afc25d2eb90e386e5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Sep 2016 17:01:26 +0200 Subject: Fix bug #4723 and FIXME in API for solve_by_tac This avoids leakage of universes. Also makes Program Lemma/Fact work again, it tries to solve the remaining evars using the obligation tactic. --- pretyping/pretyping.ml | 6 ++++-- pretyping/pretyping.mli | 4 +++- proofs/pfedit.ml | 10 ++++++---- proofs/pfedit.mli | 6 +++--- stm/lemmas.ml | 6 ++++-- stm/lemmas.mli | 4 +++- test-suite/bugs/closed/4723.v | 28 ++++++++++++++++++++++++++++ toplevel/vernacentries.ml | 22 +++++++++++++++++++++- 8 files changed, 72 insertions(+), 14 deletions(-) create mode 100644 test-suite/bugs/closed/4723.v diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 46f0219f91..48bf9149d0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -239,10 +239,12 @@ let interp_elimination_sort = function | GSet -> InSet | GType _ -> InType +type inference_hook = env -> evar_map -> evar -> evar_map * constr + type inference_flags = { use_typeclasses : bool; use_unif_heuristics : bool; - use_hook : (env -> evar_map -> evar -> constr) option; + use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } @@ -272,7 +274,7 @@ let apply_inference_hook hook evdref pending = if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then try - let c = hook sigma evk in + let sigma, c = hook sigma evk in Evd.define evk c sigma with Exit -> sigma diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 824bb11aa4..eead48a549 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -47,10 +47,12 @@ val empty_lvar : ltac_var_map type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr +type inference_hook = env -> evar_map -> evar -> evar_map * constr + type inference_flags = { use_typeclasses : bool; use_unif_heuristics : bool; - use_hook : (env -> evar_map -> evar -> constr) option; + use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e4bae20128..a3ece19134 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -161,11 +161,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in - let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in + let ce, status, univs = + build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with @@ -232,8 +233,9 @@ let solve_by_implicit_tactic env sigma evk = (try let c = Evarutil.nf_evars_universes sigma evi.evar_concl in if Evarutil.has_undefined_evars sigma c then raise Exit; - let (ans, _, _) = + let (ans, _, ctx) = build_by_tactic env (Evd.evar_universe_context sigma) c tac in - ans + let sigma = Evd.set_universe_context sigma ctx in + sigma, ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 666730e1af..ea604e08eb 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -167,7 +167,8 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> types -> unit Proofview.tactic -> - Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context + Safe_typing.private_constants Entries.definition_entry * bool * + Evd.evar_universe_context val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> @@ -189,5 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) -(* FIXME: interface: it may incur some new universes etc... *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr +val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 50f2b82c3b..bf10b91339 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = call_hook (fun exn -> exn) hook strength ref) thms_data in start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard -let start_proof_com kind thms hook = +let start_proof_com use_hook kind thms hook = let env0 = Global.env () in let levels = Option.map snd (fst (List.hd thms)) in let evdref = ref (match levels with @@ -459,7 +459,9 @@ let start_proof_com kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); + let flags = all_and_fail_flags in + let flags = { flags with use_hook } in + evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/stm/lemmas.mli b/stm/lemmas.mli index f751598f04..904cdeef4d 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -33,7 +33,9 @@ val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_ma ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit -val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> +val start_proof_com : + Pretyping.inference_hook option -> + goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit val start_proof_with_initialization : diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v new file mode 100644 index 0000000000..8884812102 --- /dev/null +++ b/test-suite/bugs/closed/4723.v @@ -0,0 +1,28 @@ + +Require Coq.Program.Tactics. + +Record Matrix (m n : nat). + +Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q): + Matrix (m*p) (n*q). Admitted. + +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Ltac Obligation Tactic := admit. +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Axiom cheat : forall {A}, A. +Obligation Tactic := apply cheat. + +Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. +admit. +Admitted. \ No newline at end of file diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 48a85b709f..6723a8b489 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -448,7 +448,27 @@ let vernac_notation locality local = (***********) (* Gallina *) -let start_proof_and_print k l hook = start_proof_com k l hook +let start_proof_and_print k l hook = + let use_hook = + if Flags.is_program_mode () then + let hook env sigma ev = + let tac = !Obligations.default_tactic in + let evi = Evd.find sigma ev in + let env = Evd.evar_filtered_env evi in + try + let concl = Evarutil.nf_evars_universes sigma evi.Evd.evar_concl in + if Evarutil.has_undefined_evars sigma concl then raise Exit; + let c, _, ctx = + Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) + concl (Tacticals.New.tclCOMPLETE tac) + in Evd.set_universe_context sigma ctx, c + with Logic_monad.TacticFailure e when Logic.catchable_exception e -> + error "The statement obligations could not be resolved \ + automatically, write a statement definition first." + in Some hook + else None + in + start_proof_com use_hook k l hook let no_hook = Lemmas.mk_hook (fun _ _ -> ()) -- cgit v1.2.3 From 6a5f10f725a1e10a88df404574331c9f679bc474 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 28 Sep 2016 16:37:52 +0200 Subject: Adding interface files to Nsatz ML files. --- plugins/nsatz/ideal.ml | 69 ------------------------------------------------- plugins/nsatz/ideal.mli | 47 +++++++++++++++++++++++++++++++++ plugins/nsatz/nsatz.mli | 9 +++++++ 3 files changed, 56 insertions(+), 69 deletions(-) create mode 100644 plugins/nsatz/ideal.mli create mode 100644 plugins/nsatz/nsatz.mli diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 7c2178222f..48bdad8264 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -19,75 +19,6 @@ open Utile exception NotInIdeal -module type S = sig - -(* Monomials *) -type mon = int array - -val mult_mon : mon -> mon -> mon -val deg : mon -> int -val compare_mon : mon -> mon -> int -val div_mon : mon -> mon -> mon -val div_mon_test : mon -> mon -> bool -val ppcm_mon : mon -> mon -> mon - -(* Polynomials *) - -type deg = int -type coef -type poly -type polynom - -val repr : poly -> (coef * mon) list -val polconst : coef -> poly -val zeroP : poly -val gen : int -> poly - -val equal : poly -> poly -> bool -val name_var : string list ref -val getvar : string list -> int -> string -val lstringP : poly list -> string -val printP : poly -> unit -val lprintP : poly list -> unit - -val div_pol_coef : poly -> coef -> poly -val plusP : poly -> poly -> poly -val mult_t_pol : coef -> mon -> poly -> poly -val selectdiv : mon -> poly list -> poly -val oppP : poly -> poly -val emultP : coef -> poly -> poly -val multP : poly -> poly -> poly -val puisP : poly -> int -> poly -val contentP : poly -> coef -val contentPlist : poly list -> coef -val pgcdpos : coef -> coef -> coef -val div_pol : poly -> poly -> coef -> coef -> mon -> poly -val reduce2 : poly -> poly list -> coef * poly - -val poldepcontent : coef list ref -val coefpoldep_find : poly -> poly -> poly -val coefpoldep_set : poly -> poly -> poly -> unit -val initcoefpoldep : poly list -> unit -val reduce2_trace : poly -> poly list -> poly list -> poly list * poly -val spol : poly -> poly -> poly -val etrangers : poly -> poly -> bool -val div_ppcm : poly -> poly -> poly -> bool - -val genPcPf : poly -> poly list -> poly list -> poly list -val genOCPf : poly list -> poly list - -val is_homogeneous : poly -> bool - -type certificate = - { coef : coef; power : int; - gb_comb : poly list list; last_comb : poly list } - -val test_dans_ideal : poly -> poly list -> poly list -> - poly list * poly * certificate -val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate - -end - (*********************************************************************** Global options *) diff --git a/plugins/nsatz/ideal.mli b/plugins/nsatz/ideal.mli new file mode 100644 index 0000000000..d1a2a0a7d1 --- /dev/null +++ b/plugins/nsatz/ideal.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (coef * int array) list +val polconst : int -> coef -> poly +val zeroP : poly +val gen : int -> int -> poly + +val equal : poly -> poly -> bool +val name_var : string list ref + +val plusP : poly -> poly -> poly +val oppP : poly -> poly +val multP : poly -> poly -> poly +val puisP : poly -> int -> poly + +val poldepcontent : coef list ref + +type certificate = + { coef : coef; power : int; + gb_comb : poly list list; last_comb : poly list } + +val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate + +module Hashpol : Hashtbl.S with type key = poly + +val sugar_flag : bool ref +val divide_rem_with_critical_pair : bool ref + +end + +exception NotInIdeal + +val lexico : bool ref diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli new file mode 100644 index 0000000000..e876ccfa5d --- /dev/null +++ b/plugins/nsatz/nsatz.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit Proofview.tactic -- cgit v1.2.3 From 1c3bc5642fe29855cc4d72aa677ff7ffd4787271 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 28 Sep 2016 17:30:26 +0200 Subject: ZDivEucl: notations in different scope to avoid a warning --- theories/Numbers/Integer/Abstract/ZDivEucl.v | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 278e1bcffa..c2fa69e535 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -30,18 +30,23 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. We just ignore them here. *) -Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A). - Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b. +Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod A). + Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= B.modulo a b < abs b. End EuclidSpec. Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z. -Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z. Module ZEuclidProp (Import A : ZAxiomsSig') (Import B : ZMulOrderProp A) (Import C : ZSgnAbsProp A B) - (Import D : ZEuclid' A). + (Import D : ZEuclid A). + + (** We put notations in a scope, to avoid warnings about + redefinitions of notations *) + Infix "/" := D.div : euclid. + Infix "mod" := D.modulo : euclid. + Local Open Scope euclid. Module Import Private_NZDiv := Nop <+ NZDivProp A D B. @@ -615,4 +620,3 @@ intros (c,Hc). rewrite Hc. now apply mod_mul. Qed. End ZEuclidProp. - -- cgit v1.2.3 From ed53e048fc5e4b995c1e0c42bf1ba1611c331cce Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 28 Sep 2016 17:49:41 +0200 Subject: Ring_theory: avoid overriding a few notations --- plugins/setoid_ring/Ring_theory.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 7fcd6c08a7..f7757a18da 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -238,7 +238,6 @@ Section ALMOST_RING. Variable req : R -> R -> Prop. Notation "0" := rO. Notation "1" := rI. Infix "==" := req. Infix "+" := radd. Infix "* " := rmul. - Infix "-" := rsub. Notation "- x" := (ropp x). (** Leibniz equality leads to a setoid theory and is extensional*) Lemma Eqsth : Equivalence (@eq R). @@ -263,7 +262,7 @@ Section ALMOST_RING. -x = x and x - y = x + y *) Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). - Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). + Definition SRsub x y := x + -y. Infix "-" := SRsub. Lemma SRopp_ext : forall x y, x == y -> -x == -y. Proof. intros x y H; exact H. Qed. @@ -320,6 +319,8 @@ Section ALMOST_RING. Qed. End SEMI_RING. + Infix "-" := rsub. + Notation "- x" := (ropp x). Variable Reqe : ring_eq_ext radd rmul ropp req. Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. -- cgit v1.2.3 From e1df1b77f8c72636b6e347f41f6f38976c86e909 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Sep 2016 16:32:42 +0200 Subject: -profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100) With this command line flag one can profile ltac in files /and/ trim the results without actually touching the files. --- lib/flags.ml | 1 + lib/flags.mli | 1 + ltac/profile_ltac.ml | 4 ++-- ltac/profile_ltac_tactics.ml4 | 2 +- toplevel/coqtop.ml | 1 + 5 files changed, 6 insertions(+), 3 deletions(-) diff --git a/lib/flags.ml b/lib/flags.ml index 13525165ab..d29064c97f 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -226,6 +226,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false +let profile_ltac_cutoff = ref 0.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 8fe64d24fa..839c252cbb 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -149,6 +149,7 @@ val tactic_context_compat : bool ref context vs. appcontext) is set. *) val profile_ltac : bool ref +val profile_ltac_cutoff : float ref (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 102918e5e5..a91ff98fb9 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -401,11 +401,11 @@ let print_results ~cutoff = print_results_filter ~cutoff ~filter:(fun _ -> true) let print_results_tactic tactic = - print_results_filter ~cutoff:0.0 ~filter:(fun s -> + print_results_filter ~cutoff:!Flags.profile_ltac_cutoff ~filter:(fun s -> String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic))))) let do_print_results_at_close () = - if get_profiling () then print_results ~cutoff:0.0 + if get_profiling () then print_results ~cutoff:!Flags.profile_ltac_cutoff let _ = Declaremods.append_end_library_hook do_print_results_at_close diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index 9083bda60a..8cb76d81c5 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -31,7 +31,7 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY -| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ] +| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ] | [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] END diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ee331e37c7..47d433d790 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -523,6 +523,7 @@ let parse_args arglist = |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) |"-outputstate" -> set_outputstate (next ()) |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 + |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) |"-require" -> add_require (next ()) |"-top" -> set_toplevel_name (dirpath_of_string (next ())) |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) -- cgit v1.2.3 From a6832ccfacd9c105b23a9a77dadc3202f7af26fc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 Sep 2016 10:46:53 +0200 Subject: Argument : assert does fail if no arg is given (fix #4864) --- test-suite/output/Arguments.v | 2 +- test-suite/success/simpl_tuning.v | 2 +- toplevel/vernacentries.ml | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 05eeaac631..bd9240476f 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). Arguments fcomp {_ _ _}%type_scope f g x /. About fcomp. Definition volatile := fun x : nat => x. -Arguments volatile /. +Arguments volatile / _. About volatile. Set Implicit Arguments. Section S1. diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v index d4191b939b..2728672f30 100644 --- a/test-suite/success/simpl_tuning.v +++ b/test-suite/success/simpl_tuning.v @@ -106,7 +106,7 @@ match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end. Abort. Definition volatile := fun x : nat => x. -Arguments volatile /. +Arguments volatile / _. Lemma foo : volatile = volatile. simpl. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 48a85b709f..382a716298 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -986,9 +986,9 @@ let vernac_declare_arguments locality r l nargs flags = | _::li, _::ld, _::ls -> check li ld ls | _ -> assert false in let () = match l with - | [[]] -> () + | [[]] when List.exists ((<>) `Assert) flags -> () | _ -> - List.iter2 (fun l -> check inf_names l) (names :: rest) scopes + List.iter2 (check inf_names) (names :: rest) scopes in (* we take extra scopes apart, and we check they are consistent *) let l, scopes = -- cgit v1.2.3 From af051436672561b4c15e07dfe4f9cee93f0741a4 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 12 Jul 2016 18:46:08 +0200 Subject: Extraction: ignore some useless stuff about universes --- plugins/extraction/extraction.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 312c2eab3d..a980a43f53 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -371,8 +371,7 @@ and extract_really_ind env kn mib = let packets = Array.mapi (fun i mip -> - let (ind,u), ctx = - Universes.fresh_inductive_instance env (kn,i) in + let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in let info = (fst (flag_of_type env ar) = Info) in let s,v = if info then type_sign_vl env ar else [],[] in @@ -591,10 +590,10 @@ let rec extract_term env mle mlt c args = with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' mle' mlt c2 args')) - | Const (kn,u) -> - extract_cst_app env mle mlt kn u args - | Construct (cp,u) -> - extract_cons_app env mle mlt cp u args + | Const (kn,_) -> + extract_cst_app env mle mlt kn args + | Construct (cp,_) -> + extract_cons_app env mle mlt cp args | Proj (p, c) -> let term = Retyping.expand_projection env (Evd.from_env env) p c [] in extract_term env mle mlt term args @@ -645,7 +644,7 @@ and make_mlargs env e s args typs = (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn u args = +and extract_cst_app env mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) let nb,t = record_constant_type env kn None in let schema = nb, expand env t in @@ -718,7 +717,7 @@ and extract_cst_app env mle mlt kn u args = they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args = +and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in -- cgit v1.2.3 From 83435e2c02cfe450eddde50eb92ed2b501f25dfc Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 29 Sep 2016 14:34:38 +0200 Subject: Ncring_initial: avoid a notation overriding --- plugins/setoid_ring/Ncring_initial.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 96885d2f7a..20022c00ec 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -18,7 +18,6 @@ Require Import BinInt. Require Import Setoid. Require Export Ncring. Require Export Ncring_polynom. -Import List. Set Implicit Arguments. @@ -78,7 +77,8 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Notation "[ x ]" := (gen_phiZ x). + Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Local Open Scope ZMORPHISM. Definition get_signZ z := match z with -- cgit v1.2.3 From 1c52cde4e5f5438305e17d95435dbdcf3bf8ea00 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 29 Sep 2016 14:40:00 +0200 Subject: Cleanup API, making inference_hook optional --- stm/lemmas.ml | 4 ++-- stm/lemmas.mli | 2 +- toplevel/vernacentries.ml | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index bf10b91339..022c89ad9a 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = call_hook (fun exn -> exn) hook strength ref) thms_data in start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard -let start_proof_com use_hook kind thms hook = +let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in let levels = Option.map snd (fst (List.hd thms)) in let evdref = ref (match levels with @@ -460,7 +460,7 @@ let start_proof_com use_hook kind thms hook = let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in let flags = all_and_fail_flags in - let flags = { flags with use_hook } in + let flags = { flags with use_hook = inference_hook } in evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map get_name ctx in (compute_proof_name (pi1 kind) sopt, diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 904cdeef4d..39c089be9f 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -34,7 +34,7 @@ val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_ma (Evd.evar_universe_context option -> unit declaration_hook) -> unit val start_proof_com : - Pretyping.inference_hook option -> + ?inference_hook:Pretyping.inference_hook -> goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6723a8b489..f67f6f91ce 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -449,7 +449,7 @@ let vernac_notation locality local = (* Gallina *) let start_proof_and_print k l hook = - let use_hook = + let inference_hook = if Flags.is_program_mode () then let hook env sigma ev = let tac = !Obligations.default_tactic in @@ -468,7 +468,7 @@ let start_proof_and_print k l hook = in Some hook else None in - start_proof_com use_hook k l hook + start_proof_com ?inference_hook k l hook let no_hook = Lemmas.mk_hook (fun _ _ -> ()) -- cgit v1.2.3 From 5348a615a484e379896deac8a6944af1f92b2d4c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Sep 2016 17:58:06 +0200 Subject: test-suite: fix sed on OS X, does not handle + --- test-suite/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index 1dfbb29ff0..a40ea80ae4 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -304,16 +304,16 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ | grep -v "^" \ - | sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \ + | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ > $$tmpoutput; \ - sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \ + sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ - $*.out > $$tmpexpected; \ + $*.out > $$tmpexpected; \ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ -- cgit v1.2.3 From 4e3d4646788c96f16193df14a81aa79938812194 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 29 Sep 2016 09:35:07 +0200 Subject: Fix a bug in subst releaved by an OCaml warning. --- tactics/equality.ml | 8 +- test-suite/output/subst.out | 208 ++++++++++++++++++++++++++++++++++++++++++++ test-suite/output/subst.v | 11 +++ 3 files changed, 224 insertions(+), 3 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index 06a9b317a2..b4c027382a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1730,20 +1730,22 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in - let test (hyp,_,c) = + let select_equation_name (hyp,_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match kind_of_term x, kind_of_term y with - | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) -> + | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> + Some hyp + | _, Var z when not (is_evaluable env (EvalVarRef z)) -> Some hyp | _ -> None with Constr_matching.PatternMatchingFailure -> None in let hyps = Proofview.Goal.hyps gl in - List.rev (List.map_filter test hyps) + List.rev (List.map_filter select_equation_name hyps) in (* Second step: treat equations *) diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out index 209b2bc26f..dbb9e09a43 100644 --- a/test-suite/output/subst.out +++ b/test-suite/output/subst.out @@ -26,6 +26,19 @@ True 1 subgoal + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + x, y : nat Hx : x = 0 Hy : y = 0 @@ -39,6 +52,45 @@ True 1 subgoal + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : 0 = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + H1 : 0 = 1 HA : True H2 : 0 = 2 @@ -49,6 +101,58 @@ True 1 subgoal + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : 0 = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + y, z : nat Hy : y = 0 Hz : z = 0 @@ -75,6 +179,19 @@ True 1 subgoal + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + x, y : nat Hx : x = 0 Hy : y = 0 @@ -88,6 +205,45 @@ True 1 subgoal + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + HB : True + H4 : z = 4 + H3 : 0 = 3 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + HA, HB : True H4 : 0 = 4 H3 : 0 = 3 @@ -95,3 +251,55 @@ H2 : 0 = 2 ============================ True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + HB : True + H4 : z = 4 + H3 : 0 = 3 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v index e48aa6bb28..91bdd03e02 100644 --- a/test-suite/output/subst.v +++ b/test-suite/output/subst.v @@ -45,4 +45,15 @@ Show. trivial. Qed. +(* A bug revealed by OCaml 4.03 warnings *) +Goal forall y, let x:=0 in y=x -> y=y. +intros * H; +subst. +Fail clear H. (* Was working *) +Abort. +Goal forall y, let x:=0 in y=x -> y=y. +intros * H; +subst. +Fail clear H. (* Was failing before fix *) +Abort. -- cgit v1.2.3 From c1c488d08857636381d6cbf3a9202e7123923dd0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 29 Sep 2016 15:17:02 +0200 Subject: Fix bug #5011: Anomaly on [Existing Class]. --- test-suite/bugs/closed/5011.v | 2 ++ toplevel/record.ml | 4 +--- 2 files changed, 3 insertions(+), 3 deletions(-) create mode 100644 test-suite/bugs/closed/5011.v diff --git a/test-suite/bugs/closed/5011.v b/test-suite/bugs/closed/5011.v new file mode 100644 index 0000000000..c3043ca5d1 --- /dev/null +++ b/test-suite/bugs/closed/5011.v @@ -0,0 +1,2 @@ +Record decoder (n : nat) W := { decode : W -> nat }. +Existing Class decoder. diff --git a/toplevel/record.ml b/toplevel/record.ml index 71d070776d..9c4d41ea50 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -521,11 +521,9 @@ let add_inductive_class ind = | LocalDef _ -> None | LocalAssum (_, t) -> Some (lazy t) in - let args = List.map_filter map ctx in - let ty = Inductive.type_of_inductive_knowing_parameters + let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) - (Array.of_list args) in { cl_impl = IndRef ind; cl_context = List.map (const None) ctx, ctx; -- cgit v1.2.3 From 6d20e4c136fb2726ec8577bdfee051ecacdf8261 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 28 Sep 2016 16:24:51 +0200 Subject: fix bug 3683 : adds references to the web site for the bug tracker in error messages --- checker/checker.ml | 3 ++- config/coq_config.mli | 1 + configure.ml | 1 + lib/cErrors.ml | 4 +++- toplevel/coqloop.ml | 4 +++- toplevel/himsg.ml | 3 ++- 6 files changed, 12 insertions(+), 4 deletions(-) diff --git a/checker/checker.ml b/checker/checker.ml index 0c411ae44d..503697b592 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -209,7 +209,8 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report.") +let report () = (str "." ++ spc () ++ str "Please report" ++ + strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") let guill s = str "\"" ++ str s ++ str "\"" diff --git a/config/coq_config.mli b/config/coq_config.mli index a0e1019fa8..6087c01169 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -62,6 +62,7 @@ val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *) val wwwcoq : string val wwwrefman : string +val wwwbugtracker : string val wwwstdlib : string val localwwwrefman : string diff --git a/configure.ml b/configure.ml index 2c1d531ead..23ec93e078 100644 --- a/configure.ml +++ b/configure.ml @@ -1043,6 +1043,7 @@ let write_configml f = pr "let with_geoproof = ref %B\n" !Prefs.geoproof; pr_s "browser" browser; pr_s "wwwcoq" !Prefs.coqwebsite; + pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/"); pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 1459141d1e..c69c7e4001 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -93,7 +93,9 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.") + hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ + strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++ + str ".") else hov 0 (raw_anomaly e) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 0d4807e163..69d68bd357 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -348,5 +348,7 @@ let rec loop () = | any -> Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++ str (Printexc.to_string any) ++ - fnl() ++ str"Please report."); + fnl() ++ + str"Please report" ++ + strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); loop () diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ff4c18ad21..6ee695bc24 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -304,7 +304,8 @@ let explain_unification_error env sigma p1 p2 = function else [] | MetaOccurInBody evk -> [str "instance for " ++ quote (pr_existential_key sigma evk) ++ - strbrk " refers to a metavariable - please report your example"] + strbrk " refers to a metavariable - please report your example" ++ + strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."] | InstanceNotSameType (evk,env,t,u) -> let t, u = pr_explicit env sigma t u in [str "unable to find a well-typed instantiation for " ++ -- cgit v1.2.3 From 9615c025a2a09b69f2001d44a66a1fddef74e680 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 29 Sep 2016 15:51:18 +0200 Subject: Fix bug #4869, allow Prop, Set, and level names in constraints. --- intf/vernacexpr.mli | 2 +- library/declare.ml | 24 ++++++++++++++++-------- library/declare.mli | 4 +++- parsing/g_constr.ml4 | 6 +++--- parsing/g_vernac.ml4 | 4 ++-- parsing/pcoq.ml | 1 + parsing/pcoq.mli | 1 + printing/ppconstr.ml | 6 ++++++ printing/ppconstrsig.mli | 1 + printing/ppvernac.ml | 3 ++- test-suite/bugs/closed/4869.v | 18 ++++++++++++++++++ toplevel/command.mli | 2 +- 12 files changed, 55 insertions(+), 17 deletions(-) create mode 100644 test-suite/bugs/closed/4869.v diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ed44704df4..e6599a30d1 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -346,7 +346,7 @@ type vernac_expr = | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list - | VernacConstraint of (lident * Univ.constraint_type * lident) list + | VernacConstraint of (glob_level * Univ.constraint_type * glob_level) list (* Gallina extensions *) | VernacBeginSection of lident diff --git a/library/declare.ml b/library/declare.ml index 3d063225f4..7025839d0c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -491,12 +491,20 @@ let input_constraints : constraint_decl -> Libobject.obj = classify_function = (fun a -> Keep a) } let do_constraint poly l = - let u_of_id = - let names, _ = Universes.global_universe_names () in - fun (loc, id) -> - try Idmap.find id names - with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + let open Misctypes in + let u_of_id x = + match x with + | GProp -> Loc.dummy_loc, (false, Univ.Level.prop) + | GSet -> Loc.dummy_loc, (false, Univ.Level.set) + | GType None -> + user_err_loc (Loc.dummy_loc, "Constraint", + str "Cannot declare constraints on anonymous universes") + | GType (Some (loc, id)) -> + let id = Id.of_string id in + let names, _ = Universes.global_universe_names () in + try loc, Idmap.find id names + with Not_found -> + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) in let in_section = Lib.sections_are_opened () in let () = @@ -514,8 +522,8 @@ let do_constraint poly l = ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let p, lu = u_of_id l and p', ru = u_of_id r in - check_poly (fst l) p (fst r) p'; + let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in + check_poly ploc p rloc p'; Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in diff --git a/library/declare.mli b/library/declare.mli index 7824506da0..4051174a75 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -90,4 +90,6 @@ val exists_name : Id.t -> bool (** Global universe names and constraints *) val do_universe : polymorphic -> Id.t Loc.located list -> unit -val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_constraint : polymorphic -> + (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> + unit diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 74994c5e3d..7f3a3d10ca 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -127,7 +127,7 @@ let name_colon = let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None GEXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr sort global + GLOBAL: binder_constr lconstr constr operconstr universe_level sort global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; @@ -298,10 +298,10 @@ GEXTEND Gram | -> [] ] ] ; instance: - [ [ "@{"; l = LIST1 level; "}" -> Some l + [ [ "@{"; l = LIST1 universe_level; "}" -> Some l | -> None ] ] ; - level: + universe_level: [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c09693b364..78176d9346 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -226,8 +226,8 @@ GEXTEND Gram [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ] ; univ_constraint: - [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; - r = identref -> (l, ord, r) ] ] + [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; + r = universe_level -> (l, ord, r) ] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 714e25f85e..4e069c9e33 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -304,6 +304,7 @@ module Constr = let binder_constr = gec_constr "binder_constr" let ident = make_gen_entry uconstr "ident" let global = make_gen_entry uconstr "global" + let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" let pattern = Gram.entry_create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 635b0170ae..7f49c997fe 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -157,6 +157,7 @@ module Constr : val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry val global : reference Gram.entry + val universe_level : glob_level Gram.entry val sort : glob_sort Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index a00e4bab30..aa0ebbb83b 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -149,6 +149,12 @@ end) = struct | GType [] -> tag_type (str "Type") | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) + let pr_glob_level = function + | GProp -> tag_type (str "Prop") + | GSet -> tag_type (str "Set") + | GType None -> tag_type (str "Type") + | GType (Some (_, u)) -> tag_type (str u) + let pr_qualid sp = let (sl, id) = repr_qualid sp in let id = tag_ref (pr_id id) in diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli index a59fc6d67d..3de0d805c4 100644 --- a/printing/ppconstrsig.mli +++ b/printing/ppconstrsig.mli @@ -44,6 +44,7 @@ module type Pp = sig val pr_qualid : qualid -> std_ppcmds val pr_patvar : patvar -> std_ppcmds + val pr_glob_level : glob_level -> std_ppcmds val pr_glob_sort : glob_sort -> std_ppcmds val pr_guard_annot : (constr_expr -> std_ppcmds) -> local_binder list -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 40ce28dc0c..2c41d1146c 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -838,7 +838,8 @@ module Make ) | VernacConstraint v -> let pr_uconstraint (l, d, r) = - pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r + pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ + pr_glob_level r in return ( hov 2 (keyword "Constraint" ++ spc () ++ diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v new file mode 100644 index 0000000000..6d21b66fe9 --- /dev/null +++ b/test-suite/bugs/closed/4869.v @@ -0,0 +1,18 @@ +Universes i. + +Fail Constraint i < Set. +Fail Constraint i <= Set. +Fail Constraint i = Set. +Constraint Set <= i. +Constraint Set < i. +Fail Constraint i < j. (* undeclared j *) +Fail Constraint i < Type. (* anonymous *) + +Set Universe Polymorphism. + +Section Foo. + Universe j. + Constraint Set < j. + + Definition foo := Type@{j}. +End Foo. \ No newline at end of file diff --git a/toplevel/command.mli b/toplevel/command.mli index d353724294..616afb91f0 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -22,7 +22,7 @@ open Pfedit val do_universe : polymorphic -> Id.t Loc.located list -> unit val do_constraint : polymorphic -> - (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit + (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit (** {6 Hooks for Pcoq} *) -- cgit v1.2.3 From 14e47506ffabc43c25bf8da108abb6df78b803ad Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 29 Sep 2016 17:33:47 +0200 Subject: Being more informative about the change of behavior of "subst". --- CHANGES | 5 ++++- COMPATIBILITY | 6 ++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/CHANGES b/CHANGES index c3eaae6ee0..cf1fefa75d 100644 --- a/CHANGES +++ b/CHANGES @@ -27,7 +27,10 @@ Specification language Tactics - Flag "Bracketing Last Introduction Pattern" is now on by default. -- Flag "Regular Subst Tactic" is now on by default. +- Flag "Regular Subst Tactic" is now on by default: it respects the + initial order of hypothesis, it contracts cycles, it unfolds no + local definitions (common source of incompatibilities, fixable by + "Unset Regular Subst Tactic"). - New flag "Refolding Reduction", now disabled by default, which turns on refolding of constants/fixpoints (as in cbn) during the reductions done during type inference and tactic retyping. Can be extremely diff --git a/COMPATIBILITY b/COMPATIBILITY index 892eaa599e..d423e71df3 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -11,6 +11,12 @@ Remedy: instead (compatible with 8.4). - Unset the option for the program/proof the obligation/subproof originates from. + +Symptom: In a goal, order of hypotheses, or absence of an equality of +the form "x = t" or "t = x", or no unfolding of a local definition. +Cause: This might be connected to a number of fixes in the tactic +"subst". The former behavior can be reactivated by issuing "Unset +Regular Subst Tactic". Potential sources of incompatibilities between Coq V8.4 and V8.5 ---------------------------------------------------------------- -- cgit v1.2.3 From cf87e73ff4dd0b9c70436d66d326ae839868ba78 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Sep 2016 17:26:14 +0200 Subject: Fix bug #5036 autorewrite, sections and universes Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately). --- library/declare.ml | 26 +++++++++++++++++++++----- library/declare.mli | 4 +++- ltac/extratactics.ml4 | 3 ++- test-suite/bugs/closed/5036.v | 10 ++++++++++ 4 files changed, 36 insertions(+), 7 deletions(-) create mode 100644 test-suite/bugs/closed/5036.v diff --git a/library/declare.ml b/library/declare.ml index 3d063225f4..7d32b93dc5 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -434,6 +434,23 @@ let assumption_message id = (** Global universe names, in a different summary *) +type universe_context_decl = polymorphic * Univ.universe_context_set + +let cache_universe_context (p, ctx) = + Global.push_context_set p ctx; + if p then Lib.add_section_context ctx + +let input_universe_context : universe_context_decl -> Libobject.obj = + declare_object + { (default_object "Global universe context state") with + cache_function = (fun (na, pi) -> cache_universe_context pi); + load_function = (fun _ (_, pi) -> cache_universe_context pi); + discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); + classify_function = (fun a -> Keep a) } + +let declare_universe_context poly ctx = + Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) + (* Discharged or not *) type universe_decl = polymorphic * (Id.t * Univ.universe_level) list @@ -446,9 +463,8 @@ let cache_universes (p, l) = Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in - Global.push_context_set p ctx; - if p then Lib.add_section_context ctx; - Universes.set_global_universe_names glob' + cache_universe_context (p, ctx); + Universes.set_global_universe_names glob' let input_universes : universe_decl -> Libobject.obj = declare_object @@ -475,8 +491,8 @@ let do_universe poly l = type constraint_decl = polymorphic * Univ.constraints let cache_constraints (na, (p, c)) = - Global.add_constraints c; - if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty) + let ctx = Univ.ContextSet.add_constraints c Univ.ContextSet.empty in + cache_universe_context (p,ctx) let discharge_constraints (_, (p, c as a)) = if p then None else Some a diff --git a/library/declare.mli b/library/declare.mli index 7824506da0..e614f5206a 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -87,7 +87,9 @@ val exists_name : Id.t -> bool -(** Global universe names and constraints *) +(** Global universe contexts, names and constraints *) + +val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit val do_universe : polymorphic -> Id.t Loc.located list -> unit val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e50b0520bc..d6ba670d83 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -263,7 +263,8 @@ let add_rewrite_hint bases ort t lcsr = let ctx = let ctx = UState.context_set ctx in if poly then ctx - else (Global.push_context_set false ctx; Univ.ContextSet.empty) + else (Declare.declare_universe_context false ctx; + Univ.ContextSet.empty) in Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in let eqs = List.map f lcsr in diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v new file mode 100644 index 0000000000..12c958be67 --- /dev/null +++ b/test-suite/bugs/closed/5036.v @@ -0,0 +1,10 @@ +Section foo. + Context (F : Type -> Type). + Context (admit : forall {T}, F T = True). + Hint Rewrite (fun T => @admit T). + Lemma bad : F False. + Proof. + autorewrite with core. + constructor. + Qed. +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *) \ No newline at end of file -- cgit v1.2.3 From 601fd9343a241706c0a205aaf8e08255753c3780 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 Sep 2016 15:23:07 +0200 Subject: Arguments: cleanup + detect discrepancy rename/implicit (#3753) It seems warnings are not taken into account in output/ tests. --- intf/vernacexpr.mli | 9 +++- parsing/g_vernac.ml4 | 20 +++++-- printing/ppvernac.ml | 14 ++--- test-suite/bugs/closed/3045.v | 2 +- test-suite/bugs/closed/3753.v | 4 ++ test-suite/bugs/opened/3753.v | 4 -- test-suite/output/Arguments_renaming.out | 20 +++++-- test-suite/output/Arguments_renaming.v | 2 +- toplevel/vernacentries.ml | 90 ++++++++++++++++++++++---------- 9 files changed, 118 insertions(+), 47 deletions(-) create mode 100644 test-suite/bugs/closed/3753.v delete mode 100644 test-suite/bugs/opened/3753.v diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ed44704df4..6df85f0764 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -415,7 +415,7 @@ type vernac_expr = | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * - ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list * + (vernac_argument_status list) list * int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list @@ -477,6 +477,13 @@ and tacdef_body = | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) +and vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : (Loc.t * string) option; + implicit_status : [ `Implicit | `MaximallyImplicit | `NotImplicit]; +} + (* A vernac classifier has to tell if a command: vernac_when: has to be executed now (alters the parser) or later vernac_type: if it is starts, ends, continues a proof or diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c09693b364..b0b656acf6 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -653,23 +653,35 @@ GEXTEND Gram | IDENT "Arguments"; qid = smart_global; impl = LIST1 [ l = LIST0 [ item = argument_spec -> - let id, r, s = item in [`Id (id,r,s,false,false)] + let name, recarg_like, notation_scope = item in + [`Id { name=name; recarg_like=recarg_like; + notation_scope=notation_scope; + implicit_status = `NotImplicit}] | "/" -> [`Slash] | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = `NotImplicit}) items | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = `Implicit}) items | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = `MaximallyImplicit}) items ] -> l ] SEP ","; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> let mods = match mods with None -> [] | Some l -> List.flatten l in diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 40ce28dc0c..1d8dcabccd 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1029,16 +1029,18 @@ module Make pr_smart_global q ++ let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in let pr_if b x = if b then x else str "" in - let pr_br imp max x = match imp, max with - | true, false -> str "[" ++ x ++ str "]" - | true, true -> str "{" ++ x ++ str "}" - | _ -> x in + let pr_br imp x = match imp with + | `Implicit -> str "[" ++ x ++ str "]" + | `MaximallyImplicit -> str "{" ++ x ++ str "}" + | `NotImplicit -> x in let rec aux n l = match n, l with | 0, l -> spc () ++ str"/" ++ aux ~-1 l | _, [] -> mt() - | n, (id,k,s,imp,max) :: tl -> - spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ + | n, { name = id; recarg_like = k; + notation_scope = s; + implicit_status = imp } :: tl -> + spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ aux (n-1) tl in prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ (if not (List.is_empty mods) then str" : " else str"") ++ diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v index ef110ad0d0..5f80013df2 100644 --- a/test-suite/bugs/closed/3045.v +++ b/test-suite/bugs/closed/3045.v @@ -12,7 +12,7 @@ Record SpecializedCategory (obj : Type) := Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' }. -Arguments Compose {obj} [C s d d'] m1 m2 : rename. +Arguments Compose {obj} [C s d d'] _ _ : rename. Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type := | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'. diff --git a/test-suite/bugs/closed/3753.v b/test-suite/bugs/closed/3753.v new file mode 100644 index 0000000000..5bfbee9494 --- /dev/null +++ b/test-suite/bugs/closed/3753.v @@ -0,0 +1,4 @@ +Axiom foo : Type -> Type. +Axiom bar : forall (T : Type), T -> foo T. +Arguments bar A x : rename. +About bar. \ No newline at end of file diff --git a/test-suite/bugs/opened/3753.v b/test-suite/bugs/opened/3753.v deleted file mode 100644 index 05d77c831b..0000000000 --- a/test-suite/bugs/opened/3753.v +++ /dev/null @@ -1,4 +0,0 @@ -Axiom foo : Type -> Type. -Axiom bar : forall (T : Type), T -> foo T. -Arguments bar A x : rename. -Fail About bar. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 3488cb3056..815305581c 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,9 +1,20 @@ +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36: +Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. +[arguments-assert,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to B. -The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. -Argument A renamed to T. +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. +[arguments-assert,vernacular] +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +Warning: This command is just asserting the number and names of arguments of +identity. If this is what you want add ': assert' to silence the warning. If +you want to clear implicit arguments add ': clear implicits'. If you want to +clear notation scopes add ': clear scopes' [arguments-assert,vernacular] +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 4, characters 0-40: +Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. +[arguments-assert,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -110,6 +121,9 @@ The command has indeed failed with message: Error: Argument z cannot be declared implicit. The command has indeed failed with message: Error: Extra argument y. +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 53, characters 0-26: +Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. +[arguments-assert,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index b6fbeb6ec7..e42c983361 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -1,5 +1,5 @@ Fail Arguments eq_refl {B y}, [B] y. -Fail Arguments identity T _ _. +Arguments identity T _ _. Arguments eq_refl A x : assert. Arguments eq_refl {B y}, [B] y : rename. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 25d16f91f5..1d6278066a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -979,12 +979,17 @@ let warn_arguments_assert = strbrk "to clear implicit arguments add ': clear implicits'. " ++ strbrk "If you want to clear notation scopes add ': clear scopes'") +let warn_renaming_nonimplicit = + CWarnings.create ~name:"arguments-assert" ~category:"vernacular" + (fun (oldn, newn) -> + strbrk "Ignoring rename of "++pr_id oldn++str" into "++pr_id newn++ + strbrk ". Only implicit arguments can be renamed.") let vernac_declare_arguments locality r l nargs flags = let extra_scope_flag = List.mem `ExtraScopes flags in - let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let names = List.map (List.map (fun { name } -> name)) l in let names, rest = List.hd names, List.tl names in - let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in + let scopes = List.map (List.map (fun { notation_scope = s } -> s)) l in if List.exists (fun na -> not (List.equal Name.equal na names)) rest then error "All arguments lists must declare the same names."; if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names)) @@ -1023,13 +1028,15 @@ let vernac_declare_arguments locality r l nargs flags = | [[]] -> l | _ -> let name_anons = function - | (Anonymous, a,b,c,d), Name id -> Name id, a,b,c,d + | { name = Anonymous } as x, Name id -> { x with name = Name id } | x, _ -> x in List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in - let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let names_decl = List.map (List.map (fun { name } -> name)) l in let renamed_arg = ref None in let set_renamed a b = - if Option.is_empty !renamed_arg && not (Id.equal a b) then renamed_arg := Some(b,a) in + if Option.is_empty !renamed_arg && not (Id.equal a b) then + renamed_arg := Some(b,a) + in let some_renaming_specified = try let names = Arguments_renaming.arguments_names sr in @@ -1039,22 +1046,50 @@ let vernac_declare_arguments locality r l nargs flags = match l with | [[]] -> false, [[]] | _ -> - List.fold_map (fun sr il -> - let sr', impl = List.fold_map (fun b -> function - | (Anonymous, _,_, true, max), Name id -> assert false - | (Name x, _,_, true, _), Anonymous -> - errorlabstrm "vernac_declare_arguments" - (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.") - | (Name iid, _,_, true, max), Name id -> - set_renamed iid id; - b || not (Id.equal iid id), Some (ExplByName id, max, false) - | (Name iid, _,_, _, _), Name id -> - set_renamed iid id; - b || not (Id.equal iid id), None - | _ -> b, None) - sr (List.combine il inf_names) in - sr || sr', List.map_filter (fun x -> x) impl) - some_renaming_specified l in + let some_renaming = ref some_renaming_specified in + let rec aux il = + match il with + | [] -> [] + | il :: ils -> aux_single il inf_names :: aux ils + and aux_single impl inf_names = + match impl, inf_names with + | [], _ -> [] + | { name = Anonymous; + implicit_status = (`Implicit|`MaximallyImplicit)} :: _, + Name id :: _ -> + assert false + | { name = Name x; + implicit_status = (`Implicit|`MaximallyImplicit)} :: _, + Anonymous :: _ -> + errorlabstrm "vernac_declare_arguments" + (str"Argument "++ pr_id x ++str " cannot be declared implicit.") + | { name = Name iid; + implicit_status = (`Implicit|`MaximallyImplicit as i)} :: impl, + Name id :: inf_names -> + let max = i = `MaximallyImplicit in + set_renamed iid id; + some_renaming := !some_renaming || not (Id.equal iid id); + (ExplByName id,max,false) :: aux_single impl inf_names + | { name = Name iid } :: impl, + Name id :: inf_names when not (Id.equal iid id) -> + warn_renaming_nonimplicit (id, iid); + aux_single impl inf_names + | { name = Name iid } :: impl, Name id :: inf_names + when not (Id.equal iid id) -> + aux_single impl inf_names + | { name = Name iid } :: impl, Name id :: inf_names -> + set_renamed iid id; + some_renaming := !some_renaming || not (Id.equal iid id); + aux_single impl inf_names + | _ :: impl, _ :: inf_names -> + (* no rename, no implicit status *) aux_single impl inf_names + | _ :: _, [] -> assert false (* checked before in check() *) + in + !some_renaming, aux l in + (* We check if renamed arguments do match previously declared imp args, + * since the system has this invariant *) + let some_implicits_specified = + match implicits with [[]] -> false | _ -> true in if some_renaming_specified then if not (List.mem `Rename flags) then errorlabstrm "vernac_declare_arguments" @@ -1062,14 +1097,13 @@ let vernac_declare_arguments locality r l nargs flags = match !renamed_arg with | None -> mt () | Some (o,n) -> - str "\nArgument " ++ pr_id o ++ str " renamed to " ++ pr_id n ++ str ".") + str "\nArgument " ++ pr_id o ++ + str " renamed to " ++ pr_id n ++ str ".") else Arguments_renaming.rename_arguments - (make_section_locality locality) sr names_decl; + (make_section_locality locality) sr names_decl; (* All other infos are in the first item of l *) let l = List.hd l in - let some_implicits_specified = match implicits with - | [[]] -> false | _ -> true in let scopes = List.map (function | None -> None | Some (o, k) -> @@ -1080,7 +1114,7 @@ let vernac_declare_arguments locality r l nargs flags = let some_scopes_specified = List.exists ((!=) None) scopes in let rargs = Util.List.map_filter (function (n, true) -> Some n | _ -> None) - (Util.List.map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in + (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 l) in if some_scopes_specified || List.mem `ClearScopes flags then vernac_arguments_scope locality r scopes; if not some_implicits_specified && List.mem `DefaultImplicits flags then @@ -1101,7 +1135,9 @@ let vernac_declare_arguments locality r l nargs flags = | ConstRef _ as c -> Reductionops.ReductionBehaviour.set (make_section_locality locality) c (rargs, nargs, flags) - | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.") + | _ -> errorlabstrm "" + (strbrk "Modifiers of the behavior of the simpl tactic "++ + strbrk "are relevant for constants only.") end; if not (some_renaming_specified || some_implicits_specified || -- cgit v1.2.3 From 89c2942352ec5d8d5b9cfe1116376412770cb396 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 Sep 2016 17:33:38 +0200 Subject: STM: compute the correct state for edited Qed (#5086) When a proof is 're-opened', the Qed node does not change. Still the STM has to install the old state (where only the future proof has to be updated). This bit was missing. Why was it working: the bug happens only if you reopen the very last proof, i.e. there is no sentence that stays valid after the Qed. If there is such a sentence, its state was computed correctly before, and is not changed. If it is the very last, then the next state is based on the wrong one... --- stm/stm.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/stm/stm.ml b/stm/stm.ml index c53bd958aa..bb4f5f72f3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2177,7 +2177,10 @@ let known_state ?(redefine_qed=false) ~cache id = Slaves.build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name in Future.replace ofp fp; - qed.fproof <- Some (fp, cancel) + qed.fproof <- Some (fp, cancel); + (* We don't generate a new state, but we still need + * to install the right one *) + State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> reach ~cache:`Shallow start; -- cgit v1.2.3 From edb55a94fc5c0473e57f5a61c0c723194c2ff414 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 27 Sep 2016 17:15:10 +0200 Subject: Fix bug #4798: compat notations should not modify the parser. This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data. --- ide/texmacspp.ml | 3 +- intf/vernacexpr.mli | 3 +- lib/flags.ml | 27 +++++++++------- lib/flags.mli | 1 + parsing/g_vernac.ml4 | 5 ++- printing/ppvernac.ml | 8 ++--- test-suite/bugs/closed/4798.v | 3 ++ toplevel/metasyntax.ml | 75 ++++++++++++++++++++++++++++--------------- 8 files changed, 80 insertions(+), 45 deletions(-) create mode 100644 test-suite/bugs/closed/4798.v diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 53a29008ad..9de1df9f1e 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -189,7 +189,8 @@ match sm with end | SetEntryType (s, _) -> ["entrytype", s] | SetOnlyPrinting -> ["onlyprinting", ""] - | SetOnlyParsing v -> ["compat", Flags.pr_version v] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion v -> ["compat", Flags.pr_version v] | SetFormat (system, (loc, s)) -> let start, stop = unlock loc in ["format-"^system, s; "begin", start; "end", stop] diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 6df85f0764..1063a74d9f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -211,8 +211,9 @@ type syntax_modifier = | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key - | SetOnlyParsing of Flags.compat_version + | SetOnlyParsing | SetOnlyPrinting + | SetCompatVersion of Flags.compat_version | SetFormat of string * string located type proof_end = diff --git a/lib/flags.ml b/lib/flags.ml index d29064c97f..af55e9e2bb 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -112,17 +112,22 @@ type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current let compat_version = ref Current -let version_strictly_greater v = match !compat_version, v with -| V8_2, (V8_2 | V8_3 | V8_4 | V8_5 | Current) -> false -| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false -| V8_4, (V8_4 | V8_5 | Current) -> false -| V8_5, (V8_5 | Current) -> false -| Current, Current -> false -| V8_3, V8_2 -> true -| V8_4, (V8_2 | V8_3) -> true -| V8_5, (V8_2 | V8_3 | V8_4) -> true -| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> true - +let version_compare v1 v2 = match v1, v2 with +| V8_2, V8_2 -> 0 +| V8_2, (V8_3 | V8_4 | V8_5 | Current) -> -1 +| V8_3, V8_2 -> 1 +| V8_3, V8_3 -> 0 +| V8_3, (V8_4 | V8_5 | Current) -> -1 +| V8_4, (V8_2 | V8_3) -> 1 +| V8_4, V8_4 -> 0 +| V8_4, (V8_5 | Current) -> -1 +| V8_5, (V8_2 | V8_3 | V8_4) -> 1 +| V8_5, V8_5 -> 0 +| V8_5, Current -> -1 +| Current, Current -> 0 +| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 1 + +let version_strictly_greater v = version_compare !compat_version v > 0 let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function diff --git a/lib/flags.mli b/lib/flags.mli index 839c252cbb..9dc0c9c048 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -64,6 +64,7 @@ val univ_print : bool ref type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current val compat_version : compat_version ref +val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool val pr_version : compat_version -> string diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b0b656acf6..1a40128916 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1115,10 +1115,9 @@ GEXTEND Gram | IDENT "right"; IDENT "associativity" -> SetAssoc RightA | IDENT "no"; IDENT "associativity" -> SetAssoc NonA | IDENT "only"; IDENT "printing" -> SetOnlyPrinting - | IDENT "only"; IDENT "parsing" -> - SetOnlyParsing Flags.Current + | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> - SetOnlyParsing (Coqinit.get_compat_version s) + SetCompatVersion (Coqinit.get_compat_version s) | IDENT "format"; s1 = [s = STRING -> (!@loc,s)]; s2 = OPT [s = STRING -> (!@loc,s)] -> begin match s1, s2 with diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 1d8dcabccd..503b29aaf2 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -367,8 +367,8 @@ module Make | SetAssoc NonA -> keyword "no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ | SetOnlyPrinting -> keyword "only printing" - | SetOnlyParsing Flags.Current -> keyword "only parsing" - | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") + | SetOnlyParsing -> keyword "only parsing" + | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat("text",s) -> keyword "format " ++ pr_located qs s | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s @@ -1002,13 +1002,13 @@ module Make ) | VernacHints (_, dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> + | VernacSyntacticDefinition (id,(ids,c),_,compat) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers - (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) + (match compat with None -> [] | Some v -> [SetCompatVersion v])) ) | VernacDeclareImplicits (q,[]) -> return ( diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v new file mode 100644 index 0000000000..dbc3d46fce --- /dev/null +++ b/test-suite/bugs/closed/4798.v @@ -0,0 +1,3 @@ +Check match 2 with 0 => 0 | S n => n end. +Notation "|" := 1 (compat "8.4"). +Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a1edb7139e..ce8798c713 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -673,8 +673,13 @@ type syntax_extension = { synext_notgram : notation_grammar; synext_unparsing : unparsing list; synext_extra : (string * string) list; + synext_compat : Flags.compat_version option; } +let is_active_compat = function +| None -> true +| Some v -> 0 <= Flags.version_compare v !Flags.compat_version + type syntax_extension_obj = locality_flag * syntax_extension list let cache_one_syntax_extension se = @@ -685,13 +690,15 @@ let cache_one_syntax_extension se = let oldprec = Notation.level_of_notation ntn in if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec with Not_found -> - (* Reserve the notation level *) - Notation.declare_notation_level ntn prec; - (* Declare the parsing rule *) - if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; - (* Declare the notation rule *) - Notation.declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram + if is_active_compat se.synext_compat then begin + (* Reserve the notation level *) + Notation.declare_notation_level ntn prec; + (* Declare the parsing rule *) + if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; + (* Declare the notation rule *) + Notation.declare_notation_rule ntn + ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram + end let cache_syntax_extension (_, (_, sy)) = List.iter cache_one_syntax_extension sy @@ -725,9 +732,10 @@ let inSyntaxExtension : syntax_extension_obj -> obj = let interp_modifiers modl = let onlyparsing = ref false in let onlyprinting = ref false in + let compat = ref None in let rec interp assoc level etyps format extra = function | [] -> - (assoc,level,etyps,!onlyparsing,!onlyprinting,format,extra) + (assoc,level,etyps,!onlyparsing,!onlyprinting,!compat,format,extra) | SetEntryType (s,typ) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then @@ -749,12 +757,15 @@ let interp_modifiers modl = | SetAssoc a :: l -> if not (Option.is_empty assoc) then error"An associativity is given more than once."; interp (Some a) level etyps format extra l - | SetOnlyParsing _ :: l -> + | SetOnlyParsing :: l -> onlyparsing := true; interp assoc level etyps format extra l | SetOnlyPrinting :: l -> onlyprinting := true; interp assoc level etyps format extra l + | SetCompatVersion v :: l -> + compat := Some v; + interp assoc level etyps format extra l | SetFormat ("text",s) :: l -> if not (Option.is_empty format) then error "A format is given more than once."; interp assoc level etyps (Some s) extra l @@ -763,7 +774,7 @@ let interp_modifiers modl = in interp None None [] None [] modl let check_infix_modifiers modifiers = - let (_, _, t, _, _, _, _) = interp_modifiers modifiers in + let (_, _, t, _, _, _, _, _) = interp_modifiers modifiers in if not (List.is_empty t) then error "Explicit entry level or type unexpected in infix notation." @@ -775,20 +786,25 @@ let check_useless_entry_types recvars mainvars etyps = | _ -> () let not_a_syntax_modifier = function -| SetOnlyParsing _ -> true +| SetOnlyParsing -> true | SetOnlyPrinting -> true +| SetCompatVersion _ -> true | _ -> false let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods let is_only_parsing mods = - let test = function SetOnlyParsing _ -> true | _ -> false in + let test = function SetOnlyParsing -> true | _ -> false in List.exists test mods let is_only_printing mods = let test = function SetOnlyPrinting -> true | _ -> false in List.exists test mods +let get_compat_version mods = + let test = function SetCompatVersion v -> Some v | _ -> None in + try Some (List.find_map test mods) with Not_found -> None + (* Compute precedences from modifiers (or find default ones) *) let set_entry_type etyps (x,typ) = @@ -966,7 +982,7 @@ let remove_curly_brackets l = in aux true l let compute_syntax_data df modifiers = - let (assoc,n,etyps,onlyparse,onlyprint,fmt,extra) = interp_modifiers modifiers in + let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in let assoc = match assoc with None -> (* default *) Some NonA | a -> a in let toks = split_notation_string df in let (recvars,mainvars,symbols) = analyze_notation_tokens toks in @@ -992,12 +1008,12 @@ let compute_syntax_data df modifiers = let sy_data = (n,sy_typs,symbols',fmt) in let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in - let i_data = (onlyparse,onlyprint,recvars,mainvars,(ntn_for_interp,df')) in + let i_data = (onlyparse,onlyprint,compat,recvars,mainvars,(ntn_for_interp,df')) in (* Return relevant data for interpretation and for parsing/printing *) (msgs,i_data,i_typs,sy_fulldata,extra) let compute_pure_syntax_data df mods = - let (msgs,(onlyparse,onlyprint,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in + let (msgs,(onlyparse,onlyprint,_,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in let msgs = if onlyparse then (Feedback.msg_warning ?loc:None, @@ -1014,6 +1030,7 @@ type notation_obj = { notobj_interp : interpretation; notobj_onlyparse : bool; notobj_onlyprint : bool; + notobj_compat : Flags.compat_version option; notobj_notation : notation * notation_location; } @@ -1024,7 +1041,9 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin + let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in + let active = is_active_compat nobj.notobj_compat in + if Int.equal i 1 && fresh && active then begin (* Declare the interpretation *) let onlyprint = nobj.notobj_onlyprint in let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in @@ -1094,7 +1113,9 @@ let recover_syntax ntn = synext_notation = ntn; synext_notgram = pa_rule; synext_unparsing = pp_rule; - synext_extra = pp_extra_rules } + synext_extra = pp_extra_rules; + synext_compat = None; + } with Not_found -> raise NoSyntaxRule @@ -1128,7 +1149,7 @@ let make_pp_rule (n,typs,symbols,fmt) = | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) -let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint = +let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint compat = let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in let pp_rule = make_pp_rule sy_data in let sy = { @@ -1137,6 +1158,7 @@ let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint = synext_notgram = pa_rule; synext_unparsing = pp_rule; synext_extra = extra; + synext_compat = compat; } in (* By construction, the rule for "{ _ }" is declared, but we need to redeclare it because the file where it is declared needs not be open @@ -1153,9 +1175,9 @@ let to_map l = let add_notation_in_scope local df c mods scope = let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in (* Prepare the interpretation *) - let (onlyparse, onlyprint, recvars,mainvars, df') = i_data in + let (onlyparse, onlyprint, compat, recvars,mainvars, df') = i_data in (* Prepare the parsing and printing rules *) - let sy_rules = make_syntax_rules sy_data extra onlyprint in + let sy_rules = make_syntax_rules sy_data extra onlyprint compat in let i_vars = make_internalization_vars recvars mainvars i_typs in let nenv = { ninterp_var_type = to_map i_vars; @@ -1173,6 +1195,7 @@ let add_notation_in_scope local df c mods scope = (** Order is important here! *) notobj_onlyparse = onlyparse; notobj_onlyprint = onlyprint; + notobj_compat = compat; notobj_notation = df'; } in (* Ready to change the global state *) @@ -1181,7 +1204,7 @@ let add_notation_in_scope local df c mods scope = Lib.add_anonymous_leaf (inNotation notation); df' -let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint = +let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let dfs = split_notation_string df in let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) @@ -1212,6 +1235,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) (** Order is important here! *) notobj_onlyparse = onlyparse; notobj_onlyprint = onlyprint; + notobj_compat = compat; notobj_notation = df'; } in Lib.add_anonymous_leaf (inNotation notation); @@ -1221,19 +1245,19 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let add_syntax_extension local ((loc,df),mods) = let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in - let sy_rules = make_syntax_rules sy_data extra onlyprint in + let sy_rules = make_syntax_rules sy_data extra onlyprint None in Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) (* Notations with only interpretation *) let add_notation_interpretation ((loc,df),c,sc) = - let df' = add_notation_interpretation_core false df c sc false false in + let df' = add_notation_interpretation_core false df c sc false false None in Dumpglob.dump_notation (loc,df') sc true let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore - (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false) ()); + (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); with NoSyntaxRule -> error "Parsing rule for this notation has to be previously declared."); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc @@ -1246,7 +1270,8 @@ let add_notation local c ((loc,df),modifiers) sc = (* No syntax data: try to rely on a previously declared rule *) let onlyparse = is_only_parsing modifiers in let onlyprint = is_only_printing modifiers in - try add_notation_interpretation_core local df c sc onlyparse onlyprint + let compat = get_compat_version modifiers in + try add_notation_interpretation_core local df c sc onlyparse onlyprint compat with NoSyntaxRule -> (* Try to determine a default syntax rule *) add_notation_in_scope local df c modifiers sc -- cgit v1.2.3 From 46daf37ed46397b03a30fa2d89b62ffcc2c8d166 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 14:32:50 -0400 Subject: Set the default LtacProf cutoff to 2% This was the original value from Tobias' code. When a user passes -profile-ltac on the command line, or inserts [Show Ltac Profile] in the document, the most useful default behavior is to not overload them with useless information. When GUI clients want to display fancier profiling information, there is no cost to the user to requiring them to specify what cutoff they want. If the GUI client does not have any special LtacProf handling, the most useful presentation is again the one that cuts off the display at 2% total time. --- lib/flags.ml | 2 +- test-suite/Makefile | 2 +- test-suite/output-modulo-time/ltacprof.v | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/flags.ml b/lib/flags.ml index af55e9e2bb..65873e5214 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -231,7 +231,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false -let profile_ltac_cutoff = ref 0.0 +let profile_ltac_cutoff = ref 2.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/test-suite/Makefile b/test-suite/Makefile index a40ea80ae4..d2899034b8 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -51,7 +51,7 @@ SINGLE_QUOTE=" get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1))))) # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1))) -has_profile_ltac_or_compile_flag = $(filter "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) +has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command)) diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v index d79451f0f7..6611db70e2 100644 --- a/test-suite/output-modulo-time/ltacprof.v +++ b/test-suite/output-modulo-time/ltacprof.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *) Ltac sleep' := do 100 (do 100 (do 100 idtac)). Ltac sleep := sleep'. -- cgit v1.2.3 From c4c7aa6d7b14a6d76c287b97d487abe055406577 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 18:28:24 -0400 Subject: LtacProf cutoff is for total percent, not time --- ltac/profile_ltac.ml | 4 +-- test-suite/Makefile | 4 +-- test-suite/output-modulo-time/ltacprof_cutoff.out | 33 +++++++++++++++++++++++ test-suite/output-modulo-time/ltacprof_cutoff.v | 12 +++++++++ 4 files changed, 49 insertions(+), 4 deletions(-) create mode 100644 test-suite/output-modulo-time/ltacprof_cutoff.out create mode 100644 test-suite/output-modulo-time/ltacprof_cutoff.v diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index a91ff98fb9..2514ededb0 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -128,7 +128,7 @@ let to_ltacprof_results xml = | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML") let feedback_results results = - Feedback.(feedback + Feedback.(feedback (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results))) (* ************** pretty printing ************************************* *) @@ -218,7 +218,7 @@ let to_string ~filter ?(cutoff=0.0) node = !global in warn_encountered_multi_success_backtracking (); - let filter s n = filter s && n >= cutoff in + let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in let msg = h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ fnl () ++ diff --git a/test-suite/Makefile b/test-suite/Makefile index a40ea80ae4..e3800ee22e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -304,12 +304,12 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ | grep -v "^" \ - | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ + | sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ > $$tmpoutput; \ - sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ + sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out new file mode 100644 index 0000000000..13cd87b8c2 --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_cutoff.out @@ -0,0 +1,33 @@ +total time: 1.584s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─sleep --------------------------------- 100.0% 100.0% 3 0.572s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s +─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s +└foo1 ---------------------------------- 0.0% 63.9% 1 1.012s + +total time: 1.584s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─sleep --------------------------------- 100.0% 100.0% 3 0.572s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s +─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s +─foo0 ---------------------------------- 0.0% 31.3% 1 0.496s +─constructor --------------------------- 0.0% 0.0% 1 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s + ├─foo1 -------------------------------- 0.0% 63.9% 1 1.012s + │ ├─sleep ----------------------------- 32.6% 32.6% 1 0.516s + │ └─foo0 ------------------------------ 0.0% 31.3% 1 0.496s + │ └sleep ----------------------------- 31.3% 31.3% 1 0.496s + └─sleep ------------------------------- 36.1% 36.1% 1 0.572s +─constructor --------------------------- 0.0% 0.0% 1 0.000s + diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v new file mode 100644 index 0000000000..50131470eb --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -0,0 +1,12 @@ +(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *) +Require Coq.ZArith.BinInt. +Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). + +Ltac foo0 := idtac; sleep. +Ltac foo1 := sleep; foo0. +Ltac foo2 := sleep; foo1. +Goal True. + foo2. + Show Ltac Profile CutOff 47. + constructor. +Qed. -- cgit v1.2.3 From 844b076bf5150a107d31cd4648955c3a6538a34b Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Wed, 28 Sep 2016 10:40:54 +0200 Subject: Fix #4762. --- tactics/eauto.ml4 | 3 ++- test-suite/bugs/closed/4762.v | 24 ++++++++++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4762.v diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index cb206a7dd1..7e37722e93 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -291,7 +291,8 @@ module SearchProblem = struct in let rec_tacs = let l = - filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) + let concl = Reductionops.nf_evar (project g)(pf_concl g) in + filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) concl) in List.map (fun (lgls, cost, pp) -> diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v new file mode 100644 index 0000000000..7a87b07a8e --- /dev/null +++ b/test-suite/bugs/closed/4762.v @@ -0,0 +1,24 @@ +Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q. + +Lemma foo P Q R : R = myand P Q -> P -> Q -> R. +Proof. intros ->; constructor; auto. Qed. + +Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test1. +Qed. + +Hint Extern 0 => + match goal with + | |- myand _ _ => eapply foo; [reflexivity| |] + end : test2. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test2. (* works *) +Qed. + -- cgit v1.2.3 From 627659dd1449d4521132efb1f01ad57b128b235c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 09:50:48 +0200 Subject: Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimpl --- toplevel/vernacentries.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1d6278066a..6c903ce14e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -980,7 +980,8 @@ let warn_arguments_assert = strbrk "If you want to clear notation scopes add ': clear scopes'") let warn_renaming_nonimplicit = - CWarnings.create ~name:"arguments-assert" ~category:"vernacular" + CWarnings.create ~name:"arguments-ignore-rename-nonimpl" + ~category:"vernacular" (fun (oldn, newn) -> strbrk "Ignoring rename of "++pr_id oldn++str" into "++pr_id newn++ strbrk ". Only implicit arguments can be renamed.") -- cgit v1.2.3 From 61112fa8bd336b17f4a2e724c4751c550f27c69a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 09:53:04 +0200 Subject: In <= 8.5 compat accept "Arguments f /" even if f has arguments (#5112) --- toplevel/vernacentries.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6c903ce14e..2e2a60c861 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1012,7 +1012,9 @@ let vernac_declare_arguments locality r l nargs flags = | _::li, _::ld, _::ls -> check li ld ls | _ -> assert false in let () = match l with - | [[]] when List.exists ((<>) `Assert) flags -> () + | [[]] when List.exists ((<>) `Assert) flags || + (* Arguments f /. used to be allowed by mistake *) + (Flags.version_less_or_equal Flags.V8_5 && nargs >= 0) -> () | _ -> List.iter2 (check inf_names) (names :: rest) scopes in -- cgit v1.2.3 From 775b8f28562d1d5063da2b28a06e59610b76f06f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 10:14:10 +0200 Subject: Ignore file names in warning emitted by test-suite/output/* (#5111) --- test-suite/Makefile | 2 +- test-suite/output/Arguments_renaming.out | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index a40ea80ae4..6ecc7bcaad 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -280,7 +280,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ - | grep -v "^" \ + | sed 's/File "[^"]*"/File "stdin"/' \ > $$tmpoutput; \ diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 815305581c..1633ad9765 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,20 +1,20 @@ -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36: +File "stdin", line 1, characters 0-36: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to B. -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +File "stdin", line 2, characters 0-25: Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. -[arguments-assert,vernacular] -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +[arguments-ignore-rename-nonimpl,vernacular] +File "stdin", line 2, characters 0-25: Warning: This command is just asserting the number and names of arguments of identity. If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes' [arguments-assert,vernacular] -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 4, characters 0-40: +File "stdin", line 4, characters 0-40: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -121,9 +121,9 @@ The command has indeed failed with message: Error: Argument z cannot be declared implicit. The command has indeed failed with message: Error: Extra argument y. -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 53, characters 0-26: +File "stdin", line 53, characters 0-26: Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to R. -- cgit v1.2.3 From 69d43e7615f080c2e4e57a87e84b51be857ab678 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 11:08:47 +0200 Subject: Restore code ignoring lines in output (camlp5 warnings) --- test-suite/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/test-suite/Makefile b/test-suite/Makefile index 6ecc7bcaad..acf1dae059 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -280,6 +280,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ + | grep -v "^" \ | sed 's/File "[^"]*"/File "stdin"/' \ > $$tmpoutput; \ diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ -- cgit v1.2.3 From c78af970e1f003587fba9bebdf3ab5ca3b23face Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 30 Sep 2016 12:16:01 +0200 Subject: Fix test-suite. Restore subst output test file modified by mistake. --- test-suite/output/subst.out | 208 -------------------------------------------- test-suite/output/subst.v | 11 --- 2 files changed, 219 deletions(-) diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out index dbb9e09a43..209b2bc26f 100644 --- a/test-suite/output/subst.out +++ b/test-suite/output/subst.out @@ -26,19 +26,6 @@ True 1 subgoal - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - x, y : nat Hx : x = 0 Hy : y = 0 @@ -52,45 +39,6 @@ True 1 subgoal - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - x, z : nat - Hx : x = 0 - Hz : z = 0 - H1 : x = 1 - HA : True - H2 : x = 2 - H3 : 0 = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - H1 : 0 = 1 HA : True H2 : 0 = 2 @@ -101,58 +49,6 @@ True 1 subgoal - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - x, z : nat - Hx : x = 0 - Hz : z = 0 - H1 : x = 1 - HA : True - H2 : x = 2 - H3 : 0 = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - y, z : nat Hy : y = 0 Hz : z = 0 @@ -179,19 +75,6 @@ True 1 subgoal - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - x, y : nat Hx : x = 0 Hy : y = 0 @@ -205,45 +88,6 @@ True 1 subgoal - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - - x, z : nat - Hx : x = 0 - Hz : z = 0 - H1 : x = 1 - HA : True - H2 : x = 2 - HB : True - H4 : z = 4 - H3 : 0 = 3 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - HA, HB : True H4 : 0 = 4 H3 : 0 = 3 @@ -251,55 +95,3 @@ H2 : 0 = 2 ============================ True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - - x, z : nat - Hx : x = 0 - Hz : z = 0 - H1 : x = 1 - HA : True - H2 : x = 2 - HB : True - H4 : z = 4 - H3 : 0 = 3 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v index 91bdd03e02..e48aa6bb28 100644 --- a/test-suite/output/subst.v +++ b/test-suite/output/subst.v @@ -45,15 +45,4 @@ Show. trivial. Qed. -(* A bug revealed by OCaml 4.03 warnings *) -Goal forall y, let x:=0 in y=x -> y=y. -intros * H; -subst. -Fail clear H. (* Was working *) -Abort. -Goal forall y, let x:=0 in y=x -> y=y. -intros * H; -subst. -Fail clear H. (* Was failing before fix *) -Abort. -- cgit v1.2.3 From 98da77db53b4a41062c47f8f55418eb1fbb7e5bb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 16:19:45 +0200 Subject: test-suite/output-modulo-time made more robust Order of items made stable --- test-suite/Makefile | 5 ++++- test-suite/output-modulo-time/ltacprof_cutoff.out | 4 +--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index efa0236c35..b32071e802 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -309,12 +309,15 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ + -e 's/^[^a-zA-Z]*//' \ + | sort \ > $$tmpoutput; \ sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ - $*.out > $$tmpexpected; \ + -e 's/^[^a-zA-Z]*//' \ + $*.out | sort > $$tmpexpected; \ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out index 13cd87b8c2..0cd5777ccf 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.out +++ b/test-suite/output-modulo-time/ltacprof_cutoff.out @@ -2,8 +2,8 @@ total time: 1.584s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep --------------------------------- 100.0% 100.0% 3 0.572s ─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s +─sleep --------------------------------- 100.0% 100.0% 3 0.572s ─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s tactic local total calls max @@ -19,7 +19,6 @@ total time: 1.584s ─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s ─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s ─foo0 ---------------------------------- 0.0% 31.3% 1 0.496s -─constructor --------------------------- 0.0% 0.0% 1 0.000s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ @@ -29,5 +28,4 @@ total time: 1.584s │ └─foo0 ------------------------------ 0.0% 31.3% 1 0.496s │ └sleep ----------------------------- 31.3% 31.3% 1 0.496s └─sleep ------------------------------- 36.1% 36.1% 1 0.572s -─constructor --------------------------- 0.0% 0.0% 1 0.000s -- cgit v1.2.3 From 14427a707f0e97e15e01bb9d297319917a0379f2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 16:20:05 +0200 Subject: coqc: recognize -profile-ltac-cutoff --- tools/coqc.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/coqc.ml b/tools/coqc.ml index ecbbfefac6..b59bbdb1e0 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -107,7 +107,7 @@ let parse_args () = |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" - |"-o" + |"-o"|"-profile-ltac-cutoff" as o) :: rem -> begin match rem with -- cgit v1.2.3 From 024cf5ae087024399cc894b121437d72cd11b480 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 30 Sep 2016 16:42:54 +0200 Subject: Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk. This bug was introduced by 37ab45726, because the new apply_type function was not checking that the new goal was indeed well-typed. We add this check locally in the generalize dependent tactic. --- tactics/tactics.ml | 2 ++ test-suite/bugs/closed/4471.v | 6 ++++++ 2 files changed, 8 insertions(+) create mode 100644 test-suite/bugs/closed/4471.v diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2d901c2dbc..2fe8e0bc34 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2807,6 +2807,8 @@ let old_generalize_dep ?(with_let=false) c gl = in let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) (cl',project gl) in + (** Check that the generalization is indeed well-typed *) + let (evd, _) = Typing.type_of env evd cl'' in let args = Context.Named.to_instance to_quantify_rev in tclTHENLIST [tclEVARS evd; diff --git a/test-suite/bugs/closed/4471.v b/test-suite/bugs/closed/4471.v new file mode 100644 index 0000000000..36efc42d47 --- /dev/null +++ b/test-suite/bugs/closed/4471.v @@ -0,0 +1,6 @@ +Goal forall (A B : Type) (P : forall _ : prod A B, Type) (a : A) (b : B) (p p0 : forall (x : A) (x' : B), P (@pair A B x x')), + @eq (P (@pair A B a b)) (p (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))) + (p0 (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))). +Proof. + intros. + Fail generalize dependent (a, b). -- cgit v1.2.3 From 064de6f6839c4ef963b83018812c5d4113eb2bb9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 30 Sep 2016 17:25:58 +0200 Subject: Fix bug #5045: [generalize] creates ill-typed terms in 8.6. --- tactics/tactics.ml | 2 ++ test-suite/bugs/closed/5045.v | 3 +++ 2 files changed, 5 insertions(+) create mode 100644 test-suite/bugs/closed/5045.v diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2fe8e0bc34..c550df1019 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2821,10 +2821,12 @@ let generalize_dep ?(with_let = false) c = (** *) let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let env = Proofview.Goal.env gl in let newcl, evd = List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr (Tacmach.New.pf_concl gl,Tacmach.New.project gl) in + let (evd, _) = Typing.type_of env evd newcl in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in let tac = apply_type newcl (List.map_filter map lconstr) in Sigma.Unsafe.of_pair (tac, evd) diff --git a/test-suite/bugs/closed/5045.v b/test-suite/bugs/closed/5045.v new file mode 100644 index 0000000000..dc38738d8f --- /dev/null +++ b/test-suite/bugs/closed/5045.v @@ -0,0 +1,3 @@ +Axiom silly : 1 = 1 -> nat -> nat. +Goal forall pf : 1 = 1, silly pf 0 = 0 -> True. + Fail generalize (@eq nat). -- cgit v1.2.3 From 89ec88f1e750cfb786de1929ef44fac70c9a29ab Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 30 Sep 2016 18:45:06 +0200 Subject: Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime. --- tactics/equality.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index b4c027382a..95b3e2b779 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1752,15 +1752,16 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let process hyp = Proofview.Goal.enter begin fun gl -> let gl = Proofview.Goal.assume gl in + let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in let (_,_,c) = pf_get_hyp hyp gl in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else match kind_of_term x, kind_of_term y with - | Var x', _ when not (occur_term x y) -> + | Var x', _ when not (occur_term x y) && not (is_evaluable env (EvalVarRef x')) -> subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (occur_term y x) -> + | _, Var y' when not (occur_term y x) && not (is_evaluable env (EvalVarRef y')) -> subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () -- cgit v1.2.3 From cc407dc4272928944af06ee141d71ff3c9622347 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 1 Oct 2016 08:37:59 +0200 Subject: Micro refactoring: use exact_no_check. This does not affect the semantics of these functions. --- tactics/tactics.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c550df1019..c8cdae53be 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1937,9 +1937,7 @@ let exact_check c = let cast_no_check cast c = Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - Refine.refine ~unsafe:true { run = begin fun sigma -> - Sigma.here (Term.mkCast (c, cast, concl)) sigma - end } + exact_no_check (Term.mkCast (c, cast, concl)) end } let vm_cast_no_check c = cast_no_check Term.VMcast c @@ -1976,7 +1974,7 @@ let assumption = in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> - Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h } + exact_no_check (mkVar (get_id decl)) else arec gl only_eq rest in let assumption_tac = { enter = begin fun gl -> -- cgit v1.2.3 From 2e7c8893e6df7af924dba0291f70dd6fa771cb78 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 29 Sep 2016 18:59:57 +0200 Subject: Speed up the Search commands. The blacklist set was converted into a string list for each item in the environment during a search. In fact, the blacklist was checked for each item, even if the item was already known to be ultimately discarded. This commit fixes both performance issues. First, blacklist_filter is no longer used directly but in two stages. Second, the boolean values are no longer computed before calling the shortcutting operators. It seems like someone had already noticed part of the second issue, since some (but not all) of the boolean values were lazily computed. The speed up becomes noticeable when the blacklist set contains more than four elements. --- toplevel/search.ml | 50 ++++++++++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 24 deletions(-) diff --git a/toplevel/search.ml b/toplevel/search.ml index e670b59b79..921308f78a 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -155,8 +155,9 @@ let full_name_of_reference ref = DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) -let blacklist_filter ref env typ = +let blacklist_filter_aux () = let l = SearchBlacklist.elements () in + fun ref env typ -> let name = full_name_of_reference ref in let is_not_bl str = not (String.string_contains ~where:name ~what:str) in List.for_all is_not_bl l @@ -182,11 +183,11 @@ let search_about_filter query gr env typ = match query with let search_pattern gopt pat mods = let ans = ref [] in + let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = - let f_module = module_filter mods ref env typ in - let f_blacklist = blacklist_filter ref env typ in - let f_pattern () = pattern_filter pat ref env typ in - f_module && f_pattern () && f_blacklist + module_filter mods ref env typ && + pattern_filter pat ref env typ && + blacklist_filter ref env typ in let iter ref env typ = if filter ref env typ then plain_display ans ref env typ @@ -208,14 +209,12 @@ let search_rewrite gopt pat mods = let pat1 = rewrite_pat1 pat in let pat2 = rewrite_pat2 pat in let ans = ref [] in + let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = - let f_module = module_filter mods ref env typ in - let f_blacklist = blacklist_filter ref env typ in - let f_pattern () = - pattern_filter pat1 ref env typ || - pattern_filter pat2 ref env typ - in - f_module && f_pattern () && f_blacklist + module_filter mods ref env typ && + (pattern_filter pat1 ref env typ || + pattern_filter pat2 ref env typ) && + blacklist_filter ref env typ in let iter ref env typ = if filter ref env typ then plain_display ans ref env typ @@ -227,11 +226,11 @@ let search_rewrite gopt pat mods = let search_by_head gopt pat mods = let ans = ref [] in + let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = - let f_module = module_filter mods ref env typ in - let f_blacklist = blacklist_filter ref env typ in - let f_pattern () = head_filter pat ref env typ in - f_module && f_pattern () && f_blacklist + module_filter mods ref env typ && + head_filter pat ref env typ && + blacklist_filter ref env typ in let iter ref env typ = if filter ref env typ then plain_display ans ref env typ @@ -243,12 +242,13 @@ let search_by_head gopt pat mods = let search_about gopt items mods = let ans = ref [] in + let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in - let f_module = module_filter mods ref env typ in - let f_about (b, i) = eqb b (search_about_filter i ref env typ) in - let f_blacklist = blacklist_filter ref env typ in - f_module && List.for_all f_about items && f_blacklist + module_filter mods ref env typ && + List.for_all + (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items && + blacklist_filter ref env typ in let iter ref env typ = if filter ref env typ then plain_display ans ref env typ @@ -287,6 +287,7 @@ let interface_search = let (name, tpe, subtpe, mods, blacklist) = extract_flags [] [] [] [] false flags in + let blacklist_filter = blacklist_filter_aux () in let filter_function ref env constr = let id = Names.Id.to_string (Nametab.basename_of_global ref) in let path = Libnames.dirpath (Nametab.path_of_global ref) in @@ -305,13 +306,11 @@ let interface_search = let match_module (mdl, flag) = toggle (Libnames.is_dirpath_prefix_of mdl path) flag in - let in_blacklist = - blacklist || (blacklist_filter ref env constr) - in List.for_all match_name name && List.for_all match_type tpe && List.for_all match_subtype subtpe && - List.for_all match_module mods && in_blacklist + List.for_all match_module mods && + (blacklist || blacklist_filter ref env constr) in let ans = ref [] in let print_function ref env constr = @@ -342,3 +341,6 @@ let interface_search = in let () = generic_search glnum iter in !ans + +let blacklist_filter ref env typ = + blacklist_filter_aux () ref env typ -- cgit v1.2.3 From acbe712fd643516ff63ecfe3e106deb695dbd9b3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Oct 2016 21:37:16 +0200 Subject: Fix bug #4661: Cannot mask the absolute name. The patch is quite dumb: it essentially consists in alpha-renaming bound module names when printing a functor, by checking that the name was not already present, and generating a fresh one otherwise. --- printing/printmod.ml | 17 +++++++++++------ test-suite/bugs/closed/4661.v | 10 ++++++++++ test-suite/output/PrintModule.out | 1 + test-suite/output/PrintModule.v | 16 ++++++++++++++++ 4 files changed, 38 insertions(+), 6 deletions(-) create mode 100644 test-suite/bugs/closed/4661.v diff --git a/printing/printmod.ml b/printing/printmod.ml index c939f54e80..dfa66d4376 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -247,19 +247,24 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with | _ -> raise Not_found let nametab_register_modparam mbid mtb = + let id = MBId.to_id mbid in match mtb.mod_type with - | MoreFunctor _ -> () (* functorial param : nothing to register *) + | MoreFunctor _ -> id (* functorial param : nothing to register *) | NoFunctor struc -> (* We first try to use the algebraic type expression if any, via a Declaremods function that converts back to module entries *) try - Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) + let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in + id with e when CErrors.noncritical e -> (* Otherwise, we try to play with the nametab ourselves *) let mp = MPbound mbid in - let dir = DirPath.make [MBId.to_id mbid] in + let check id = Nametab.exists_dir (DirPath.make [id]) in + let id = Namegen.next_ident_away_from id check in + let dir = DirPath.make [id] in nametab_register_dir mp; - List.iter (nametab_register_body mp dir) struc + List.iter (nametab_register_body mp dir) struc; + id let print_body is_impl env mp (l,body) = let name = pr_label l in @@ -353,7 +358,7 @@ let print_mod_expr env mp locals = function let rec print_functor fty fatom is_type env mp locals = function |NoFunctor me -> fatom is_type env mp locals me |MoreFunctor (mbid,mtb1,me2) -> - nametab_register_modparam mbid mtb1; + let id = nametab_register_modparam mbid mtb1 in let mp1 = MPbound mbid in let pr_mtb1 = fty env mp1 locals mtb1 in let env' = Option.map (Modops.add_module_type mp1 mtb1) env in @@ -361,7 +366,7 @@ let rec print_functor fty fatom is_type env mp locals = function let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ - str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++ + str "(" ++ pr_id id ++ str ":" ++ pr_mtb1 ++ str ")" ++ spc() ++ print_functor fty fatom is_type env' mp locals' me2) let rec print_expression x = diff --git a/test-suite/bugs/closed/4661.v b/test-suite/bugs/closed/4661.v new file mode 100644 index 0000000000..03d2350a69 --- /dev/null +++ b/test-suite/bugs/closed/4661.v @@ -0,0 +1,10 @@ +Module Type Test. + Parameter t : Type. +End Test. + +Module Type Func (T:Test). + Parameter x : Type. +End Func. + +Module Shortest_path (T : Test). +Print Func. diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out index db464fd07e..751d5fcc48 100644 --- a/test-suite/output/PrintModule.out +++ b/test-suite/output/PrintModule.out @@ -2,3 +2,4 @@ Module N : S with Definition T := nat := M Module N : S with Module T := K := M +Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v index 999d9a9862..5f30f7cda6 100644 --- a/test-suite/output/PrintModule.v +++ b/test-suite/output/PrintModule.v @@ -32,3 +32,19 @@ Module N : S with Module T := K := M. Print Module N. End BAR. + +Module QUX. + +Module Type Test. + Parameter t : Type. +End Test. + +Module Type Func (T:Test). + Parameter x : T.t. +End Func. + +Module Shortest_path (T : Test). +Print Func. +End Shortest_path. + +End QUX. -- cgit v1.2.3 From 109e05059692d0f2f15a4b1699ff4a25d07e5a79 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 2 Oct 2016 01:42:29 +0200 Subject: Fix bug #5087: Improve the error message on record with duplicated fields. --- interp/constrintern.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4502aa7ace..f98873aa66 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1061,6 +1061,15 @@ let find_pattern_variable = function | Ident (loc,id) -> id | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) +let check_duplicate loc fields = + let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in + let dups = List.duplicates eq fields in + match dups with + | [] -> () + | (r, _) :: _ -> + user_err_loc (loc, "", str "This record defines several times the field " ++ + pr_reference r ++ str ".") + (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] are fields of a record and [e1] are "values" (either terms, when @@ -1094,6 +1103,7 @@ let sort_fields ~complete loc fields completer = try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) with Not_found -> anomaly (str "Environment corruption for records") in + let () = check_duplicate loc fields in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) -- cgit v1.2.3 From 527d3525b726f8136b64c7c1cf770c702f966cad Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 2 Oct 2016 02:01:19 +0200 Subject: Fix bug #5069: Scheme Equality gives anomalies in sections. --- toplevel/auto_ind_decl.ml | 12 +++++++++--- toplevel/auto_ind_decl.mli | 2 +- toplevel/indschemes.ml | 2 +- 3 files changed, 11 insertions(+), 5 deletions(-) diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 180b836ea5..0561fc4b82 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -54,7 +54,7 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of constant +exception ParameterWithoutEquality of global_reference exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported @@ -181,7 +181,13 @@ let build_beq_scheme mode kn = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in match kind_of_term c with | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants - | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants + | Var x -> + let eid = id_of_string ("eq_"^(string_of_id x)) in + let () = + try ignore (Environ.lookup_named eid env) + with Not_found -> raise (ParameterWithoutEquality (VarRef x)) + in + mkVar eid, Safe_typing.empty_private_constants | Cast (x,_,_) -> aux (applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> @@ -209,7 +215,7 @@ let build_beq_scheme mode kn = | LetIn _ -> raise (EqUnknown "LetIn") | Const kn -> (match Environ.constant_opt_value_in env kn with - | None -> raise (ParameterWithoutEquality (fst kn)) + | None -> raise (ParameterWithoutEquality (ConstRef (fst kn))) | Some c -> aux (applist (c,a))) | Proj _ -> raise (EqUnknown "Proj") | Construct _ -> raise (EqUnknown "Construct") diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index b6c66a1e84..fa5c61484e 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -21,7 +21,7 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of constant +exception ParameterWithoutEquality of Globnames.global_reference exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index f9e6c207c3..e8ea617f45 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -161,7 +161,7 @@ let try_declare_scheme what f internal names kn = let msg = match fst e with | ParameterWithoutEquality cst -> alarm what internal - (str "Boolean equality not found for parameter " ++ pr_con cst ++ + (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++ str".") | InductiveWithProduct -> alarm what internal -- cgit v1.2.3 From 466b7e69e49a5f4bba36b834a2e046f120ece07c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 2 Oct 2016 12:02:53 +0200 Subject: Move bullet detection from lexer to parser (bug #5102). That way, bullet detection no longer depends on a global variable indicating whether a line is starting. This causes a small change in the recognized language. Before the commit, "--++" was recognized as a bullet "--" followed by a keyword "++" when at the start of a line; now it is always recognized as a keyword "--++". This also fixes a bug in Tok.to_string as a side-effect. --- parsing/cLexer.ml4 | 14 -------------- parsing/compat.ml4 | 1 - parsing/g_vernac.ml4 | 35 +++++++++++++++++++---------------- parsing/tok.ml | 7 ------- parsing/tok.mli | 1 - 5 files changed, 19 insertions(+), 39 deletions(-) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index bec891f7f1..fcdc37c08b 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -479,14 +479,6 @@ let find_keyword loc id s = | None -> raise Not_found | Some c -> KEYWORD c -let process_sequence loc bp c cs = - let rec aux n cs = - match Stream.peek cs with - | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs - | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs) - in - aux 1 cs - (* Must be a special token *) let process_chars loc bp c cs = let t = progress_from_byte loc None (-1) !token_tree cs c in @@ -552,12 +544,6 @@ let rec next_token loc = parser bp | _ -> () in (t, set_loc_pos loc bp ep) - | [< ' ('-'|'+'|'*' as c); s >] -> - let t,new_between_com = - if !between_com then process_sequence loc bp c s, true - else process_chars loc bp c s,false - in - comment_stop bp; between_com := new_between_com; t | [< ''?'; s >] ep -> let t = parse_after_qmark loc bp s in comment_stop bp; (t, set_loc_pos loc ep bp) diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 18bc8d664f..5635eac7ab 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -259,7 +259,6 @@ IFDEF CAMLP5 THEN | Tok.INT s -> "INT", s | Tok.STRING s -> "STRING", s | Tok.LEFTQMARK -> "LEFTQMARK", "" - | Tok.BULLET s -> "BULLET", s | Tok.EOI -> "EOI", "" in Gramext.Stoken pattern diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 50e469dd2a..0f450ff9cb 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -33,8 +33,6 @@ let _ = List.iter CLexer.add_keyword vernac_kw let query_command = Gram.entry_create "vernac:query_command" -let subprf = Gram.entry_create "vernac:subprf" - let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" let thm_token = Gram.entry_create "vernac:thm_token" let def_body = Gram.entry_create "vernac:def_body" @@ -45,13 +43,25 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" -let make_bullet s = - let n = String.length s in - match s.[0] with - | '-' -> Dash n - | '+' -> Plus n - | '*' -> Star n - | _ -> assert false +let subprf = Gram.Entry.of_parser "vernac:subprf" (fun strm -> + match get_tok (Stream.peek strm) with + | Some (KEYWORD "{") -> Stream.junk strm; VernacSubproof None + | Some (KEYWORD "}") -> Stream.junk strm; VernacEndSubproof + | Some (KEYWORD k) -> + (match k.[0] with + | ('-'|'+'|'*') as c -> + let n = String.length k in + for i = 1 to n - 1 do + if k.[i] != c then raise Stream.Failure + done; + Stream.junk strm; + VernacBullet (match c with + | '-' -> Dash n + | '+' -> Plus n + | '*' -> Star n + | _ -> assert false) + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) GEXTEND Gram GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; @@ -102,13 +112,6 @@ GEXTEND Gram [ [ c = subgoal_command -> c None] ] ; - subprf: - [ [ s = BULLET -> VernacBullet (make_bullet s) - | "{" -> VernacSubproof None - | "}" -> VernacEndSubproof - ] ] - ; - subgoal_command: [ [ c = query_command; "." -> begin function diff --git a/parsing/tok.ml b/parsing/tok.ml index 8ae1065120..99d5c972c9 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -18,7 +18,6 @@ type t = | INT of string | STRING of string | LEFTQMARK - | BULLET of string | EOI let equal t1 t2 = match t1, t2 with @@ -30,7 +29,6 @@ let equal t1 t2 = match t1, t2 with | INT s1, INT s2 -> string_equal s1 s2 | STRING s1, STRING s2 -> string_equal s1 s2 | LEFTQMARK, LEFTQMARK -> true -| BULLET s1, BULLET s2 -> string_equal s1 s2 | EOI, EOI -> true | _ -> false @@ -42,7 +40,6 @@ let extract_string = function | FIELD s -> s | INT s -> s | LEFTQMARK -> "?" - | BULLET s -> s | EOI -> "" let to_string = function @@ -53,7 +50,6 @@ let to_string = function | INT s -> Format.sprintf "INT %s" s | STRING s -> Format.sprintf "STRING %S" s | LEFTQMARK -> "LEFTQMARK" - | BULLET s -> Format.sprintf "STRING %S" s | EOI -> "EOI" let match_keyword kwd = function @@ -75,7 +71,6 @@ let of_pattern = function | "INT", s -> INT s | "STRING", s -> STRING s | "LEFTQMARK", _ -> LEFTQMARK - | "BULLET", s -> BULLET s | "EOI", _ -> EOI | _ -> failwith "Tok.of_pattern: not a constructor" @@ -87,7 +82,6 @@ let to_pattern = function | INT s -> "INT", s | STRING s -> "STRING", s | LEFTQMARK -> "LEFTQMARK", "" - | BULLET s -> "BULLET", s | EOI -> "EOI", "" let match_pattern = @@ -100,7 +94,6 @@ let match_pattern = | "INT", "" -> (function INT s -> s | _ -> err ()) | "STRING", "" -> (function STRING s -> s | _ -> err ()) | "LEFTQMARK", "" -> (function LEFTQMARK -> "" | _ -> err ()) - | "BULLET", "" -> (function BULLET s -> s | _ -> err ()) | "EOI", "" -> (function EOI -> "" | _ -> err ()) | pat -> let tok = of_pattern pat in diff --git a/parsing/tok.mli b/parsing/tok.mli index b9286c53e2..b1e79dc90d 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -16,7 +16,6 @@ type t = | INT of string | STRING of string | LEFTQMARK - | BULLET of string | EOI val equal : t -> t -> bool -- cgit v1.2.3