diff options
| author |  courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-13 07:37:16 +0000 |
|---|---|---|
| committer | courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-13 07:37:16 +0000 |
| commit | 8b3cceaf9356ddbb214e91371f01394663ff0375 (patch) | |
| tree | 3aef2c64203d510b424a9d4762ecd369b0a4ef73 /tactics/hipattern.mli | |
| parent | 13e17eac2e476114305472e581a433d8c08d48d6 (diff) | |
eclaircissement du code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hipattern.mli')
| -rw-r--r-- | tactics/hipattern.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index f1a758d8b..02ba94350 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -64,6 +64,8 @@ val match_with_empty_type : constr matching_function val is_empty_type : testing_function val match_with_unit_type : constr matching_function + +(* type with only one constructor and no arguments *) val is_unit_type : testing_function val match_with_equation : (constr * constr list) matching_function |