diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-07 15:08:12 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-07 15:08:12 +0000 |
| commit | 26ca22424b286f5ff22a1fa97c38d15e224b3dc2 (patch) | |
| tree | 190e12acf505e47d3a81ef0fd625a405ff782c04 /interp | |
| parent | 5f9b04da0f3c72f4b582cd094edae721b1bc9a9e (diff) | |
- Documentation of the Program tactics.
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.ml | 7 | ||||
| -rw-r--r-- | interp/coqlib.mli | 2 |
2 files changed, 9 insertions, 0 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 8a55bfc2c..f9a1c6466 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -166,6 +166,13 @@ let build_sigma_type () = intro = init_constant ["Specif"] "existT"; typ = init_constant ["Specif"] "sigT" } +let build_prod () = + { proj1 = init_constant ["Datatypes"] "fst"; + proj2 = init_constant ["Datatypes"] "snd"; + elim = init_constant ["Datatypes"] "prod_rec"; + intro = init_constant ["Datatypes"] "pair"; + typ = init_constant ["Datatypes"] "prod" } + (* Equalities *) type coq_leibniz_eq_data = { eq : constr; diff --git a/interp/coqlib.mli b/interp/coqlib.mli index ed5e46c1a..098dad1d5 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -94,6 +94,8 @@ type coq_sigma_data = { val build_sigma_set : coq_sigma_data delayed 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 = { eq : constr; |