From 22a24e1cadd4e1206db195c9ef19ca3130eb1bc8 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 16 Dec 2003 15:54:06 +0000
Subject: tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8401 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Program.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/Program.tex')

diff --git a/doc/Program.tex b/doc/Program.tex
index ddcf8d920f..aa900ecb90 100644
--- a/doc/Program.tex
+++ b/doc/Program.tex
@@ -607,7 +607,7 @@ Lemma permut_app_app : (m1,m2,n1,n2 :list)
      (permut m1 n1)->(permut m2 n2)->(permut (app m1 m2) (app n1 n2)).
         Intros m1 m2 n1 n2 h1 h2.
         Elim h1 ; Intros.
-        Exact h2.
+        exact h2.
         Apply permut_tran with (app m n2) ; Auto.
         Apply permut_tran with (app m m2) ; Auto.
         Auto.
@@ -692,7 +692,7 @@ Inductive sort : list->Prop :=
 Hints Resolve sort_nil sort_mil.
 Lemma permutapp : (a0:A)(y,l1,l2:list)(permut y (app l1 l2))->(permut (cons a0 y) (app l1 (cons a0 l2))).
 Intros.
-Exact (permut_cmil a0 y l1 l2 H).
+exact (permut_cmil a0 y l1 l2 H).
 Save.
 Hints Resolve permutapp.
 Lemma sortmil : (a:A)(x,x0,l1,l2:list)(sup_list a l1)->(inf_list a l2)->(sort x)->(sort x0)->(permut l1 x)->(permut l2 x0)->(sort (mil a x x0)).
-- 
cgit v1.2.3