diff options
| -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 |