Tentative fix for a badly used Option.get in Reductionops.

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)