diff options
| -rw-r--r-- | pretyping/reductionops.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 69f2ba2d00..f545d29518 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -699,7 +699,10 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies)) let bd = mkCoFix (ind,typedbodies) in match env with | None -> bd - | Some e -> magicaly_constant_of_fixbody e (Option.get reference) bd names.(ind) in + | Some e -> + match reference with + | None -> bd + | Some r -> magicaly_constant_of_fixbody e r bd names.(ind) in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -733,7 +736,10 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty let bd = mkFix ((recindices,ind),typedbodies) in match env with | None -> bd - | Some e -> magicaly_constant_of_fixbody e (Option.get reference) bd names.(ind) in + | Some e -> + match reference with + | None -> bd + | Some r -> magicaly_constant_of_fixbody e r bd names.(ind) in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) |