From 767920af6289d2b7916cc57d4de18316026d7fa9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Oct 2003 07:52:08 +0000
Subject: Syntaxe VernacEndProof changee pour ajout mot-cle 'Admitted'

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

diff --git a/ide/coqide.ml b/ide/coqide.ml
index f466bafaff..ae04c8d642 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -537,7 +537,7 @@ let push_phrase start_of_phrase_mark end_of_phrase_mark ast =
   in
   push x;
   match snd ast with
-    | VernacEndProof (_, None) -> update_on_end_of_proof ()
+    | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
     | VernacEndSegment id -> update_on_end_of_segment id
     | _ -> ()
 
@@ -545,7 +545,7 @@ let repush_phrase x =
   let x = { x with reset_info = Coq.compute_reset_info (snd x.ast) } in
   push x;
   match snd x.ast with
-    | VernacEndProof (_, None) -> update_on_end_of_proof ()
+    | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
     | VernacEndSegment id -> update_on_end_of_segment id
     | _ -> ()
 
-- 
cgit v1.2.3