Merge PR #11889: Fix a spelling mistake in the code: s/magicaly/magically/

1 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8822cc2338..8bb268a92e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -715,7 +715,7 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
     f x := t. End M. Definition f := u. and say goodbye to any hope
     of refolding M.f this way ...
 *)
-let magicaly_constant_of_fixbody env sigma reference bd = function
+let magically_constant_of_fixbody env sigma reference bd = function
   | Name.Anonymous -> bd
   | Name.Name id ->
     let open UnivProblem in
@@ -757,7 +757,7 @@ let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbo
       | Some e ->
         match reference with
         | None -> bd
-        | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+        | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
   let closure = List.init nbodies make_Fi in
   substl closure bodies.(bodynum)
 
@@ -799,7 +799,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
         | Some e ->
           match reference with
           | None -> bd
-          | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+          | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
     let closure = List.init nbodies make_Fi in
     substl closure bodies.(bodynum)