diff options
Diffstat (limited to 'interp/coqlib.ml')
| -rw-r--r-- | interp/coqlib.ml | 84 |
1 files changed, 23 insertions, 61 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 3a0a5047b..ba3b3d872 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -23,8 +23,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let gen_reference locstr dir s = let dir = make_dir ("Coq"::dir) in - let id = Constrextern.id_of_v7_string s in - let sp = Libnames.make_path dir id in + let sp = Libnames.make_path dir (id_of_string s) in try Nametab.absolute_reference sp with Not_found -> @@ -46,7 +45,7 @@ let has_suffix_in_dirs dirs ref = let gen_constant_in_modules locstr dirs s = let dirs = List.map make_dir dirs in - let id = Constrextern.id_of_v7_string s in + let id = id_of_string s in let all = Nametab.locate_all (make_short_qualid id) in let these = List.filter (has_suffix_in_dirs dirs) all in match these with @@ -181,9 +180,10 @@ let build_coq_eq_data () = { rrec = Some (Lazy.force coq_eq_rec); rect = Some (Lazy.force coq_eq_rect); congr = Lazy.force coq_eq_congr; - sym = Lazy.force coq_eq_sym } + sym = Lazy.force coq_eq_sym } let build_coq_eq () = Lazy.force coq_eq_eq +let build_coq_sym_eq () = Lazy.force coq_eq_sym let build_coq_f_equal2 () = Lazy.force coq_f_equal2 (* Specif *) @@ -191,56 +191,23 @@ let coq_sumbool = lazy_init_constant ["Specif"] "sumbool" let build_coq_sumbool () = Lazy.force coq_sumbool -(* Equality on Type *) - -let coq_eqT_eq = lazy_init_constant ["Logic"] "eq" -let coq_eqT_refl = lazy_init_constant ["Logic"] "refl_equal" -let coq_eqT_ind = lazy_init_constant ["Logic"] "eq_ind" -let coq_eqT_congr =lazy_init_constant ["Logic"] "f_equal" -let coq_eqT_sym = lazy_init_constant ["Logic"] "sym_eq" - -let build_coq_eqT_data () = { - eq = Lazy.force coq_eqT_eq; - refl = Lazy.force coq_eqT_refl; - ind = Lazy.force coq_eqT_ind; - rrec = None; - rect = None; - congr = Lazy.force coq_eqT_congr; - sym = Lazy.force coq_eqT_sym } - -let build_coq_eqT () = Lazy.force coq_eqT_eq -let build_coq_sym_eqT () = Lazy.force coq_eqT_sym - (* Equality on Type as a Type *) -let coq_idT_eq = lazy_init_constant ["Datatypes"] "identity" -let coq_idT_refl = lazy_init_constant ["Datatypes"] "refl_identity" -let coq_idT_ind = lazy_init_constant ["Datatypes"] "identity_ind" -let coq_idT_rec = lazy_init_constant ["Datatypes"] "identity_rec" -let coq_idT_rect = lazy_init_constant ["Datatypes"] "identity_rect" -let coq_idT_congr = lazy_init_constant ["Logic_Type"] "congr_id" -let coq_idT_sym = lazy_init_constant ["Logic_Type"] "sym_id" - -let build_coq_idT_data () = { - eq = Lazy.force coq_idT_eq; - refl = Lazy.force coq_idT_refl; - ind = Lazy.force coq_idT_ind; - rrec = Some (Lazy.force coq_idT_rec); - rect = Some (Lazy.force coq_idT_rect); - congr = Lazy.force coq_idT_congr; - sym = Lazy.force coq_idT_sym } - -let lazy_init_constant_v7 d id id7 = - if !Options.v7 then lazy_init_constant d id else - lazy (anomaly - (id7^" does no longer exist in V8 new syntax, use "^id - ^" instead (probably an error in ML contributed code)")) - -(* Empty Type *) -let coq_EmptyT = lazy_init_constant_v7 ["Logic"] "False" "EmptyT" - -(* Unit Type and its unique inhabitant *) -let coq_UnitT = lazy_init_constant_v7 ["Datatypes"] "unit" "UnitT" -let coq_IT = lazy_init_constant_v7 ["Datatypes"] "tt" "IT" +let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity" +let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity" +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"] "congr_id" +let coq_identity_sym = lazy_init_constant ["Logic_Type"] "sym_id" + +let build_coq_identity_data () = { + eq = Lazy.force coq_identity_eq; + refl = Lazy.force coq_identity_refl; + ind = Lazy.force coq_identity_ind; + rrec = Some (Lazy.force coq_identity_rec); + rect = Some (Lazy.force coq_identity_rect); + congr = Lazy.force coq_identity_congr; + sym = Lazy.force coq_identity_sym } (* The False proposition *) let coq_False = lazy_init_constant ["Logic"] "False" @@ -256,10 +223,6 @@ let coq_or = lazy_init_constant ["Logic"] "or" let coq_ex = lazy_init_constant ["Logic"] "ex" (* Runtime part *) -let build_coq_EmptyT () = Lazy.force coq_EmptyT -let build_coq_UnitT () = Lazy.force coq_UnitT -let build_coq_IT () = Lazy.force coq_IT - let build_coq_True () = Lazy.force coq_True let build_coq_I () = Lazy.force coq_I @@ -285,8 +248,8 @@ let coq_eq_pattern = lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)")) let coq_eqT_pattern = lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)")) -let coq_idT_pattern = - lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identityT ?1 ?2 ?3)")) +let coq_identity_pattern = + lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identity ?1 ?2 ?3)")) let coq_existS_pattern = lazy (snd (parse_pattern "(Coq.Init.Specif.existS ?1 ?2 ?3 ?4)")) let coq_existT_pattern = @@ -305,8 +268,7 @@ let coq_eqdec_pattern = (* The following is less readable but does not depend on parsing *) let coq_eq_ref = lazy (init_reference ["Logic"] "eq") -let coq_eqT_ref = coq_eq_ref -let coq_idT_ref = lazy (init_reference ["Datatypes"] "identity") +let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") let coq_existS_ref = lazy (init_reference ["Specif"] "existS") let coq_existT_ref = lazy (init_reference ["Specif"] "existT") let coq_not_ref = lazy (init_reference ["Logic"] "not") |