diff options
| author | herbelin | 2011-07-16 20:35:13 +0000 |
|---|---|---|
| committer | herbelin | 2011-07-16 20:35:13 +0000 |
| commit | 6a4c604f17719bd782efd71517a865d327ec6b0e (patch) | |
| tree | 3356c3aa6a98cfe3681da988428f812a5628fb41 /interp | |
| parent | 928070fda675de585b40e8f8eca500d2695f09b9 (diff) | |
Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and <- when a variable is about to be substituted (subst_one rewrite the whole context at once, while multi_rewrite rewrites each hyp independently, what may break typing in case of dependencies). Also generalize "dependent rewrite" to "sig" (to be done: generalize it to eq_dep, eq_dep1, and any dependent tuple).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14279 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |