diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-01 15:16:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-01 15:16:57 +0000 |
| commit | 2f0c35cfcbab959bad20f436849c74ec63910f51 (patch) | |
| tree | be017201340ec2f43e9d126ac6e63bdbe428fe93 /tactics/hipattern.ml | |
| parent | 5efbe2d6be224aea70bf570b7ee26d80d79bc54f (diff) | |
Renommage AppL en App
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index d9d81238b..1f78dcb85 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -96,7 +96,7 @@ let op2bool = function Some _ -> true | None -> false let match_with_non_recursive_type t = match kind_of_term t with - | IsAppL _ -> + | IsApp _ -> let (hdapp,args) = decomp_app t in (match kind_of_term hdapp with | IsMutInd ind -> |