Réorganisation des points d'appui du undo de CoqIDE (type reset_info).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10990 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index dce435087..889e4bff5 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -347,9 +347,9 @@ type reset_mark =
 
 type reset_info =
   | NoReset
-  | ResetAtDecl of reset_mark * bool ref
   | ResetAtSegmentStart of Names.identifier * bool ref 
-  | ResetAtFrozenState of Libnames.object_name * bool ref
+  | ResetAtStatement of reset_mark * bool ref
+  | ResetAtRegisteredObject of reset_mark * bool ref
 
 let reset_mark id = match Lib.has_top_frozen_state () with
   | Some sp -> ResetToState sp
@@ -365,15 +365,15 @@ let compute_reset_info = function
   | VernacDefinition (_, (_,id), DefineBody _, _)
   | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
   | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
-      ResetAtDecl (reset_mark id, ref true)
+      ResetAtRegisteredObject (reset_mark id, ref true)
 
   | VernacDefinition (_, (_,id), ProveBody _, _)
   | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
-      ResetAtDecl (reset_mark id, ref false)
+      ResetAtStatement (reset_mark id, ref false)
 
   | VernacEndProof _ | VernacEndSegment _ -> NoReset
   | _ -> match Lib.has_top_frozen_state () with
-      | Some sp -> ResetAtFrozenState (sp, ref true)
+      | Some sp -> ResetAtRegisteredObject (ResetToState sp, ref true)
       | None -> NoReset
 
 let reset_initial () =