pb facto des Fixpoint + erreur avec -dump-glob et Load

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 21 insertions, 2 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8a16a56db..8ac87a4d4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -123,6 +123,22 @@ let error_bad_inductive_type loc =
 
 (**********************************************************************)
 (* Dump of globalization (to be used by coqdoc)                       *)
+let token_number = ref 0
+let last_pos = ref 0
+
+type coqdoc_state = Lexer.location_table * int * int
+
+let coqdoc_freeze () =
+  let lt = Lexer.location_table() in
+  let state = (lt,!token_number,!last_pos) in
+  token_number := 0;
+  last_pos := 0;
+  state
+
+let coqdoc_unfreeze (lt,tn,lp) =
+  Lexer.restore_location_table lt;
+  token_number := tn;
+  last_pos := lp
 
 let add_glob loc ref = 
 (*i
@@ -148,8 +164,6 @@ let ntn_loc = loc_of_notation constr_loc
 let patntn_loc = loc_of_notation cases_pattern_loc
 
 let dump_notation_location =
-  let token_number = ref 0 in
-  let last_pos = ref 0 in
   fun pos ntn ((path,df),sc) ->
     let rec next growing =
       let (bp,_ as loc) = Lexer.location_function !token_number in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 91a345476..aac3f44c3 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -116,6 +116,11 @@ val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
 
+(* Coqdoc utility functions *)
+type coqdoc_state
+val coqdoc_freeze : unit -> coqdoc_state
+val coqdoc_unfreeze : coqdoc_state -> unit
+
 (* For v8 translation *)
 val set_temporary_implicits_in :
   (identifier * Impargs.implicits_list) list -> unit