diff options
| author | herbelin | 2003-11-29 17:42:21 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-29 17:42:21 +0000 |
| commit | 7fd2b52138b1db66bb09a06508dd8d1a7e3c04d8 (patch) | |
| tree | 2b5942e4b1a46a6dde1f0a096aa88068617c874b /toplevel | |
| parent | 55c6233ea9f740d2109ab4dcece2cd886059fe82 (diff) | |
Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7; Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5029 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 3865926353..bdb5e68d41 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -58,8 +58,7 @@ let inputstate () = match !inputstate with | Some "" -> () | Some s -> intern_state s - | None -> - intern_state (if !Options.v7 then "initial.coq" else "initialnew.coq") + | None -> intern_state "initial.coq" let outputstate = ref "" let set_outputstate s = outputstate:=s |