From 99e196294f3de42f5f7285cbc7fa40f8171026a6 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Tue, 6 Oct 2009 16:56:03 +0000
Subject: Relaxed error severity when encountering unknown library objects or
 tactic extensions. This makes it possible to load .vo compiled with a
 nonstandard toplevel, e.g. ssreflect, which defines new tactics and new hint
 databases.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12375 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 770b4a0e60..a7d0413230 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -281,7 +281,13 @@ let add_interp_genarg id f =
   extragenargtab := Gmap.add id f !extragenargtab
 let lookup_genarg id =
   try Gmap.find id !extragenargtab
-  with Not_found -> failwith ("No interpretation function found for entry "^id)
+  with Not_found ->
+    let msg = "No interpretation function found for entry " ^ id in
+    warning msg;
+    let f = (fun _ _ -> failwith msg), (fun _ _ _ -> failwith msg), (fun _ a -> a) in
+    add_interp_genarg id f;
+    f
+
 
 let lookup_genarg_glob   id = let (f,_,_) = lookup_genarg id in f
 let lookup_interp_genarg id = let (_,f,_) = lookup_genarg id in f
-- 
cgit v1.2.3