diff options
| author | courant | 2001-09-13 07:37:16 +0000 |
|---|---|---|
| committer | courant | 2001-09-13 07:37:16 +0000 |
| commit | 8b3cceaf9356ddbb214e91371f01394663ff0375 (patch) | |
| tree | 3aef2c64203d510b424a9d4762ecd369b0a4ef73 | |
| parent | 13e17eac2e476114305472e581a433d8c08d48d6 (diff) | |
eclaircissement du code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1957 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/hipattern.ml | 4 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 2a2b46cba8..ae2ed421f6 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -107,8 +107,8 @@ let match_with_unit_type t = | IsMutInd ind -> let constr_types = Global.mind_nf_lc ind in let nconstr = Global.mind_nconstr ind in - let zero_args c = ((nb_prod c) - (Global.mind_nparams ind)) = 0 in - if nconstr = 1 && (array_for_all zero_args constr_types) then + let zero_args c = nb_prod c = Global.mind_nparams ind in + if nconstr = 1 && array_for_all zero_args constr_types then Some hdapp else None diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index f1a758d8ba..02ba943501 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 |