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

1 files changed, 4 insertions, 0 deletions

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)
   }