aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hipattern.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-10-11 17:27:20 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-10-11 17:27:20 +0000
commit301a70e45eac43f034077c95bce04edbcf2ab4ad (patch)
treed61c92f0d7a46203618a4610301c64d65c9c03ad /tactics/hipattern.ml
parent1d5b3f16e202af2874181671abd86a47fca37cd7 (diff)
Suppression option immediate_discharge; nettoyage de Declare et conséquences
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hipattern.ml')
-rw-r--r--tactics/hipattern.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index ae2ed421f..a3bdf52b9 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -119,9 +119,9 @@ let is_unit_type t = op2bool (match_with_unit_type t)
(* Checks if a given term is an application of an
inductive binary relation R, so that R has only one constructor
- stablishing its reflexivity. *)
+ establishing its reflexivity. *)
-let match_with_equation t =
+let match_with_equation t =
let (hdapp,args) = decomp_app t in
match (kind_of_term hdapp) with
| IsMutInd ind ->