diff options
| author | Hugo Herbelin | 2016-11-04 19:34:40 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-11-04 19:36:09 +0100 |
| commit | dc4200a1c0e37a600537fd1809377a3137ce0cc3 (patch) | |
| tree | 69ecf19bc376ec2fddb95f9eb89529027ed73591 | |
| parent | 94bdd90bacc4d4a92b79bbe0db532e523fbcbce8 (diff) | |
Quick fix of tactic parsing while Load-ing in coqide.
Note that this is still broken when loading files containing C-zar scripts.
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c03f183ff5..ef530d590f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1906,6 +1906,10 @@ let vernac_check_guard () = exception End_of_input let vernac_load interp fname = + let interp x = + let proof_mode = Proof_global.get_default_proof_mode_name () in + Proof_global.activate_proof_mode proof_mode; + interp x in let parse_sentence = Flags.with_option Flags.we_are_parsing (fun po -> match Pcoq.Gram.entry_parse Pcoq.main_entry po with |