Merge branch 'v8.5'

Author: ppedrot

checker/check_stat.ml

@@ -28,7 +28,7 @@ let pr_engagement (impr_set,type_in_type) =
     match impr_set with
     | ImpredicativeSet -> str "Theory: Set is impredicative"
     | PredicativeSet -> str "Theory: Set is predicative"
-  end ++
+  end ++ fnl() ++
   begin
     match type_in_type with
     | StratifiedType -> str "Theory: Stratified type hierarchy"

configure.ml

@@ -566,10 +566,11 @@ let check_camlp5_version () =
   | _ -> 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")
+  if caml_version_nums = [4;1;0] && !Prefs.debug && not !Prefs.force_caml_version then
+    die ("Your version of OCaml is detected to be 4.01.0 which fails to compile\n" ^
+         "Coq in -debug mode with Camlp4. Remove -debug option or use a different\n" ^
+         "version of OCaml or use Camlp5, or bypass this test by using option\n" ^
+         "-force-caml-version.\n")
 
 let config_camlpX () =
   try

doc/tutorial/Tutorial.tex

@@ -248,11 +248,14 @@ \subsection{Definitions}
 \begin{coq_example}
 Check (forall m:nat, gt m 0).
 \end{coq_example}
-We may clean-up the development by removing the contents of the
-current section:
+We may revert to the clean state of
+our initial session using the \Coq~ \verb:Reset: command:
 \begin{coq_example}
-Reset Declaration.
+Reset Initial.
 \end{coq_example}
+\begin{coq_eval}
+Set Printing Width 60.
+\end{coq_eval}
 
 \section{Introduction to the proof engine: Minimal Logic}
 
@@ -658,10 +661,8 @@ \subsection{Sections and signatures}
 as global variables. But we must be careful about the pollution of our
 global environment by such declarations. For instance, we have already 
 polluted our \Coq~ session by declaring the variables
-\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:. If we want to revert to the clean state of
-our initial session, we may use the \Coq~ \verb:Reset: command, which returns
-to the state just prior the given global notion as we did before to
-remove a section, or we may return to the initial state using~:
+\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:.
+
 \begin{coq_example}
 Reset Initial.
 \end{coq_example}
@@ -770,7 +771,7 @@ \subsection{Existential quantification}
 End R_sym_trans.
 \end{coq_example}
 
-Here \Coq's printout is a warning that all local hypotheses have been 
+All the local hypotheses have been
 discharged in the statement of \verb:refl_if:, which now becomes a general
 theorem in the first-order language declared in section 
 \verb:Predicate_calculus:. In this particular example, the use of section
@@ -1105,8 +1106,14 @@ \subsection{Principle of proof irrelevance}
 
 Conversely, ordinary mathematical definitions can be unfolded at will, they
 are {\sl transparent}. 
+
 \chapter{Induction}
 
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+\end{coq_eval}
+
 \section{Data Types as Inductively Defined Mathematical Collections}
 
 All the notions which were studied until now pertain to traditional
@@ -1195,7 +1202,7 @@ \subsection{Natural numbers}
 \verb:Set: \verb:(P i):, \verb:prim_rec: computes uniformly an element of 
 \verb:nat:. Let us check the type of \verb:prim_rec::
 \begin{coq_example}
-Check prim_rec.
+About prim_rec.
 \end{coq_example}
 
 Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we
@@ -1241,22 +1248,16 @@ \subsection{Natural numbers}
 For the rest of the session, we shall clean up what we did so far with 
 types \verb:bool: and \verb:nat:, in order to use the initial definitions
 given in \Coq's \verb:Prelude: module, and not to get confusing error
-messages due to our redefinitions. We thus revert to the state before
-our definition of \verb:bool: with the \verb:Reset: command:
+messages due to our redefinitions. We thus revert to the initial state:
 \begin{coq_example}
-Reset bool.
-\end{coq_example}
-
-
-\subsection{Simple proofs by induction}
-
-\begin{coq_eval}
 Reset Initial.
-\end{coq_eval}
+\end{coq_example}
 \begin{coq_eval}
 Set Printing Width 60.
 \end{coq_eval}
 
+\subsection{Simple proofs by induction}
+
 Let us now show how to do proofs by structural induction. We start with easy
 properties of the \verb:plus: function we just defined. Let us first
 show that $n=n+0$.
@@ -1480,6 +1481,11 @@ \section{Logic programming}
 
 \chapter{Modules}
 
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+\end{coq_eval}
+
 \section{Opening library modules}
 
 When you start \Coq~ without further requirements in the command line,
@@ -1543,19 +1549,23 @@ \section{Managing the context}
 libraries have been loaded. A convenient \verb:Search: command
 is available to lookup all known facts 
 concerning a given predicate. For instance, if you want to know all the
-known lemmas about the less or equal relation, just ask:
+known lemmas about both the successor and the less or equal relation, just ask:
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+\end{coq_eval}
 \begin{coq_example}
-Search le.
+Search S le.
 \end{coq_example}
 Another command \verb:SearchHead: displays only lemmas where the searched
 predicate appears at the head position in the conclusion.
 \begin{coq_example}
 SearchHead le.
 \end{coq_example}
 
-A new and more convenient search tool is \textsf{SearchPattern}
+A new and more convenient search tool is \verb:SearchPattern:
 developed by Yves Bertot. It allows finding the theorems with a
-conclusion matching a given pattern, where \verb:\_: can be used in
+conclusion matching a given pattern, where \verb:_: can be used in
 place of an arbitrary term. We remark in this example, that \Coq{}
 provides usual infix notations for arithmetic operators.
 

ide/coq.lang

@@ -95,11 +95,24 @@
       <keyword>Type</keyword>
     </context>
 
-    <context id="coq" class="no-spell-check">
+    <!-- Terms -->
+    <context id="constr">
       <include>
         <context ref="string"/>
         <context ref="coqdoc"/>
         <context ref="comment"/>
+        <context ref="constr-sort"/>
+        <context ref="constr-keyword"/>
+        <context id="dot-nosep">
+          <match>\.\.</match>
+        </context>
+      </include>
+    </context>
+
+    <context id="coq" class="no-spell-check">
+      <include>
+        <context ref="coqdoc"/>
+        <context ref="comment"/>
 
         <context id="declaration">
           <start>\%{decl_head}</start>
@@ -110,14 +123,7 @@
             <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/>
             <context sub-pattern="id_list" where="start" style-ref="identifier"/>
             <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
-            <context ref="constr-keyword"/>
-            <context ref="constr-sort"/>
-            <context id="dot-nosep">
-              <match>\.\.</match>
-            </context>
-            <context ref="string"/>
-            <context ref="coqdoc"/>
-            <context ref="comment"/>
+            <context ref="constr"/>
           </include>
         </context>
 
@@ -127,21 +133,19 @@
           <include>
             <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
             <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
-            <context ref="command-in-proof"/>
-            <context ref="string"/>
             <context ref="coqdoc"/>
             <context ref="comment"/>
-            <context ref="constr-keyword"/>
-            <context ref="constr-sort"/>
-            <context id="bullet" extend-parent="false">
-              <match>\%{dot_sep}\s*(?'bul'\%{bullet})</match>
+            <context id="bullet" style-ref="vernac-keyword" extend-parent="false">
+              <match>\%{bullet}</match>
+            </context>
+            <context extend-parent="false">
+              <start>\%[</start>
+              <end>\%{dot_sep}</end>
               <include>
-                <context sub-pattern="bul" style-ref="vernac-keyword"/>
+                <context ref="command-in-proof"/>
+                <context ref="constr"/>
               </include>
             </context>
-            <context id="bullet-sol" style-ref="vernac-keyword">
-              <match>^\s*\%{bullet}</match>
-            </context>
           </include>
         </context>
 
@@ -150,11 +154,19 @@
           <end>\%{dot_sep}</end>
           <include>
             <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
-            <context ref="constr-keyword"/>
-            <context ref="constr-sort"/>
+            <context ref="constr"/>
           </include>
         </context>
 
+        <context ref="command"/>
+      </include>
+    </context>
+
+    <!-- Toplevel commands -->
+    <context id="command" extend-parent="false">
+      <start>\%[</start>
+      <end>\%{dot_sep}</end>
+      <include>
         <context id="command-in-proof" style-ref="vernac-keyword">
           <keyword>About</keyword>
           <keyword>Check</keyword>
@@ -166,7 +178,7 @@
           <keyword>Transparent</keyword>
         </context>
 
-        <context id="command" style-ref="vernac-keyword">
+        <context id="toplevel-command" style-ref="vernac-keyword">
           <keyword>Add</keyword>
           <keyword>Load</keyword>
           <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
@@ -228,7 +240,10 @@
             <context sub-pattern="qua_list" style-ref="identifier"/>
           </include>
         </context>
+
+        <context ref="constr"/>
       </include>
     </context>
+
   </definitions>
 </language>

ide/coq.png

@@ -177,7 +177,7 @@ let convert_instances ~flex u u' (s, check) =
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
   match k1, k2 with
-  | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' ->
+  | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' ->
     if Univ.Instance.equal u u' then cuniv
     else 
       let flex = evaluable_constant cst (info_env infos) 

kernel/reduction.ml

@@ -264,7 +264,8 @@ let skip_in_segment f ch =
   seek_in ch stop;
   stop, digest_in f ch
 
-exception Bad_magic_number of string
+type magic_number_error = {filename: string; actual: int; expected: int}
+exception Bad_magic_number of magic_number_error
 
 let raw_extern_state magic filename =
   let channel = open_trapping_failure filename in
@@ -274,8 +275,12 @@ let raw_extern_state magic filename =
 let raw_intern_state magic filename =
   try
     let channel = open_in_bin filename in
-    if not (Int.equal (input_binary_int filename channel) magic) then
-      raise (Bad_magic_number filename);
+    let actual_magic = input_binary_int filename channel in
+    if not (Int.equal actual_magic magic) then
+        raise (Bad_magic_number {
+            filename=filename;
+            actual=actual_magic;
+            expected=magic});
     channel
   with
   | End_of_file -> error_corrupted filename "premature end of file"
@@ -305,9 +310,11 @@ let intern_state magic filename =
 
 let with_magic_number_check f a =
   try f a
-  with Bad_magic_number fname ->
+  with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
     errorlabstrm "with_magic_number_check"
-    (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++
+    (str"File " ++ str fname ++ strbrk" has bad magic number " ++
+    int actual ++ str" (expected " ++ int expected ++ str")." ++
+    spc () ++
     strbrk "It is corrupted or was compiled with another version of Coq.")
 
 (* Time stamps. *)

lib/system.ml

@@ -64,9 +64,11 @@ val file_exists_respecting_case : string -> string -> bool
 (** {6 I/O functions } *)
 (** Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
-  when the check fails, with the full file name. *)
+  when the check fails, with the full file name and expected/observed magic
+  numbers. *)
 
-exception Bad_magic_number of string
+type magic_number_error = {filename: string; actual: int; expected: int}
+exception Bad_magic_number of magic_number_error
 
 val raw_extern_state : int -> string -> out_channel
 

lib/system.mli

@@ -1765,12 +1765,12 @@ let build_inversion_problem loc env sigma tms t =
       Pushed (true,((tm,tmtyp),deps,na)))
       dep_sign decls in
   let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
-  (* [eqn1] is the first clause of the auxiliary pattern-matching that
+  (* [main_eqn] is the main clause of the auxiliary pattern-matching that
      serves as skeleton for the return type: [patl] is the
      substructure of constructors extracted from the list of
      constraints on the inductive types of the multiple terms matched
      in the original pattern-matching problem Xi *)
-  let eqn1 =
+  let main_eqn =
     { patterns = patl;
       alias_stack = [];
       eqn_loc = Loc.ghost;
@@ -1781,19 +1781,24 @@ let build_inversion_problem loc env sigma tms t =
               rhs_vars = List.map fst subst;
               avoid_ids = avoid;
 	      it = Some (lift n t) } } in
-  (* [eqn2] is the default clause of the auxiliary pattern-matching: it will
-     catch the clauses of the original pattern-matching problem Xi whose
-     type constraints are incompatible with the constraints on the
+  (* [catch_all] is a catch-all default clause of the auxiliary
+     pattern-matching, if needed: it will catch the clauses
+     of the original pattern-matching problem Xi whose type
+     constraints are incompatible with the constraints on the
      inductive types of the multiple terms matched in Xi *)
-  let eqn2 =
-    { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
-      alias_stack = [];
-      eqn_loc = Loc.ghost;
-      used = ref false;
-      rhs = { rhs_env = pb_env;
-              rhs_vars = [];
-	      avoid_ids = avoid0;
-	      it = None } } in
+  let catch_all_eqn =
+    if List.for_all (irrefutable env) patl then
+      (* No need for a catch all clause *)
+      []
+    else
+      [ { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
+          alias_stack = [];
+          eqn_loc = Loc.ghost;
+          used = ref false;
+          rhs = { rhs_env = pb_env;
+                  rhs_vars = [];
+	          avoid_ids = avoid0;
+	          it = None } } ] in
   (* [pb] is the auxiliary pattern-matching serving as skeleton for the
       return type of the original problem Xi *)
   (* let sigma, s = Evd.new_sort_variable sigma in *)
@@ -1810,7 +1815,7 @@ let build_inversion_problem loc env sigma tms t =
       pred      = (*ty *) mkSort s;
       tomatch   = sub_tms;
       history   = start_history n;
-      mat       = [eqn1;eqn2];
+      mat       = main_eqn :: catch_all_eqn;
       caseloc   = loc;
       casestyle = RegularStyle;
       typing_function = build_tycon loc env pb_env s subst} in