diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-17 08:05:56 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-17 08:05:56 +0000 |
| commit | 715e002ab56561fc3ecd5fc922459a9e9a8001b0 (patch) | |
| tree | efb7a855ddbae5ba15553f41633f6b0e8f2a305b /toplevel | |
| parent | 10ef3e09d2f602ac039684e8ee121dc908137a3a (diff) | |
pb facto des Fixpoint + erreur avec -dump-glob et Load
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7768fa95b..2607ca411 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -163,10 +163,13 @@ let pr_new_syntax loc ocom = let rec vernac_com interpfun (loc,com) = let rec interp = function | VernacLoad (verbosely, fname) -> + (* translator state *) let ch = !chan_translate in let cs = Lexer.com_state() in - let lt = Lexer.location_table() in let cl = !Pp.comments in + (* end translator state *) + (* coqdoc state *) + let cds = Constrintern.coqdoc_freeze() in if !Options.translate_file then begin let _,f = find_file_in_path (Library.get_load_path ()) (make_suffix fname ".v") in @@ -178,14 +181,14 @@ let rec vernac_com interpfun (loc,com) = if !Options.translate_file then close_out !chan_translate; chan_translate := ch; Lexer.restore_com_state cs; - Lexer.restore_location_table lt; - Pp.comments := cl + Pp.comments := cl; + Constrintern.coqdoc_unfreeze cds; with e -> if !Options.translate_file then close_out !chan_translate; chan_translate := ch; Lexer.restore_com_state cs; - Lexer.restore_location_table lt; Pp.comments := cl; + Constrintern.coqdoc_unfreeze cds; raise e end; | VernacList l -> List.iter (fun (_,v) -> interp v) l |