diff options
author | 2004-04-17 08:05:56 +0000 | |
---|---|---|
committer | 2004-04-17 08:05:56 +0000 | |
commit | 715e002ab56561fc3ecd5fc922459a9e9a8001b0 (patch) | |
tree | efb7a855ddbae5ba15553f41633f6b0e8f2a305b /interp/constrintern.ml | |
parent | 10ef3e09d2f602ac039684e8ee121dc908137a3a (diff) |
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
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r-- | interp/constrintern.ml | 18 |
1 files changed, 16 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 |