aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-04-07 15:08:12 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-04-07 15:08:12 +0000
commit26ca22424b286f5ff22a1fa97c38d15e224b3dc2 (patch)
tree190e12acf505e47d3a81ef0fd625a405ff782c04 /interp/coqlib.mli
parent5f9b04da0f3c72f4b582cd094edae721b1bc9a9e (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/coqlib.mli')
-rw-r--r--interp/coqlib.mli2
1 files changed, 2 insertions, 0 deletions
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;