From d134b5afaf26a67149d999e95bd21b264b61429b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Oct 2003 19:05:52 +0000
Subject: Conjecture declare maintenant un axiome; reorganisation
 VernacDefinition

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

(limited to 'ide')

diff --git a/ide/coq.ml b/ide/coq.ml
index 487bc13a6b..1f0efbe713 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -286,7 +286,7 @@ let word_class s =
 type reset_info = NoReset | Reset of Names.identifier * bool ref
 
 let compute_reset_info = function 
-  | VernacDefinition (_, id, DefineBody _, _, _) 
+  | VernacDefinition (_, id, DefineBody _, _) 
   | VernacBeginSection id 
   | VernacDefineModule (id, _, _, _) 
   | VernacDeclareModule (id, _, _, _)
@@ -294,7 +294,7 @@ let compute_reset_info = function
   | VernacAssumption (_, (_,(id,_))::_)
   | VernacInductive (_, (id,_,_,_,_) :: _) ->
       Reset (id, ref true)
-  | VernacDefinition (_, id, ProveBody _, _, _)
+  | VernacDefinition (_, id, ProveBody _, _)
   | VernacStartTheoremProof (_, id, _, _, _) ->
       Reset (id, ref false)
   | _ -> NoReset
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ae04c8d642..13d916480c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -499,7 +499,7 @@ let is_empty () = Stack.is_empty processed_stack
 
 let update_on_end_of_proof id =
   let lookup_lemma = function
-  | { ast = _, ( VernacDefinition (_, _, ProveBody _, _, _)
+  | { ast = _, ( VernacDefinition (_, _, ProveBody _, _)
 	       | VernacDeclareTacticDefinition _
 	       | VernacStartTheoremProof _) ; 
       reset_info = Reset (_, r) } -> 
@@ -1316,7 +1316,7 @@ Please restart and report NOW.";
 	  | { ast = _, ( VernacStartTheoremProof _ 
 		       | VernacGoal _
 		       | VernacDeclareTacticDefinition _
-		       | VernacDefinition (_,_,ProveBody _,_,_));
+		       | VernacDefinition (_,_,ProveBody _,_));
 	      reset_info=Reset(id,{contents=false})} ->
 	      ignore (pop ());
 	      (try 
-- 
cgit v1.2.3