diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-13 15:29:02 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-13 15:29:02 +0000 |
| commit | e32ca6edd210ccc11fb68d64af26a82354ea44aa (patch) | |
| tree | b9c4b0faace8389c31bbce0d36e763d7e8abbfb2 | |
| parent | f1bd83d9d6f69a0309572f1bfe22827d4c3f4eb7 (diff) | |
CoqIDE: undo plus efficace sur les inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4157 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/coq.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 6a21e451d..c71669994 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -272,7 +272,8 @@ let compute_reset_info = function | VernacDefineModule (id, _, _, _) | VernacDeclareModule (id, _, _, _) | VernacDeclareModuleType (id, _, _) - | VernacAssumption (_, (_,(id,_))::_) -> + | VernacAssumption (_, (_,(id,_))::_) + | VernacInductive (_, (id,_,_,_,_) :: _) -> Reset (id, ref true) | VernacDefinition (_, id, ProveBody _, _, _) | VernacStartTheoremProof (_, id, _, _, _) -> |