From 4f254ec43f306d289c17286e86a9aface2998224 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 30 Nov 2011 15:50:01 +0000
Subject: More type safety in query GADT (again).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14753 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/ide_intf.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 1dade4085b..0feceb5375 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -43,15 +43,15 @@ let mkcases s : string list list call = MkCases s
 let abstract_eval_call handler c =
   try
     let res = match c with
-      | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s))
-      | Rewind i -> Obj.magic (handler.rewind i)
-      | Goal -> Obj.magic (handler.goals ())
-      | Hints -> Obj.magic (handler.hints ())
-      | Status -> Obj.magic (handler.status ())
-      | GetOptions -> Obj.magic (handler.get_options ())
-      | SetOptions opts -> Obj.magic (handler.set_options opts)
-      | InLoadPath s -> Obj.magic (handler.inloadpath s)
-      | MkCases s -> Obj.magic (handler.mkcases s)
+      | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s) : string)
+      | Rewind i -> Obj.magic (handler.rewind i : int)
+      | Goal -> Obj.magic (handler.goals () : goals)
+      | Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
+      | Status -> Obj.magic (handler.status () : status)
+      | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
+      | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
+      | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
+      | MkCases s -> Obj.magic (handler.mkcases s : string list list)
     in Good res
   with e ->
     let (l, str) = handler.handle_exn e in
-- 
cgit v1.2.3