diff options
| -rw-r--r-- | printing/printer.ml | 5 | ||||
| -rw-r--r-- | proofs/logic.ml | 10 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 6 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
7 files changed, 14 insertions, 15 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 8a906b3f1..cda0403d9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -696,9 +696,8 @@ let pr_prim_rule = function | Thin ids -> (str"clear " ++ pr_sequence pr_id ids) - | Move (withdep,id1,id2) -> - (str (if withdep then "dependent " else "") ++ - str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) + | Move (id1,id2) -> + (str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) (* Backwards compatibility *) 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) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 613f85a73..bc3b1596b 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -32,7 +32,7 @@ type prim_rule = | Cofix of Id.t * (Id.t * constr) list * int | Refine of constr | Thin of Id.t list - | Move of bool * Id.t * Id.t move_location + | Move of Id.t * Id.t move_location (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 9361d48e6..dcfd4b8c1 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -24,7 +24,7 @@ type prim_rule = | Cofix of Id.t * (Id.t * constr) list * int | Refine of constr | Thin of Id.t list - | Move of bool * Id.t * Id.t move_location + | Move of Id.t * Id.t move_location (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 03f2fd2b4..fe648e765 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -118,8 +118,8 @@ let refine_no_check c gl = let thin_no_check ids gl = if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl -let move_hyp_no_check with_dep id1 id2 gl = - refiner (Move (with_dep,id1,id2)) gl +let move_hyp_no_check id1 id2 gl = + refiner (Move (id1,id2)) gl let mutual_fix f n others j gl = with_check (refiner (FixRule (f,n,others,j))) gl @@ -133,7 +133,7 @@ let internal_cut b d t = with_check (internal_cut_no_check b d t) let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) let thin c = with_check (thin_no_check c) -let move_hyp b id id' = with_check (move_hyp_no_check b id id') +let move_hyp id id' = with_check (move_hyp_no_check id id') (* Pretty-printers *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 8b95ae427..c82d1017b 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -97,7 +97,7 @@ val internal_cut : bool -> Id.t -> types -> tactic val internal_cut_rev : bool -> Id.t -> types -> tactic val refine : constr -> tactic val thin : Id.t list -> tactic -val move_hyp : bool -> Id.t -> Id.t move_location -> tactic +val move_hyp : Id.t -> Id.t move_location -> tactic (** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.std_ppcmds diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e4783707a..1ecd27935 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -254,7 +254,7 @@ let apply_clear_request clear_flag dft c = else Tacticals.New.tclIDTAC (* Moving hypotheses *) -let move_hyp id dest gl = Tacmach.move_hyp true id dest gl +let move_hyp id dest gl = Tacmach.move_hyp id dest gl (* Renaming hypotheses *) let rename_hyp repl = |