diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 96073d71a6..fee070fd65 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -53,7 +53,7 @@ will be first rewrote to: (match x as y return (x = y -> _) with | 0 => fun H : x = 0 -> t | S n => fun H : x = S n -> u - end) (refl_equal n). + end) (eq_refl n). \end{coq_example*} This permits to get the proper equalities in the context of proof |