diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:05:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:13:30 +0100 |
| commit | e98d3c3793f26265a49f63a6e78d704f88341df9 (patch) | |
| tree | c0328afc0034f3262dca2ca067531ee19bbb0ee0 /toplevel/vernacentries.ml | |
| parent | 103ec7205d9038f1f3821f9287e3bb0907a1e3ec (diff) | |
| parent | 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b6a4ab93e..b3512ffde 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2048,7 +2048,7 @@ let check_vernac_supports_polymorphism c p = let enforce_polymorphism = function | None -> Flags.is_universe_polymorphism () - | Some b -> b + | Some b -> Flags.make_polymorphic_flag b; b (** A global default timeout, controled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) @@ -2149,7 +2149,8 @@ let interp ?(verbosely=true) ?proof (loc,c) = then Flags.verbosely (interp ?proof ~loc locality poly) c else Flags.silently (interp ?proof ~loc locality poly) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then - Flags.program_mode := orig_program_mode + Flags.program_mode := orig_program_mode; + ignore (Flags.use_polymorphic_flag ()) end with | reraise when @@ -2161,6 +2162,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = let e = locate_if_not_already loc e in let () = restore_timeout () in Flags.program_mode := orig_program_mode; + ignore (Flags.use_polymorphic_flag ()); iraise e and aux_list ?locality ?polymorphism isprogcmd l = List.iter (aux false) (List.map snd l) |