diff options
| author | corbinea | 2002-05-22 09:16:38 +0000 |
|---|---|---|
| committer | corbinea | 2002-05-22 09:16:38 +0000 |
| commit | aacf4aec2dd3ff6bb8e96dc638ea28dbd5d3f1d4 (patch) | |
| tree | 9085f832b8d784c94e09280143103ea6d6f2f673 /tactics/hipattern.mli | |
| parent | cbe9f6c3d08bd854a0908448e6085505b67851c8 (diff) | |
Correction of a bug in Intuition (no more decomposition of dependent pairs).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2704 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hipattern.mli')
| -rw-r--r-- | tactics/hipattern.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 02ba943501..053175269c 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -73,3 +73,16 @@ val is_equation : testing_function val match_with_nottype : (constr * constr) matching_function val is_nottype : testing_function + + +(* I added these functions to test whether a type contains dependent + products or not, and if an inductive has constructors with dependent types + (excluding parameters). this is useful to check whether a conjunction is a + real conjunction and not a dependent tuple. (Pierre Corbineau, 13/5/2002) *) + +val has_nodep_prod_after : int -> testing_function +val has_nodep_prod : testing_function + +val match_with_nodep_ind : (constr * constr list) matching_function +val is_nodep_ind : testing_function + |