From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 checker/include | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

(limited to 'checker/include')

diff --git a/checker/include b/checker/include
index b7d46d4b..f5bd2984 100644
--- a/checker/include
+++ b/checker/include
@@ -12,10 +12,12 @@
 #directory "lib";;
 #directory "kernel";;
 #directory "checker";;
+#directory "+threads";;
 #directory "+camlp4";;
 #directory "+camlp5";;
 
 #load "unix.cma";;
+#load"threads.cma";;
 #load "str.cma";;
 #load "gramlib.cma";;
 (*#load "toplevellib.cma";;
@@ -29,12 +31,14 @@ open Typeops;;
 open Check;;
 
 open Pp;;
+open Errors;;
 open Util;;
 open Names;;
 open Term;;
 open Environ;;
 open Declarations;;
 open Mod_checking;;
+open Cic;;
 
 let pr_id id = str(string_of_id id)
 let pr_na = function Name id -> pr_id id | _ -> str"_";;
@@ -111,23 +115,33 @@ let prsub s =
 (*#install_printer prenvu;;
 #install_printer prsub;;*)
 
-Checker.init_with_argv [|""|];;
+Checker.init_with_argv [|"";"-coqlib";"."|];;
 Flags.make_silent false;;
 Flags.debug := true;;
 Sys.catch_break true;;
 
 let module_of_file f =
   let (_,mb,_,_) = Obj.magic ((intern_from_file f).library_compiled) in
-  (mb:module_body)
+  (mb:Cic.module_body)
 ;;
+let deref_mod md s =
+  let l = match md.mod_expr with
+      Struct(NoFunctor l) -> l 
+    | FullStruct ->
+      (match md.mod_type with
+	NoFunctor l -> l)
+ in
+  List.assoc (label_of_id(id_of_string s)) l
+;;
+(*
 let mod_access m fld =
   match m.mod_expr with
       Some(SEBstruct l) -> List.assoc fld l
     | _ -> failwith "bad structure type"
 ;;
-
+*)
 let parse_dp s =
-  make_dirpath(List.map id_of_string (List.rev (Str.split(Str.regexp"\\.") s)))
+  make_dirpath(List.rev_map id_of_string (Str.split(Str.regexp"\\.") s))
 ;;
 let parse_sp s =
   let l = List.rev (Str.split(Str.regexp"\\.") s) in
@@ -160,10 +174,6 @@ let read_mod s f =
     (dir_path * Digest.t) list *
     engagement option);;
 
-let deref_mod md s =
-  let (Some (SEBstruct l)) = md.mod_expr in
-  List.assoc (label_of_id(id_of_string s)) l
-;;
 
 let expln f x =
   try f x
-- 
cgit v1.2.3