aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check_stat.ml2
-rw-r--r--configure.ml9
-rw-r--r--doc/tutorial/Tutorial.tex56
-rw-r--r--ide/coq.lang59
-rw-r--r--ide/coq.pngbin71924 -> 12907 bytes
-rw-r--r--kernel/reduction.ml2
-rw-r--r--lib/system.ml17
-rw-r--r--lib/system.mli6
-rw-r--r--pretyping/cases.ml35
-rw-r--r--pretyping/cbv.ml2
-rw-r--r--test-suite/bugs/closed/4634.v16
-rw-r--r--test-suite/success/remember.v13
-rw-r--r--theories/Vectors/VectorDef.v2
13 files changed, 144 insertions, 75 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index d031975d7..84f5684d4 100644
--- a/checker/check_stat.ml
+++ b/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"
diff --git a/configure.ml b/configure.ml
index 80a776471..5baaf6d8c 100644
--- a/configure.ml
+++ b/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
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index e09feeb8e..973a0b75e 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -248,11 +248,14 @@ explicitly the type of the quantified variable. We check:
\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 @@ respectively 1 and 2. Such abstract entities may be entered in the context
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 @@ Let us now close the current section.
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 @@ mathematical justification of a logical development relies only on
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 @@ That is, instead of computing for natural \verb:i: an element of the indexed
\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 @@ Fixpoint plus (n m:nat) {struct n} : nat :=
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 @@ Qed.
\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,9 +1549,13 @@ definitions available in the current context, especially if large
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.
@@ -1553,9 +1563,9 @@ predicate appears at the head position in the conclusion.
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.
diff --git a/ide/coq.lang b/ide/coq.lang
index e25eedbca..484264ece 100644
--- a/ide/coq.lang
+++ b/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>
diff --git a/ide/coq.png b/ide/coq.png
index cccd5a9a1..136bfdd5f 100644
--- a/ide/coq.png
+++ b/ide/coq.png
Binary files differ
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cfc286135..f23ed16f0 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -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)
diff --git a/lib/system.ml b/lib/system.ml
index 10ef8580b..e54109a2f 100644
--- a/lib/system.ml
+++ b/lib/system.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. *)
diff --git a/lib/system.mli b/lib/system.mli
index e1190dfb5..4dbb3695d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -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
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c3968f896..b8fb61e35 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -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
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 43062a0e8..afd86420e 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -310,7 +310,7 @@ and cbv_stack_value info env = function
| (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
when red_set (info_flags info) fIOTA && Projection.unfolded p ->
let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
- cbv_stack_value info env (arg, stk)
+ cbv_stack_value info env (strip_appl arg stk)
(* may be reduced later by application *)
| (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl)
diff --git a/test-suite/bugs/closed/4634.v b/test-suite/bugs/closed/4634.v
new file mode 100644
index 000000000..77e31e108
--- /dev/null
+++ b/test-suite/bugs/closed/4634.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+
+Polymorphic Record pair {A B : Type} : Type :=
+ prod { pr1 : A; pr2 : B }.
+
+Notation " ( x ; y ) " := (@prod _ _ x y).
+Notation " x .1 " := (pr1 x) (at level 3).
+Notation " x .2 " := (pr2 x) (at level 3).
+
+Goal ((0; 1); 2).1.2 = 1.
+Proof.
+ cbv.
+ match goal with
+ | |- ?t = ?t => exact (eq_refl t)
+ end.
+Qed.
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 0befe054a..b26a9ff1e 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -14,3 +14,16 @@ let name := fresh "fresh" in
remember (1 + 2) as x eqn:name.
rewrite fresh.
Abort.
+
+(* An example which was working in 8.4 but failing in 8.5 and 8.5pl1 *)
+
+Module A.
+Axiom N : nat.
+End A.
+Module B.
+Include A.
+End B.
+Goal id A.N = B.N.
+reflexivity.
+Qed.
+
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 45c13e5ce..c69223804 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -297,7 +297,7 @@ Notation "[]" := [] : vector_scope.
Notation "h :: t" := (h :: t) (at level 60, right associativity)
: vector_scope.
Notation " [ x ] " := (x :: []) : vector_scope.
-Notation " [ x ; .. ; y ] " := (cons _ x _ .. (cons _ y _ (nil _)) ..) : vector_scope
+Notation " [ x ; y ; .. ; z ] " := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope
.
Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
Open Scope vector_scope.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 18:00:02 +0000