From 6fd41fb09f6d809e831f2d5904f4c4b4ff2aa253 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 17 Jun 2009 16:32:45 +0000
Subject: Fallback on not using [fix_proto] if the right imports aren't there,
 the tactics that use it won't be in scope either.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12193 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_command.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index a408d44ca4..eb135139c4 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -404,7 +404,10 @@ let interp_recursive fixkind l boxed =
   let rec_sign = 
     List.fold_left2 (fun env' id t ->
       let sort = Retyping.get_type_of env !evdref t in
-      let fixprot = mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|]) in
+      let fixprot = 
+	try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|]) 
+	with e -> t
+      in
 	(id,None,fixprot) :: env')
       [] fixnames fixtypes
   in
-- 
cgit v1.2.3