diff options
| -rw-r--r-- | pretyping/reductionops.ml | 6 |
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) |