diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.ml | 10 | ||||
| -rw-r--r-- | interp/coqlib.mli | 2 |
2 files changed, 11 insertions, 1 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 204b2b226f..eb7828eaa6 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -187,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"; @@ -363,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") diff --git a/interp/coqlib.mli b/interp/coqlib.mli index aac1206e10..5d3580f26a 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -104,6 +104,7 @@ type coq_sigma_data = { val build_sigma_set : coq_sigma_data delayed val build_sigma_type : coq_sigma_data delayed +val build_sigma : coq_sigma_data delayed (** Non-dependent pairs in Set from Datatypes *) val build_prod : coq_sigma_data delayed @@ -175,6 +176,7 @@ val coq_jmeq_ref : global_reference lazy_t val coq_eq_true_ref : global_reference lazy_t val coq_existS_ref : global_reference lazy_t val coq_existT_ref : global_reference lazy_t +val coq_exist_ref : global_reference lazy_t val coq_not_ref : global_reference lazy_t val coq_False_ref : global_reference lazy_t val coq_sumbool_ref : global_reference lazy_t |