summaryrefslogtreecommitdiff
path: root/tactics/dhyp.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /tactics/dhyp.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'tactics/dhyp.ml')
-rw-r--r--tactics/dhyp.ml12
1 files changed, 7 insertions, 5 deletions
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index f82b1f82..5dd7f5fd 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: dhyp.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: dhyp.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
(* Chet's comments about this tactic :
@@ -261,11 +261,13 @@ let add_destructor_hint local na loc pat pri code =
(inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code }))
let match_dpat dp cls gls =
+ let onconcl = cls.concl_occs <> no_occurrences_expr in
match (cls,dp) with
- | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) ->
+ | ({onhyps=lo},HypLocation(_,hypd,concld)) when not onconcl ->
let hl = match lo with
Some l -> l
- | None -> List.map (fun id -> (([],id),InHyp)) (pf_ids_of_hyps gls) in
+ | None -> List.map (fun id -> ((all_occurrences_expr,id),InHyp))
+ (pf_ids_of_hyps gls) in
if not
(List.for_all
(fun ((_,id),hl) ->
@@ -278,7 +280,7 @@ let match_dpat dp cls gls =
(is_matching concld.d_sort (pf_type_of gls cl)))
hl)
then error "No match"
- | ({onhyps=Some[];onconcl=true},ConclLocation concld) ->
+ | ({onhyps=Some[]},ConclLocation concld) when onconcl ->
let cl = pf_concl gls in
if not
((is_matching concld.d_typ cl) &
@@ -300,7 +302,7 @@ let applyDestructor cls discard dd gls =
| Some ((_,id),_), (Some x, tac) ->
let arg =
ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in
- TacLetIn ([(dummy_loc, x), None, arg], tac)
+ TacLetIn (false, [(dummy_loc, x), arg], tac)
| None, (None, tac) -> tac
| _, (Some _,_) -> error "Destructor expects an hypothesis"
| _, (None,_) -> error "Destructor is for conclusion")