diff options
| author | herbelin | 2009-08-03 20:50:11 +0000 |
|---|---|---|
| committer | herbelin | 2009-08-03 20:50:11 +0000 |
| commit | f9f35dc36f5249a2de18005ab59ae934e0fa7075 (patch) | |
| tree | 4d3dd839db319df1945c8fef474284e6f4e5f3e3 /interp/coqlib.mli | |
| parent | 25dde2366a4db47e5da13b2bbe4d03a31235706f (diff) | |
Added "etransitivity".
Added support for "injection" and "discriminate" on JMeq.
Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.
Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/coqlib.mli')
| -rw-r--r-- | interp/coqlib.mli | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 7e13b1b1ed..5b550a86bf 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -76,6 +76,8 @@ val glob_false : global_reference (* Equality *) val glob_eq : global_reference +val glob_identity : global_reference +val glob_jmeq : global_reference (*s Constructions and patterns related to Coq initial state are unknown at compile time. Therefore, we can only provide methods to build @@ -104,22 +106,23 @@ val build_sigma_type : coq_sigma_data delayed (* Non-dependent pairs in Set from Datatypes *) val build_prod : coq_sigma_data delayed -type coq_leibniz_eq_data = { +type coq_eq_data = { eq : constr; - refl : constr; ind : constr; - rrec : constr option; - rect : constr option; - congr: constr; - sym : constr } + refl : constr; + sym : constr; + trans: constr; + congr: constr } -val build_coq_eq_data : coq_leibniz_eq_data delayed -val build_coq_identity_data : coq_leibniz_eq_data delayed +val build_coq_eq_data : coq_eq_data delayed +val build_coq_identity_data : coq_eq_data delayed +val build_coq_jmeq_data : coq_eq_data delayed val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *) val build_coq_eq_sym : constr delayed (* = [(build_coq_eq_data()).sym] *) val build_coq_f_equal2 : constr delayed + (* Specif *) val build_coq_sumbool : constr delayed @@ -150,6 +153,7 @@ val build_coq_ex : constr delayed val coq_eq_ref : global_reference lazy_t val coq_identity_ref : global_reference lazy_t +val coq_jmeq_ref : global_reference lazy_t val coq_existS_ref : global_reference lazy_t val coq_existT_ref : global_reference lazy_t val coq_not_ref : global_reference lazy_t |