From 404758609f2097712a81fbd4acf4a35128504b03 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Sun, 3 Nov 2013 20:53:51 +0000
Subject: Fixup bug 3145

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17043 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0a2f9c3c39..095bf5300f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -926,7 +926,7 @@ let do_program_recursive local fixkind fixl ntns =
   in
   let (fixnames,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
-  let fixdefs = List.map Option.get fixdefs in
+  let fixdefs = List.map out_def fixdefs in
   let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
   let () = if isfix then begin
       let possible_indexes = List.map compute_possible_guardness_evidences info in
-- 
cgit v1.2.3