aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman')
-rw-r--r--doc/refman/Cases.tex4
-rw-r--r--doc/refman/Classes.tex2
-rw-r--r--doc/refman/RefMan-cic.tex50
-rw-r--r--doc/refman/RefMan-decl.tex6
-rw-r--r--doc/refman/RefMan-gal.tex14
-rw-r--r--doc/refman/RefMan-mod.tex14
-rw-r--r--doc/refman/RefMan-syn.tex8
-rw-r--r--doc/refman/RefMan-tac.tex14
8 files changed, 49 insertions, 63 deletions
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 51ec2ef81..4238bf6a5 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -194,7 +194,7 @@ system. Here is an example:
Set Printing Depth 50.
\end{coq_eval}
\begin{coq_example}
-Check (fun x:nat =>
+Fail Check (fun x:nat =>
match x with
| O => true
| S _ => false
@@ -271,7 +271,7 @@ When we use parameters in patterns there is an error message:
Set Printing Depth 50.
\end{coq_eval}
\begin{coq_example}
-Check
+Fail Check
(fun l:List nat =>
match l with
| nil A => nil nat
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 069b99127..e8ebb9f99 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -107,7 +107,7 @@ satisfied by \texttt{{eqa : EqDec A}}. In case no satisfying constraint can be
found, an error is raised:
\begin{coq_example}
-Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
+Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
\end{coq_example}
The algorithm used to solve constraints is a variant of the eauto tactic
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 1cce48b95..3fd5ae0b2 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -742,11 +742,11 @@ there is an occurrence of \List\ which is not applied to the parameter
variable in the conclusion of the type of {\tt cons'}:
\begin{coq_eval}
Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(********* Error: The 1st argument of list' must be A in ... *********)
\end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (********* Error: The 1st argument of list' must be A in ... *********)
\begin{coq_example}
-Inductive list' (A:Set) : Set :=
+Fail Inductive list' (A:Set) : Set :=
| nil' : list' A
| cons' : A -> list' A -> list' (A*A).
\end{coq_example}
@@ -919,12 +919,10 @@ 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:
-\begin{coq_eval}
-(********** The following is not correct and should produce **********)
-(*** Error: Large non-propositional inductive types must be in Type***)
-\end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (*** Error: Large non-propositional inductive types must be in Type***)
\begin{coq_example}
-Inductive exSet (P:Set->Prop) : Set
+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
@@ -1282,14 +1280,11 @@ Inductive or (A B:Prop) : Prop :=
\end{coq_example*}
The following definition which computes a boolean value by case over
the proof of \texttt{or A B} is not accepted:
-\begin{coq_eval}
-(***************************************************************)
-(*** This example should fail with ``Incorrect elimination'' ***)
-\end{coq_eval}
+% (***************************************************************)
+% (*** This example should fail with ``Incorrect elimination'' ***)
\begin{coq_example}
-Set Asymmetric Patterns.
-Definition choice (A B: Prop) (x:or A B) :=
- match x with or_introl a => true | or_intror b => false end.
+Fail Definition choice (A B: Prop) (x:or A B) :=
+ match x with or_introl _ _ a => true | or_intror _ _ b => false end.
\end{coq_example}
From the computational point of view, the structure of the proof of
\texttt{(or A B)} in this term is needed for computing the boolean
@@ -1592,8 +1587,8 @@ Fixpoint plus (n m:nat) {struct n} : nat :=
Print plus.
Fixpoint lgth (A:Set) (l:list A) {struct l} : nat :=
match l with
- | nil => O
- | cons a l' => S (lgth A l')
+ | nil _ => O
+ | cons _ a l' => S (lgth A l')
end.
Print lgth.
Fixpoint sizet (t:tree) : nat := let (f) := t in S (sizef f)
@@ -1632,13 +1627,11 @@ Definition sont (t:tree) : forest
:= let (f) := t in f.
\end{coq_example}
The following is not a conversion but can be proved after a case analysis.
-\begin{coq_eval}
-(******************************************************************)
-(** Error: Impossible to unify .... **)
-\end{coq_eval}
+% (******************************************************************)
+% (** Error: Impossible to unify .... **)
\begin{coq_example}
Goal forall t:tree, sizet t = S (sizef (sont t)).
-reflexivity. (** this one fails **)
+Fail reflexivity.
destruct t.
reflexivity.
\end{coq_example}
@@ -1701,16 +1694,13 @@ by using the compiler option \texttt{-impredicative-set}.
For example, using the ordinary \texttt{coqtop} command, the following
is rejected.
-\begin{coq_eval}
-(** This example should fail *******************************
- Error: The term forall X:Set, X -> X has type Type
- while it is expected to have type Set
-***)
-\end{coq_eval}
+% (** This example should fail *******************************
+% Error: The term forall X:Set, X -> X has type Type
+% while it is expected to have type Set ***)
\begin{coq_example}
-Definition id: Set := forall X:Set,X->X.
+Fail Definition id: Set := forall X:Set,X->X.
\end{coq_example}
-while it will type-check, if one use instead the \texttt{coqtop
+while it will type-check, if one uses instead the \texttt{coqtop
-impredicative-set} command.
The major change in the theory concerns the rule for product formation
diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex
index c84e3a9df..aae10e323 100644
--- a/doc/refman/RefMan-decl.tex
+++ b/doc/refman/RefMan-decl.tex
@@ -192,7 +192,7 @@ later.
Theorem this_is_not_so_trivial: False.
proof.
end proof. (* here a warning is issued *)
-Qed. (* fails: the proof in incomplete *)
+Fail Qed. (* fails: the proof in incomplete *)
Admitted. (* Oops! *)
\end{coq_example}
\begin{coq_eval}
@@ -404,7 +404,7 @@ proof.
\end{coq_eval}
\begin{coq_example}
Show.
-hence C. (* fails *)
+Fail hence C. (* fails *)
\end{coq_example}
\begin{coq_eval}
Abort.
@@ -578,7 +578,7 @@ let P:(nat -> Prop).
\end{coq_eval}
\begin{coq_example}
Show.
-let x. (* fails because x's type is not clear *)
+Fail let x. (* fails because x's type is not clear *)
let x be such that HP:(P x). (* here x's type is inferred from (P x) *)
\end{coq_example}
\begin{coq_eval}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 0d628ac7e..cf83d0c72 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1155,7 +1155,7 @@ Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
\end{coq_example*}
But the following definition will give an error:
\begin{coq_example}
-Inductive listw (A:Set) : Set :=
+Fail Inductive listw (A:Set) : Set :=
| nilw : listw (A*A)
| consw : A -> listw (A*A) -> listw (A*A).
\end{coq_example}
@@ -1401,11 +1401,11 @@ error message:
\begin{coq_eval}
Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(********* Error: Recursive call to wrongplus ... **********)
\end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (********* Error: Recursive call to wrongplus ... **********)
\begin{coq_example}
-Fixpoint wrongplus (n m:nat) {struct n} : nat :=
+Fail Fixpoint wrongplus (n m:nat) {struct n} : nat :=
match m with
| O => n
| S p => S (wrongplus n p)
@@ -1530,11 +1530,11 @@ function does not satisfy the guard condition:
\begin{coq_eval}
Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(***************** Error: Unguarded recursive call *******************)
\end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (***************** Error: Unguarded recursive call *******************)
\begin{coq_example}
-CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
+Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
\end{coq_example}
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index f48cf6abf..48b9315e3 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -238,14 +238,14 @@ as the body of \texttt{x}.
\begin{coq_eval}
Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(***************** Error: N.y not a defined object *******************)
\end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (***************** Error: N.y not a defined object *******************)
\begin{coq_example}
Module N : SIG with Definition T := nat := M.
Print N.T.
Print N.x.
-Print N.y.
+Fail Print N.y.
\end{coq_example}
\begin{coq_eval}
Reset N.
@@ -353,15 +353,11 @@ Example:
\begin{coq_example}
Module Mod.
-\end{coq_example}
-\begin{coq_example}
Definition T:=nat.
Check T.
-\end{coq_example}
-\begin{coq_example}
End Mod.
Check Mod.T.
-Check T. (* Incorrect ! *)
+Fail Check T. (* Incorrect! *)
Import Mod.
Check T. (* Now correct *)
\end{coq_example}
@@ -386,7 +382,7 @@ Local Definition T := nat.
End B.
End A.
Import A.
-Check B.T.
+Fail Check B.T.
\end{coq_example}
\begin{Variants}
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 15ddf6261..107b98f01 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -434,7 +434,7 @@ notation are replaced by ``\_''.
\Example
\begin{coq_example}
Locate "exists".
-Locate "'exists' _ , _".
+Locate "exists _ .. _ , _".
\end{coq_example}
\SeeAlso Section \ref{Locate}.
@@ -516,11 +516,11 @@ the next command fails because {\tt p} does not bind in
the instance of {\tt n}.
\begin{coq_eval}
Set Printing Depth 50.
-(********** The following produces **********)
-(**** The reference p was not found in the current environment ********)
\end{coq_eval}
+% (********** The following produces **********)
+% (**** The reference p was not found in the current environment ********)
\begin{coq_example}
-Check (exists_different p).
+Fail Check (exists_different p).
\end{coq_example}
\Rem Binding variables must not necessarily be parsed using the
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index c3d8ad531..52f32d0c7 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -343,7 +343,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
This behaves like {\tt apply} but it reasons modulo conversion only
on subterms that contain no variables to instantiate. For instance,
the following example does not succeed because it would require the
- conversion of {\tt id ?1234} and {\tt O}.
+ conversion of {\tt id ?foo} and {\tt O}.
\begin{coq_eval}
Reset Initial.
@@ -354,7 +354,7 @@ Hypothesis H : forall y, id y = y.
Goal O = O.
\end{coq_example*}
\begin{coq_example}
-simple apply H.
+Fail simple apply H.
\end{coq_example}
Because it reasons modulo a limited amount of conversion, {\tt
@@ -419,7 +419,7 @@ no value for {\tt y} in {\tt Rtrans} is found by {\tt apply}:
%(**** Error: generated subgoal (R n ?17) has metavariables in it *****)
%\end{coq_eval}
\begin{coq_example}
-apply Rtrans.
+Fail apply Rtrans.
\end{coq_example}
A solution is to apply {\tt (Rtrans n m p)} or {\tt (Rtrans n m)}.
@@ -914,10 +914,10 @@ containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$}
\begin{coq_example}
Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
intros * [a | (_,c)] f.
-apply (f a).
-exact c.
-Qed.
\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
\Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to
\texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons:
@@ -935,7 +935,7 @@ Qed.
Goal forall n:nat, n = 0 -> n = 0.
intros [ | ] H.
Show 2.
-Undo 2.
+Undo.
intros [ | ]; intros H.
Show 2.
\end{coq_example}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 22:46:04 +0000