From 31dbba5f5c16f81c6dac2adaba46087da787ac12 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sun, 25 Nov 2012 17:39:18 +0000 Subject: Monomorphization (tactics) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16003 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/autorewrite.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e1a4d4f36..bad5a6aa0 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -137,7 +137,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic = g::_ -> (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with (lastid,_,_)::_ -> - if last_hyp_id <> lastid then + if not (id_eq last_hyp_id lastid) then begin let gl'' = if !to_be_cleared then @@ -167,8 +167,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = let try_do_hyps treat_id l = autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas in - if cl.concl_occs <> AllOccurrences & - cl.concl_occs <> NoOccurrences + if cl.concl_occs != AllOccurrences && + cl.concl_occs != NoOccurrences then error "The \"at\" syntax isn't available yet for the autorewrite tactic." else @@ -178,7 +178,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = | _ -> tclTHENFIRST t1 t2 in compose_tac - (if cl.concl_occs <> NoOccurrences then autorewrite ~conds tac_main lbas else tclIDTAC) + (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else tclIDTAC) (match cl.onhyps with | Some l -> try_do_hyps (fun ((_,id),_) -> id) l | None -> @@ -191,7 +191,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds Refiner.tclIDTAC let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl = - let onconcl = cl.Locus.concl_occs <> NoOccurrences in + let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in match onconcl,cl.Locus.onhyps with | false,Some [_] | true,Some [] | false,Some [] -> (* autorewrite with .... in clause using tac n'est sur que -- cgit v1.2.3