Merge branch 'v8.5'

4 files changed, 10 insertions, 10 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9c041d72c3..d024c01ba5 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -42,7 +42,7 @@ let cook_this_proof p =
 
 let cook_proof () =
   cook_this_proof (fst
-    (Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)))
+    (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
 let get_pftreestate () =
   Proof_global.give_me_the_proof ()
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8677b854de..c02b909164 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -269,7 +269,7 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
-let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
+let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
@@ -290,7 +290,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
         let body = c and typ = nf t in
         let used_univs_body = Universes.universes_of_constr body in
         let used_univs_typ = Universes.universes_of_constr typ in
-        if keep_body_ucst_sepatate then
+        if keep_body_ucst_separate then
           let initunivs = Evd.evar_context_universe_context initial_euctx in
           let ctx = Evd.evar_universe_context_set initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
@@ -379,9 +379,9 @@ let return_proof ?(allow_partial=false) () =
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
-  close_proof ~keep_body_ucst_sepatate:true ~feedback_id ~now:false proof
-let close_proof ~keep_body_ucst_sepatate fix_exn =
-  close_proof ~keep_body_ucst_sepatate ~now:true
+  close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof
+let close_proof ~keep_body_ucst_separate fix_exn =
+  close_proof ~keep_body_ucst_separate ~now:true
     (Future.from_val ~fix_exn (return_proof ()))
 
 (** Gets the current terminator without checking that the proof has
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 88e047782c..b5dd5ef85f 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -91,7 +91,7 @@ val start_dependent_proof :
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof
+val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The formes is supposed to be
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 64ea5aea01..11b7d07d05 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -648,7 +648,7 @@ let goodmod p m =
 
 let cycle n =
   let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle"++spc()++int n))) >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let n' = goodmod n l in
@@ -658,7 +658,7 @@ let cycle n =
 
 let swap i j =
   let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"swap"++spc()++int i++spc()++int j))) >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
@@ -1057,7 +1057,7 @@ struct
     let comb = undefined sigma (CList.rev evs) in
     let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
     let open Proof in
-    InfoL.leaf (Info.Tactic (fun () -> Pp.(str"refine"++spc()++ Hook.get pr_constrv env sigma c))) >>
+    InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
     Pv.set { solution = sigma; comb; }
   end