diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-22 15:12:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-22 15:12:28 +0100 |
| commit | 714256f7dcc68642117013dfa7b3ff8a76e468b9 (patch) | |
| tree | 3396501cd0f349d78ac9f2a728f48ef692ae9743 /proofs/logic.ml | |
| parent | 34921bb2391e8ce8b0fa00c300d218d2ef6f27e2 (diff) | |
Removing useless flag of the historical move tactic.
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index b7a33cdba..4b97c1d3f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -233,7 +233,7 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = +let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto = let env = Global.env() in let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) = if toleft @@ -250,7 +250,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = | (hyp,_,_) as d :: right -> let (first',middle') = if List.exists (test_dep d) middle then - if with_dep && not (move_location_eq hto (MoveAfter hyp)) then + if not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++ @@ -529,7 +529,7 @@ let prim_refiner r sigma goal = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp true false ([],(id,None,t),named_context_of_val sign) + move_hyp false ([],(id,None,t),named_context_of_val sign) nexthyp, t,cl,sigma else @@ -645,11 +645,11 @@ let prim_refiner r sigma goal = let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) - | Move (withdep, hfrom, hto) -> + | Move (hfrom, hto) -> let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in let hyps' = - move_hyp withdep toleft (left,declfrom,right) hto in + move_hyp toleft (left,declfrom,right) hto in let (gl,ev,sigma) = mk_goal hyps' cl in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) |