From 7e8b7bc5fd911d2fb34eecd238788fc2e81afa0f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 12 Oct 2014 16:51:05 +0200
Subject: Tentative fix for a badly used Option.get in Reductionops.

---
 pretyping/reductionops.ml | 10 ++++++++--
 1 file 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)
 
-- 
cgit v1.2.3