summaryrefslogtreecommitdiff
path: root/interp/coqlib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/coqlib.ml')
-rw-r--r--interp/coqlib.ml39
1 files changed, 17 insertions, 22 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index c5850abf..d9649976 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqlib.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
open Pp
open Names
@@ -44,8 +42,8 @@ let global_of_extended q =
let gen_constant_in_modules locstr dirs s =
let dirs = List.map make_dir dirs in
- let id = id_of_string s in
- let all = Nametab.locate_extended_all (qualid_of_ident id) in
+ let qualid = qualid_of_string s in
+ let all = Nametab.locate_extended_all qualid in
let all = list_uniquize (list_map_filter global_of_extended all) in
let these = List.filter (has_suffix_in_dirs dirs) all in
match these with
@@ -93,10 +91,12 @@ let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
let arith_dir = ["Coq";"Arith"]
let arith_modules = [arith_dir]
+let numbers_dir = [ "Coq";"Numbers"]
+let parith_dir = ["Coq";"PArith"]
let narith_dir = ["Coq";"NArith"]
-
let zarith_dir = ["Coq";"ZArith"]
-let zarith_base_modules = [narith_dir;zarith_dir]
+
+let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir]
let init_dir = ["Coq";"Init"]
let init_modules = [
@@ -108,11 +108,6 @@ let init_modules = [
init_dir@["Wf"]
]
-let coq_id = id_of_string "Coq"
-let init_id = id_of_string "Init"
-let arith_id = id_of_string "Arith"
-let datatypes_id = id_of_string "Datatypes"
-
let logic_module_name = ["Coq";"Init";"Logic"]
let logic_module = make_dir logic_module_name
@@ -137,7 +132,7 @@ let make_con dir id = Libnames.encode_con dir id
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)
+let _ = Termops.set_impossible_default_clause (mkConst id,mkConst type_of_id)
(** Natural numbers *)
let nat_kn = make_kn datatypes_module (id_of_string "nat")
@@ -192,10 +187,17 @@ let build_sigma_set () = anomaly "Use build_sigma_type"
let build_sigma_type () =
{ proj1 = init_constant ["Specif"] "projT1";
proj2 = init_constant ["Specif"] "projT2";
- elim = init_constant ["Specif"] "sigT_rec";
+ elim = init_constant ["Specif"] "sigT_rect";
intro = init_constant ["Specif"] "existT";
typ = init_constant ["Specif"] "sigT" }
+let build_sigma () =
+ { proj1 = init_constant ["Specif"] "proj1_sig";
+ proj2 = init_constant ["Specif"] "proj2_sig";
+ elim = init_constant ["Specif"] "sig_rect";
+ intro = init_constant ["Specif"] "exist";
+ typ = init_constant ["Specif"] "sig" }
+
let build_prod () =
{ proj1 = init_constant ["Datatypes"] "fst";
proj2 = init_constant ["Datatypes"] "snd";
@@ -227,8 +229,6 @@ let lazy_logic_constant dir id = lazy (logic_constant dir id)
let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl"
let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
-let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec"
-let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect"
let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
let coq_eq_sym = lazy_init_constant ["Logic"] "eq_sym"
let coq_eq_trans = lazy_init_constant ["Logic"] "eq_trans"
@@ -250,8 +250,6 @@ let build_coq_eq_refl () = Lazy.force coq_eq_refl
let build_coq_eq_sym () = Lazy.force coq_eq_sym
let build_coq_f_equal2 () = Lazy.force coq_f_equal2
-let build_coq_sym_eq = build_coq_eq_sym (* compatibility *)
-
let build_coq_inversion_eq_data () =
let _ = check_required_library logic_module_name in {
inv_eq = Lazy.force coq_eq_eq;
@@ -263,8 +261,6 @@ let build_coq_inversion_eq_data () =
let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq"
let coq_jmeq_refl = lazy_logic_constant ["JMeq"] "JMeq_refl"
let coq_jmeq_ind = lazy_logic_constant ["JMeq"] "JMeq_ind"
-let coq_jmeq_rec = lazy_logic_constant ["JMeq"] "JMeq_rec"
-let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect"
let coq_jmeq_sym = lazy_logic_constant ["JMeq"] "JMeq_sym"
let coq_jmeq_congr = lazy_logic_constant ["JMeq"] "JMeq_congr"
let coq_jmeq_trans = lazy_logic_constant ["JMeq"] "JMeq_trans"
@@ -300,8 +296,6 @@ let build_coq_sumbool () = Lazy.force coq_sumbool
let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity"
let coq_identity_refl = lazy_init_constant ["Datatypes"] "identity_refl"
let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
-let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
-let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr"
let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym"
let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans"
@@ -376,6 +370,7 @@ let coq_jmeq_ref = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true")
let coq_existS_ref = lazy (anomaly "use coq_existT_ref")
let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
+let coq_exist_ref = lazy (init_reference ["Specif"] "exist")
let coq_not_ref = lazy (init_reference ["Logic"] "not")
let coq_False_ref = lazy (init_reference ["Logic"] "False")
let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")