From 625a129d5e9b200399a147111f191abe84282aa4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 6 Nov 2009 03:01:57 +0000
Subject: Misc fixes. - Correct backtracking function of coqdoc to handle the
 _p fields of lexers - Try a better typesetting of [[ ]] inline code
 considering it as blocks and not purely inline code like [ ] escapings. -
 Rework latex macros for better factorization and support external references
 in pdf output. - Better criterion for generalization of variables in
 dependent elimination tactic and better error message in
 [specialize_hypothesis]. - In autounfold, don't put the core unfolds by
 default.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/implicit_quantifiers.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 93f4eedff2..dc2f8ad0aa 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -55,9 +55,13 @@ let add_generalizable gen table =
 
 let cache_generalizable_type (_,(local,cmd)) =
   generalizable_table := add_generalizable cmd !generalizable_table
+
+let load_generalizable_type _ (_,(local,cmd)) =
+  generalizable_table := add_generalizable cmd !generalizable_table
     
 let (in_generalizable, _) =
   declare_object {(default_object "GENERALIZED-IDENT") with
+    load_function = load_generalizable_type;
     cache_function = cache_generalizable_type;
     classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
   }
-- 
cgit v1.2.3