diff options
| -rw-r--r-- | doc/newfaq/main.tex | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index 9f1b796930..5c26a19d3e 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -756,15 +756,15 @@ You can use the {\tt Admitted} command to state your current proof as an axiom. You can use the \discriminate tactic. -%\begin{coq_example} -%Inductive toto : Set := -% C1 : toto -% | C2 : toto. +\begin{coq_example} +Inductive toto : Set := + C1 : toto + | C2 : toto. -%Goal C1 <> C2. -%discriminate. -%Qed. -%\end{coq_example} +Goal C1 <> C2. +discriminate. +Qed. +\end{coq_example} \Question[coqccoqtop]{What is the difference between coqc et coqtop ?} |