diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index c38b8fa820..c6a8fdaa55 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -429,6 +429,11 @@ let quit = ref false (** Disabled *) let print_ast id = Xml_datatype.PCData "ERROR" +let idetop_make_cases iname = + let qualified_iname = Libnames.qualid_of_string iname in + let iref = Nametab.global_inductive qualified_iname in + ComInductive.make_cases iref + (** Grouping all call handlers together + error handling *) let eval_call c = let interruptible f x = @@ -449,7 +454,7 @@ let eval_call c = Interface.search = interruptible search; Interface.get_options = interruptible get_options; Interface.set_options = interruptible set_options; - Interface.mkcases = interruptible Vernacentries.make_cases; + Interface.mkcases = interruptible idetop_make_cases; Interface.quit = (fun () -> quit := true); Interface.init = interruptible init; Interface.about = interruptible about; |