From 8b3cceaf9356ddbb214e91371f01394663ff0375 Mon Sep 17 00:00:00 2001
From: courant
Date: Thu, 13 Sep 2001 07:37:16 +0000
Subject: eclaircissement du code

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1957 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/hipattern.ml  | 4 ++--
 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
-- 
cgit v1.2.3