Merge branch 'v8.6'

5 files changed, 8 insertions, 15 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5aba6b614f..d23a4ad61b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -278,6 +278,11 @@ let move_hyp toleft (left,declfrom,right) hto =
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
+let move_hyp_in_named_context hfrom hto sign =
+  let (left,right,declfrom,toleft) =
+    split_sign hfrom hto (named_context_of_val sign) in
+  move_hyp toleft (left,declfrom,right) hto
+
 (**********************************************************************)
 
 
@@ -552,12 +557,3 @@ let prim_refiner r sigma goal =
 	let sgl = List.rev sgl in
 	let sigma = Goal.V82.partial_solution sigma goal oterm in
 	  (sgl, sigma)
-
-    | Move (hfrom, hto) ->
-  	let (left,right,declfrom,toleft) =
-	  split_sign hfrom hto (named_context_of_val sign) in
-  	let hyps' =
-	  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/logic.mli b/proofs/logic.mli
index 2764d28c02..0dba9ef1ee 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -56,3 +56,6 @@ val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   Context.Named.Declaration.t -> Environ.named_context_val
+
+val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location ->
+  Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index ff60ae5bf7..03bc5e4710 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -21,7 +21,6 @@ open Misctypes
 type prim_rule =
   | Cut of bool * bool * Id.t * types
   | Refine of constr
-  | 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 93e276f4ba..904e226814 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -123,15 +123,11 @@ let internal_cut_rev_no_check replace id t gl =
 let refine_no_check c gl =
   refiner (Refine c) gl
 
-let move_hyp_no_check id1 id2 gl =
-  refiner (Move (id1,id2)) gl
-
 (* Versions with consistency checks *)
 
 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 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 100ed1522e..727efcf6dc 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -92,7 +92,6 @@ val refine_no_check           : constr -> tactic
 val internal_cut     : bool -> Id.t -> types -> tactic
 val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> 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