summaryrefslogtreecommitdiff
path: root/interp/coqlib.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /interp/coqlib.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'interp/coqlib.ml')
-rw-r--r--interp/coqlib.ml36
1 files changed, 25 insertions, 11 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 0c3ffd0c..65e4dcd5 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqlib.ml 10067 2007-08-09 17:13:16Z msozeau $ *)
+(* $Id: coqlib.ml 11072 2008-06-08 16:13:37Z herbelin $ *)
open Util
open Pp
@@ -36,13 +36,6 @@ let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
let gen_reference = coq_reference
let gen_constant = coq_constant
-let list_try_find f =
- let rec try_find_f = function
- | [] -> raise Not_found
- | h::t -> try f h with Not_found -> try_find_f t
- in
- try_find_f
-
let has_suffix_in_dirs dirs ref =
let dir = dirpath (sp_of_global ref) in
List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
@@ -77,7 +70,7 @@ let check_required_library d =
(dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
*)
(* or failing ...*)
- error ("Library "^(list_last d)^" has to be required first")
+ error ("Library "^(string_of_dirpath dir)^" has to be required first")
(************************************************************************)
(* Specific Coq objects *)
@@ -109,13 +102,22 @@ let init_id = id_of_string "Init"
let arith_id = id_of_string "Arith"
let datatypes_id = id_of_string "Datatypes"
-let logic_module = make_dir ["Coq";"Init";"Logic"]
+let logic_module_name = ["Coq";"Init";"Logic"]
+let logic_module = make_dir logic_module_name
let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
let arith_module = make_dir ["Coq";"Arith";"Arith"]
(* TODO: temporary hack *)
let make_kn dir id = Libnames.encode_kn dir id
+let make_con dir id = Libnames.encode_con dir id
+
+(** Identity *)
+
+let id = make_con datatypes_module (id_of_string "id")
+let type_of_id = make_con datatypes_module (id_of_string "ID")
+
+let _ = Cases.set_impossible_default_clause (mkConst id,mkConst type_of_id)
(** Natural numbers *)
let nat_kn = make_kn datatypes_module (id_of_string "nat")
@@ -150,8 +152,19 @@ type coq_sigma_data = {
intro : constr;
typ : constr }
+type coq_bool_data = {
+ andb : constr;
+ andb_prop : constr;
+ andb_true_intro : constr}
+
type 'a delayed = unit -> 'a
+let build_bool_type () =
+ { andb = init_constant ["Datatypes"] "andb";
+ andb_prop = init_constant ["Datatypes"] "andb_prop";
+ andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" }
+
+
let build_sigma_set () = anomaly "Use build_sigma_type"
let build_sigma_type () =
@@ -190,7 +203,8 @@ let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
let coq_eq_sym = lazy_init_constant ["Logic"] "sym_eq"
let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
-let build_coq_eq_data () = {
+let build_coq_eq_data () =
+ let _ = check_required_library logic_module_name in {
eq = Lazy.force coq_eq_eq;
refl = Lazy.force coq_eq_refl;
ind = Lazy.force coq_eq_ind;