From d5cbd7b881dcc8b3599b3330e342f0aa55ef467f Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Fri, 8 Apr 2016 14:48:34 +0100 Subject: Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v The extraction of [Z] into Ocaml's [Big_int] passed arguments in the wrong order to [Big.compare_case] for [Pos.compare_cont]. It seems unlikely this ever worked before. --- plugins/extraction/ExtrOcamlZBigInt.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index 9a1a4aa01b..c9e8eac0c5 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -46,7 +46,7 @@ Extract Constant Pos.max => "Big.max". Extract Constant Pos.compare => "fun x y -> Big.compare_case Eq Lt Gt x y". Extract Constant Pos.compare_cont => - "fun x y c -> Big.compare_case c Lt Gt x y". + "fun c x y -> Big.compare_case c Lt Gt x y". Extract Constant N.add => "Big.add". Extract Constant N.succ => "Big.succ". -- cgit v1.2.3 From 4b4fc278887d33299aea32aceea93e9849a65855 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 30 Mar 2016 17:34:44 +0200 Subject: TYPOGRAPHY: adding missing \noindent macros --- doc/refman/RefMan-cic.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 1554ee04d3..50f4dc1330 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -552,14 +552,14 @@ The declaration for parameterized lists is: \end{array}\right]} \vskip.5em -which corresponds to the result of the \Coq\ declaration: +\noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} Inductive list (A:Set) : Set := | nil : list A | cons : A -> list A -> list A. \end{coq_example*} -The declaration for a mutual inductive definition of forests and trees is: +\noindent The declaration for a mutual inductive definition of forests and trees is: \vskip.5em \ind{}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]} {\left[\begin{array}{r \colon l} @@ -569,7 +569,7 @@ The declaration for a mutual inductive definition of forests and trees is: \end{array}\right]} \vskip.5em -which corresponds to the result of the \Coq\ +\noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} Inductive tree : Set := @@ -579,7 +579,7 @@ with forest : Set := | consf : tree -> forest -> forest. \end{coq_example*} -The declaration for a mutual inductive definition of even and odd is: +\noindent The declaration for a mutual inductive definition of even and odd is: \newcommand\GammaI{\left[\begin{array}{r \colon l} \even & \nat\ra\Prop \\ \odd & \nat\ra\Prop @@ -594,7 +594,7 @@ The declaration for a mutual inductive definition of even and odd is: \vskip.5em \ind{1}{\GammaI}{\GammaC} \vskip.5em -which corresponds to the result of the \Coq\ +\noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} Inductive even : nat -> Prop := -- cgit v1.2.3 From 2bd36760f84f1d79af63cdee4d5d53f289a51204 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 12 Apr 2016 17:17:18 +0200 Subject: FIX: HTML version of Chapter 4 of the Reference Manual --- doc/common/macros.tex | 4 +- doc/refman/RefMan-cic.tex | 257 ++++++++++++++++++++++++++++++++++++---------- 2 files changed, 202 insertions(+), 59 deletions(-) diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 3b12f259b6..bbc78a8517 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -405,8 +405,8 @@ \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](\begin{array}[t]{@{}l@{}}#3:=#4 \,)\end{array}$}} %END LATEX -%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}} -%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}} +%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#2\,:=\,#3)$}} +%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](#3\,:=\,#4)$}} \newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4 \,)\end{array}$}} diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 50f4dc1330..b9c17d8148 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -544,14 +544,43 @@ $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of param \def\colon{@{\hskip.5em:\hskip.5em}} The declaration for parameterized lists is: +\begin{latexonly} \vskip.5em -\ind{1}{\List:\Set\ra\Set}{\left[\begin{array}{r \colon l} - \Nil & \forall A:\Set,\List~A \\ - \cons & \forall A:\Set, A \ra \List~A \ra \List~A - \end{array}\right]} +\ind{1}{[\List:\Set\ra\Set]}{\left[\begin{array}{r \colon l} + \Nil & \forall A:\Set,\List~A \\ + \cons & \forall A:\Set, A \ra \List~A \ra \List~A + \end{array} + \right]} \vskip.5em - +\end{latexonly} +\begin{rawhtml}

+  
+    
+    
+    
+    
+    
+    
+    
+    
+    
+  
+
Ind[1]⎛
⎝		[ list : Set → Set ]:=⎡
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
nil:=∀A : Set, list A
cons:=∀A : Set, A → list A → list A

+    		⎤
⎦		⎞
⎠
+\end{rawhtml} \noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} Inductive list (A:Set) : Set := @@ -559,16 +588,64 @@ Inductive list (A:Set) : Set := | cons : A -> list A -> list A. \end{coq_example*} -\noindent The declaration for a mutual inductive definition of forests and trees is: +\noindent The declaration for a mutual inductive definition of {\tree} and {\forest} is: +\begin{latexonly} \vskip.5em -\ind{}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]} - {\left[\begin{array}{r \colon l} - \node & \forest \ra \tree\\ - \emptyf & \forest\\ - \consf & \tree \ra \forest \ra \forest\\ - \end{array}\right]} +\ind{~}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]} + {\left[\begin{array}{r \colon l} + \node & \forest \ra \tree\\ + \emptyf & \forest\\ + \consf & \tree \ra \forest \ra \forest\\ + \end{array}\right]} \vskip.5em - +\end{latexonly} +\begin{rawhtml}

+  
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+  
+
Ind[1]⎛
⎜
⎝		⎡
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
tree:Set
forest:Set

+    		⎤
⎦		:=⎡
⎢
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
node:forest → tree
emptyf:forest
consf:tree → forest → forest

+    		⎤
⎥
⎦		⎞
⎟
⎠
+\end{rawhtml} \noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} @@ -579,7 +656,8 @@ with forest : Set := | consf : tree -> forest -> forest. \end{coq_example*} -\noindent The declaration for a mutual inductive definition of even and odd is: +\noindent The declaration for a mutual inductive definition of {\even} and {\odd} is: +\begin{latexonly} \newcommand\GammaI{\left[\begin{array}{r \colon l} \even & \nat\ra\Prop \\ \odd & \nat\ra\Prop @@ -594,6 +672,54 @@ with forest : Set := \vskip.5em \ind{1}{\GammaI}{\GammaC} \vskip.5em +\end{latexonly} +\begin{rawhtml}

+  
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+  
+
Ind[1]⎛
⎜
⎝		⎡
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
even:nat → Prop
odd:nat → Prop

+    		⎤
⎦		:=⎡
⎢
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
even_O:even O
even_S:∀n : nat, odd n → even (S n)
odd_S:∀n : nat, even n → odd (S n)

+    		⎤
⎥
⎦		⎞
⎟
⎠
+\end{rawhtml} \noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} @@ -610,9 +736,9 @@ contains an inductive declaration. \begin{description} \item[Ind] \index{Typing rules!Ind} - \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(a:A)\in\Gamma_I}{\WTEG{a}{A}}} + \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(a:A)\in\Gamma_I}{\WTEG{a}{A}}} \item[Constr] \index{Typing rules!Constr} - \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(c:C)\in\Gamma_C}{\WTEG{c}{C}}} + \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(c:C)\in\Gamma_C}{\WTEG{c}{C}}} \end{description} \begin{latexonly}% @@ -726,19 +852,16 @@ any $u_i$ the type $V$ satisfies the nested positivity condition for $X$ \end{itemize} -%% \begin{latexonly}% - \newcommand\vv{\textSFxi} % │ - \newcommand\hh{\textSFx} % ─ - \newcommand\vh{\textSFviii} % ├ - \newcommand\hv{\textSFii} % └ - \newlength\framecharacterwidth - \settowidth\framecharacterwidth{\hh} - \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth} - \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}} -%% \def\captionstrut{\vbox to 1.5em{}} +\newcommand\vv{\textSFxi} % │ +\newcommand\hh{\textSFx} % ─ +\newcommand\vh{\textSFviii} % ├ +\newcommand\hv{\textSFii} % └ +\newlength\framecharacterwidth +\settowidth\framecharacterwidth{\hh} +\newcommand\ws{\hbox{}\hskip\the\framecharacterwidth} +\newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}} -%% \begin{figure}[H] -For instance, if one considers the type +\noindent For instance, if one considers the type \begin{verbatim} Inductive tree (A:Type) : Type := @@ -746,29 +869,49 @@ Inductive tree (A:Type) : Type := | node : A -> (nat -> tree A) -> tree A \end{verbatim} -Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$ - +\begin{latexonly} +\noindent Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$\\ \noindent - \ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\ - \ws\ws\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\ - \ws\ws\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\ - \ws\ws\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\ - \ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1 -%% \caption{\captionstrut A proof that $X$ occurs strictly positively in $\ListA$} -%% \end{figure} -%% \end{latexonly}% +\ws\ws\vv\\ +\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\ +\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\ +\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\ +\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\ +\ws\ws\vv\\ +\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\ +\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\ +\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1 +\end{latexonly} +\begin{rawhtml} +
+Then every instantiated constructor of list A satisfies the nested positivity condition for list
+  │
+  ├─ concerning type list A of constructor nil:
+  │    Type list A of constructor nil satisfies the positivity condition for list
+  │    because list does not appear in any (real) arguments of the type of that constructor
+  │    (primarily because list does not have any (real) arguments) ... (bullet 1)
+  │
+  ╰─ concerning type ∀ A → list A → list A of constructor cons:
+       Type ∀ A : Type, A → list A → list A of constructor cons
+       satisfies the positivity condition for list because:
+       │
+       ├─ list occurs only strictly positively in Type ... (bullet 3)
+       │
+       ├─ list occurs only strictly positively in A ... (bullet 3)
+       │
+       ├─ list occurs only strictly positively in list A ... (bullet 4)
+       │
+       ╰─ list satisfies the positivity condition for list A ... (bullet 1)
+
+\end{rawhtml} \paragraph{Correctness rules.} We shall now describe the rules allowing the introduction of a new @@ -783,7 +926,7 @@ inductive definition. \inference{ \frac{ (\WTE{\Gamma_P}{A_j}{s'_j})_{j=1\ldots k} - ~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots n} + ~~~~~~~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots n} } {\WF{E;\Ind{}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}} provided that the following side conditions hold: @@ -811,23 +954,23 @@ inductive definition. The following declaration introduces the second-order existential quantifier $\exists X.P(X)$. \begin{coq_example*} -Inductive exProp (P:Prop->Prop) : Prop - := exP_intro : forall X:Prop, P X -> exProp P. +Inductive exProp (P:Prop->Prop) : Prop := + exP_intro : forall X:Prop, P X -> exProp P. \end{coq_example*} The same definition on \Set{} is not allowed and fails: % (********** The following is not correct and should produce **********) % (*** Error: Large non-propositional inductive types must be in Type***) \begin{coq_example} -Fail Inductive exSet (P:Set->Prop) : Set - := exS_intro : forall X:Set, P X -> exSet P. +Fail Inductive exSet (P:Set->Prop) : Set := + exS_intro : forall X:Set, P X -> exSet P. \end{coq_example} It is possible to declare the same inductive definition in the universe \Type. The \texttt{exType} inductive definition has type $(\Type_i \ra\Prop)\ra \Type_j$ with the constraint that the parameter \texttt{X} of \texttt{exT\_intro} has type $\Type_k$ with $kProp) : Type - := exT_intro : forall X:Type, P X -> exType P. +Inductive exType (P:Type->Prop) : Type := + exT_intro : forall X:Type, P X -> exType P. \end{coq_example*} %We shall assume for the following definitions that, if necessary, we %annotated the type of constructors such that we know if the argument -- cgit v1.2.3 From 927e88de465e94bf18b970b45faaf97b4c2dff82 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 12 Apr 2016 18:59:55 +0200 Subject: Quick fix for #4603 (part 2): Anomaly: Universe undefined This is a follow-up on Matthieu's 7e7b5684 The Definition command was classified incorrectly when a body was provided. This fix is a bit ad-hoc. A better one would require more expressiveness in side effect classification, but I'll do it in trunk only since it could impact plugins. Thanks a lot to Enrico for his help! --- stm/stm.ml | 6 +++++- test-suite/bugs/closed/4603.v | 10 ++++++++++ 2 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4603.v diff --git a/stm/stm.ml b/stm/stm.ml index a6d119f0cd..094457431e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2250,7 +2250,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue}); - VCS.propagate_sideff (Some x); + let replay = match x.expr with + | VernacDefinition(_, _, DefineBody _) -> None + | _ -> Some x + in + VCS.propagate_sideff replay; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); `Ok diff --git a/test-suite/bugs/closed/4603.v b/test-suite/bugs/closed/4603.v new file mode 100644 index 0000000000..e7567623a6 --- /dev/null +++ b/test-suite/bugs/closed/4603.v @@ -0,0 +1,10 @@ +Axiom A : Type. + +Goal True. exact I. +Check (fun P => P A). +Abort. + +Goal True. +Definition foo (A : Type) : Prop:= True. + set (x:=foo). split. +Qed. \ No newline at end of file -- cgit v1.2.3 From 3a54bb00dd2420b2710c2f90e1c0c4cf9c267175 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Apr 2016 20:33:51 +0200 Subject: A fix to #4666 (Exc_located capsule added by camlp5 overwriting location set by lexer). This improves on abb4e7b0c by recovering the lexer location. AFAICS, it has an effect on lexer's errors Unterminated_comment and Unterminated_string. The other errors were not wrongly located, presumably because the Exc_located location added by camlp5 coincided with the location given by the lexer. --- parsing/compat.ml4 | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index d1d55c81fe..17038ab5fc 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -193,7 +193,11 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct let entry_create = Entry.create let entry_parse e p = try Entry.parse e p - with Exc_located (loc,e) -> Loc.raise (to_coqloc loc) e + with Exc_located (loc,e) -> + let loc' = Loc.get_loc (Exninfo.info e) in + let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in + Loc.raise loc e + IFDEF CAMLP5_6_02_1 THEN let entry_print ft x = Entry.print ft x ELSE -- cgit v1.2.3 From 08dbef1f220c3f97ad1baa159b9f0a6913e922b3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 8 Apr 2016 21:32:59 +0200 Subject: Build stm debugging messages lazily so that they are not silently computed when not in debugging mode (especially those printing a command). --- stm/stm.ml | 52 ++++++++++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index 094457431e..bec9d18d51 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -8,8 +8,8 @@ let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr -let prerr_endline s = if false then begin pr_err s end else () -let prerr_debug s = if !Flags.debug then begin pr_err s end else () +let prerr_endline s = if false then begin pr_err (s ()) end else () +let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else () open Vernacexpr open Errors @@ -104,11 +104,11 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el | _ -> false in if internal_command expr then begin - prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) + prerr_endline (fun () -> "ignoring " ^ string_of_ppcmds(pr_vernac expr)) end else begin set_id_for_feedback ?route (Feedback.State id); Aux_file.record_in_aux_set_at loc; - prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr)); + prerr_endline (fun () -> "interpreting " ^ string_of_ppcmds(pr_vernac expr)); try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)) with e -> let e = Errors.push e in @@ -478,7 +478,7 @@ end = struct (* {{{ *) let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in checkout branch; - prerr_endline ("mode:" ^ mode); + prerr_endline (fun () -> "mode:" ^ mode); Proof_global.activate_proof_mode mode with Failure _ -> checkout Branch.master; @@ -744,7 +744,7 @@ end = struct (* {{{ *) if is_cached id && not redefine then anomaly (str"defining state "++str str_id++str" twice"); try - prerr_endline("defining "^str_id^" (cache="^ + prerr_endline (fun () -> "defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); let good_id = match safe_id with None -> !cur_id | Some id -> id in fix_exn_ref := exn_on id ~valid:good_id; @@ -752,7 +752,7 @@ end = struct (* {{{ *) fix_exn_ref := (fun x -> x); if cache = `Yes then freeze `No id else if cache = `Shallow then freeze `Shallow id; - prerr_endline ("setting cur id to "^str_id); + prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then Hooks.(call state_computed id ~in_cache:false); @@ -1134,8 +1134,8 @@ end = struct (* {{{ *) | Some (safe, err) -> err, safe | None -> Stateid.dummy, Stateid.dummy in let e_msg = iprint (e, info) in - prerr_endline "failed with the following exception:"; - prerr_endline (string_of_ppcmds e_msg); + prerr_endline (fun () -> "failed with the following exception:"); + prerr_endline (fun () -> string_of_ppcmds e_msg); let e_safe_states = List.filter State.is_cached my_states in RespError { e_error_at; e_safe_id; e_msg; e_safe_states } @@ -1400,7 +1400,7 @@ end = struct (* {{{ *) | Some (ReqBuildProof (r, b, _)) -> Some(r, b) | _ -> None) tasks in - prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length reqs)); + prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs)); reqs let reset_task_queue () = TaskQueue.clear (Option.get !queue) @@ -1567,7 +1567,7 @@ end = struct (* {{{ *) with Not_found -> Errors.anomaly(str"Partac: wrong focus") in if Future.is_over f then let pt, uc = Future.join f in - prerr_endline (string_of_ppcmds(hov 0 ( + prerr_endline (fun () -> string_of_ppcmds(hov 0 ( str"g=" ++ str gid ++ spc () ++ str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ str"uc=" ++ Evd.pr_evar_universe_context uc))); @@ -1679,7 +1679,7 @@ let delegate name = || !Flags.async_proofs_full let collect_proof keep cur hd brkind id = - prerr_endline ("Collecting proof ending at "^Stateid.to_string id); + prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in let name = function | [] -> no_name @@ -1780,7 +1780,7 @@ let string_of_reason = function | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section" | `Unknown -> "unsupported case" -let log_string s = prerr_debug ("STM: " ^ s) +let log_string s = prerr_debug (fun () -> "STM: " ^ s) let log_processing_async id name = log_string Printf.(sprintf "%s: proof %s: asynch" (Stateid.to_string id) name ) @@ -1802,17 +1802,17 @@ let known_state ?(redefine_qed=false) ~cache id = Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate id = Future.purify (fun id -> - prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id); + prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); reach id; cherry_pick_non_pstate ()) id (* traverses the dag backward from nodes being already calculated *) and reach ?(redefine_qed=false) ?(cache=cache) id = - prerr_endline ("reaching: " ^ Stateid.to_string id); + prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin State.install_cached id; Hooks.(call state_computed id ~in_cache:true); - prerr_endline ("reached (cache)") + prerr_endline (fun () -> "reached (cache)") end else let step, cache_step, feedback_processed = let view = VCS.visit id in @@ -1950,7 +1950,7 @@ let known_state ?(redefine_qed=false) ~cache id = else cache_step in State.define ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; - prerr_endline ("reached: "^ Stateid.to_string id) in + prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in reach ~redefine_qed id end (* }}} *) @@ -1965,7 +1965,7 @@ let init () = Backtrack.record (); Slaves.init (); if Flags.async_proofs_is_master () then begin - prerr_endline "Initializing workers"; + prerr_endline (fun () -> "Initializing workers"); Query.init (); let opts = match !Flags.async_proofs_private_flags with | None -> [] @@ -2017,9 +2017,9 @@ let rec join_admitted_proofs id = let join () = finish (); wait (); - prerr_endline "Joining the environment"; + prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); - prerr_endline "Joining Admitted proofs"; + prerr_endline (fun () -> "Joining Admitted proofs"); join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); VCS.print (); VCS.print () @@ -2095,7 +2095,7 @@ let handle_failure (e, info) vcs tty = anomaly(str"error with no safe_id attached:" ++ spc() ++ Errors.iprint_no_report (e, info)) | Some (safe_id, id) -> - prerr_endline ("Failed at state " ^ Stateid.to_string id); + prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; if tty && interactive () = `Yes then begin (* We stay on a valid state *) @@ -2120,13 +2120,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let warn_if_pos a b = if b then msg_warning(pr_ast a ++ str" should not be part of a script") in let v, x = expr, { verbose = verbose; loc; expr } in - prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x)); + prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); let vcs = VCS.backup () in try let head = VCS.current_branch () in VCS.checkout head; let rc = begin - prerr_endline (" classified as: " ^ string_of_vernac_classification c); + prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with (* PG stuff *) | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok @@ -2162,7 +2162,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> - prerr_endline ("undo to state " ^ Stateid.to_string id); + prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); Reach.known_state ~cache:(interactive ()) id; `Ok @@ -2301,7 +2301,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = expr = VernacShow (ShowGoal OpenSubgoals) } | _ -> () end; - prerr_endline "processed }}}"; + prerr_endline (fun () -> "processed }}}"); VCS.print (); rc with e -> @@ -2479,7 +2479,7 @@ let edit_at id = anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ Errors.print_no_report e) | Some (_, id) -> - prerr_endline ("Failed at state " ^ Stateid.to_string id); + prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; VCS.print (); iraise (e, info) -- cgit v1.2.3 From 9e2f24d5105370ac3964d2e3aae76759f3912db3 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 17 Apr 2016 14:22:54 +0200 Subject: Add changelog for 8.5pl1 after the fact. Will be displayed on the website, but not part of the package. --- CHANGES | 66 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/CHANGES b/CHANGES index 531d5049fd..f06cd13b3b 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,69 @@ +Changes from V8.5 to V8.5pl1 +============================ + +Critical bugfix +- The subterm relation for the guard condition was incorrectly defined on + primitive projections (#4588) + +Plugin development tools +- add a .merlin target to the makefile + +Various performance improvements (time, space used by .vo files) + +Other bugfixes + +- Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v +- Added compatibility coercions from Specif.v which were present in Coq 8.4. +- Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic. +- Allow to unset the refinement mode of Instance in ML +- Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite. +- Add -compat 8.4 econstructor tactics, and tests +- Add compatibility Nonrecursive Elimination Schemes +- Fixing the "No applicable tactic" non informative error message regression on apply. +- Univs: fix get_current_context (bug #4603, part I) +- Fix a bug in Program coercion code +- Fix handling of arity of definitional classes. +- #4630: Some tactics are 20x slower in 8.5 than 8.4. +- #4627: records with no declared arity can be template polymorphic. +- #4623: set tactic too weak with universes (regression) +- Fix incorrect behavior of CS resolution +- #4591: Uncaught exception in directory browsing. +- CoqIDE is more resilient to initialization errors. +- #4614: "Fully check the document" is uninterruptable. +- Try eta-expansion of records only on non-recursive ones +- Fix bug when a sort is ascribed to a Record +- Primitive projections: protect kernel from erroneous definitions. +- Fixed bug #4533 with previous Keyed Unification commit +- Win: kill unreliable hence do not waitpid after kill -9 (Close #4369) +- Fix strategy of Keyed Unification +- #4608: Anomaly "output_value: abstract value (outside heap)". +- #4607: do not read native code files if native compiler was disabled. +- #4105: poor escaping in the protocol between CoqIDE and coqtop. +- #4596: [rewrite] broke in the past few weeks. +- #4533 (partial): respect declared global transparency of projections in unification.ml +- #4544: Backtrack on using full betaiota reduction during keyed unification. +- #4540: CoqIDE bottom progress bar does not update. +- Fix regression from 8.4 in reflexivity +- #4580: [Set Refine Instance Mode] also used for Program Instance. +- #4582: cannot override notation [ x ]. +- STM: Print/Extraction have to be skipped if -quick +- #4542: CoqIDE: STOP button also stops workers +- STM: classify some variants of Instance as regular `Fork nodes. +- #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity"). +- Do not give a name to anonymous evars anymore. See bug #4547. +- STM: always stock in vio files the first node (state) of a proof +- STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530 +- Don't fail fatally if PATH is not set. +- #4537: Coq 8.5 is slower in typeclass resolution. +- #4522: Incorrect "Warning..." on windows. +- #4373: coqdep does not know about .vio files. +- #3826: "Incompatible module types" is uninformative. +- #4495: Failed assertion in metasyntax.ml. +- #4511: evar tactic can create non-typed evars. +- #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported. +- #4519: oops, global shadowed local universe level bindings. +- #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed. + Changes from V8.5beta3 to V8.5 ============================== -- cgit v1.2.3 From f5dc54519f2a62bab2f7b9059e8c3c8dc53619be Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Apr 2016 00:01:19 +0200 Subject: Fixing printing of surrounding parentheses in "ltac:". --- printing/pptactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7e903d2d3d..d1039c1277 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1278,7 +1278,7 @@ module Make | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a)) + keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a))) in pr_tac -- cgit v1.2.3 From 50266aab0b9d9ba3bede37429bcdc5c2bfdc1159 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 17 Apr 2016 21:55:18 +0200 Subject: Updating configure.ml wrt Coq not compilable with OCaml 4.01.0 in debug mode. --- configure.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/configure.ml b/configure.ml index 48bcf34e11..6291de03cb 100644 --- a/configure.ml +++ b/configure.ml @@ -520,6 +520,9 @@ let check_caml_version () = die ("Your version of OCaml is 4.02.0 which suffers from a bug inducing\n" ^ "very slow compilation times. If you still want to use it, use \n" ^ "option -force-caml-version.\n") + else if caml_version_nums = [4;1;0] && !Prefs.debug then + die ("Your version of OCaml is 4.01.0 which fails to compile Coq in " ^ + "-debug mode.\nRemove -debug option or use a different version of OCaml.\n") else printf "You have OCaml %s. Good!\n" caml_version else -- cgit v1.2.3 From d926105c022177b70578982d037b12e5d914922b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 8 Apr 2016 21:32:59 +0200 Subject: Building lazily a few debugging messages involving expressions of commands so that they are not silently computed when not in debugging mode. --- toplevel/vernacentries.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 72dd967b92..ee11d356d1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -34,8 +34,8 @@ open Misctypes open Locality let debug = false -let prerr_endline = - if debug then prerr_endline else fun _ -> () +let prerr_endline x = + if debug then prerr_endline (x ()) else () (* Misc *) @@ -1841,7 +1841,7 @@ let vernac_load interp fname = * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) let interp ?proof ~loc locality poly c = - prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); + prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* Done later in this file *) | VernacLoad _ -> assert false -- cgit v1.2.3 From 7f85eb4f4cba0194f68034d6ccc0de0be9b5f067 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 17 Apr 2016 22:21:54 +0200 Subject: Revert "Fixing printing of surrounding parentheses in "ltac:"." I made a confusion between ltac: in constr and ltac: in tactics, the one needing parentheses in v8.5 but the latter needing parentheses only in trunk. This reverts commit f5dc54519f2a62bab2f7b9059e8c3c8dc53619be. --- printing/pptactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index d1039c1277..7e903d2d3d 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1278,7 +1278,7 @@ module Make | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a))) + keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a)) in pr_tac -- cgit v1.2.3 From b038ff00e3d1873bed580c13df1b18ce0510abb2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 19 Apr 2016 09:37:55 +0200 Subject: Fixing 50266aab on incompatibility of OCaml 4.01.0 with option -debug. This was only when compiling with Camlp4 and it was producing an assertion failure in asmcomp/emitaux.ml at line 226, reported as OCaml's bug #6243. Note: The issue of a problematic compilation with 4.01.0 was raised at last WG. --- configure.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/configure.ml b/configure.ml index 6291de03cb..83005f0c50 100644 --- a/configure.ml +++ b/configure.ml @@ -520,9 +520,6 @@ let check_caml_version () = die ("Your version of OCaml is 4.02.0 which suffers from a bug inducing\n" ^ "very slow compilation times. If you still want to use it, use \n" ^ "option -force-caml-version.\n") - else if caml_version_nums = [4;1;0] && !Prefs.debug then - die ("Your version of OCaml is 4.01.0 which fails to compile Coq in " ^ - "-debug mode.\nRemove -debug option or use a different version of OCaml.\n") else printf "You have OCaml %s. Good!\n" caml_version else @@ -600,6 +597,12 @@ let check_camlp5_version () = | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n" +let check_caml_version_for_camlp4 () = + if caml_version_nums = [4;1;0] && !Prefs.debug then + die ("Your version of OCaml is 4.01.0 which fails to compile Coq in -debug\n" ^ + "mode with Camlp4. Remove -debug option or use a different version of OCaml\n" ^ + "or use Camlp5.\n") + let config_camlpX () = try if not !Prefs.usecamlp5 then raise NoCamlp5; @@ -618,6 +621,7 @@ let config_camlpX () = let camlp4orf = which_camlpX "camlp4orf" in let version_line, _ = run ~err:StdOut camlp4orf ["-v"] in let camlp4_version = List.nth (string_split ' ' version_line) 2 in + check_caml_version_for_camlp4 (); "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod, camlp4_version with _ -> die "No Camlp4 installation found.\n" -- cgit v1.2.3 From 75a48bfc6b91f1e5095d9cdfbcc0ae2bf8cf16ec Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 19 Apr 2016 19:13:23 +0200 Subject: Fixing #4677 (collision of a global variable and of a local variable while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion). --- CHANGES | 7 +++++++ interp/notation_ops.ml | 14 ++++++++++---- pretyping/glob_ops.ml | 12 +++++++++++- pretyping/glob_ops.mli | 1 + test-suite/output/Notations2.out | 4 ++++ test-suite/output/Notations2.v | 8 ++++++++ 6 files changed, 41 insertions(+), 5 deletions(-) diff --git a/CHANGES b/CHANGES index f06cd13b3b..e5aa52880a 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,10 @@ +Changes from V8.5pl1 to V8.5pl2 +=============================== + +Bugfixes + +- #4677: fix alpha-conversion in notations needing eta-expansion + Changes from V8.5 to V8.5pl1 ============================ diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 51dfadac02..5abc7794bd 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -794,15 +794,21 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = otherwise how to ensure it corresponds to a well-typed eta-expansion; we make an exception for types which are metavariables: this is useful e.g. to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *) - | b1, NLambda (Name id,(NHole _ | NVar _ as t2),b2) when inner -> - let id' = Namegen.next_ident_away id (free_glob_vars b1) in + | b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner -> + let avoid = + free_glob_vars b1 @ (* as in Namegen: *) glob_visible_short_qualid b1 in + let id' = Namegen.next_ident_away id avoid in let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_env alp sigma id2 t1 | _ -> assert false in - match_in u alp metas (bind_binder sigma id [(Name id',Explicit,None,t1)]) - (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 + let (alp,sigma) = + if Id.List.mem id blmetas then + alp, bind_binder sigma id [(Name id',Explicit,None,t1)] + else + match_names metas (alp,sigma) (Name id') na in + match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 | (GRec _ | GEvar _), _ | _,_ -> raise No_match diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index c9860864a9..e3b6fb08a8 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -266,7 +266,7 @@ let add_name_to_ids set na = | Anonymous -> set | Name id -> Id.Set.add id set -let free_glob_vars = +let free_glob_vars = let rec vars bounded vs = function | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) @@ -324,6 +324,16 @@ let free_glob_vars = let vs = vars Id.Set.empty Id.Set.empty rt in Id.Set.elements vs +let glob_visible_short_qualid c = + let rec aux acc = function + | GRef (_,c,_) -> + let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in + let dir,id = Libnames.repr_qualid qualid in + if DirPath.is_empty dir then id :: acc else acc + | c -> + fold_glob_constr aux acc c + in aux [] c + let add_and_check_ident id set = if Id.Set.mem id set then Pp.(msg_warning diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 45444234a3..e0a2de0326 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -40,6 +40,7 @@ val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list val bound_glob_vars : glob_constr -> Id.Set.t val loc_of_glob_constr : glob_constr -> Loc.t +val glob_visible_short_qualid : glob_constr -> Id.t list (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 58ec1de563..6ff1d38372 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -50,3 +50,7 @@ end : nat -> nat # _ : nat => 2 : nat -> nat +# x : nat => # H : x <= 0 => exist (le x) 0 H + : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0} +exist (Q x) y conj + : {x0 : A | Q x x0} diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index e53c94ef0a..c9efe1ead4 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -68,8 +68,10 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* In practice, only the printing rule is used here *) (* Note: does not work for pattern *) +Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). Check fun f x => f x + S x. +End A. Open Scope list_scope. Notation list1 := (1::nil)%list. @@ -98,3 +100,9 @@ Notation "# x : T => t" := (fun x : T => t) Check # x : nat => x. Check # _ : nat => 2. + +(* Check bug 4677 *) +Check fun x (H:le x 0) => exist (le x) 0 H. + +Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y). +Check (exist (Q x) y conj). -- cgit v1.2.3 From 4f087a9c3139fed092171b70ca9f6470be4bf9c0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 22 Apr 2016 14:38:01 +0200 Subject: Mention #4548 (fixed) in CHANGES. --- CHANGES | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGES b/CHANGES index e5aa52880a..b400ff1a80 100644 --- a/CHANGES +++ b/CHANGES @@ -70,6 +70,7 @@ Other bugfixes - #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported. - #4519: oops, global shadowed local universe level bindings. - #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed. +- #4548: Coqide crashes when going back one command Changes from V8.5beta3 to V8.5 ============================== -- cgit v1.2.3 From 1c506bb3d9128590f23a4872586a22d930672a69 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 22 Apr 2016 14:38:27 +0200 Subject: Mention problems with fix of #4582 in CHANGES. --- CHANGES | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGES b/CHANGES index b400ff1a80..79fe3642b2 100644 --- a/CHANGES +++ b/CHANGES @@ -52,7 +52,7 @@ Other bugfixes - #4540: CoqIDE bottom progress bar does not update. - Fix regression from 8.4 in reflexivity - #4580: [Set Refine Instance Mode] also used for Program Instance. -- #4582: cannot override notation [ x ]. +- #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683. - STM: Print/Extraction have to be skipped if -quick - #4542: CoqIDE: STOP button also stops workers - STM: classify some variants of Instance as regular `Fork nodes. -- cgit v1.2.3 From 96bb190caa138c91b4d5e5f96d6f179811a177c8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 19 Apr 2016 20:34:48 +0200 Subject: Fixing output test Notations2. --- test-suite/output/Notations2.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index c9efe1ead4..4e0d135d7d 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -71,7 +71,6 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). Check fun f x => f x + S x. -End A. Open Scope list_scope. Notation list1 := (1::nil)%list. @@ -79,6 +78,7 @@ Notation plus2 n := (S (S n)). (* plus2 was not correctly printed in the two following tests in 8.3pl1 *) Print plus2. Check fun n => match n with list1 => 0 | _ => 2 end. +End A. (* This one is not fully satisfactory because binders in the same type are re-factorized and parentheses are needed even for atomic binder -- cgit v1.2.3