Réinitialisation de token_number à chaque compilation d'un nouveau fichier (fixe le bug #914)

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

1 files changed, 26 insertions, 26 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 805ffba42..57b5762d7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -129,9 +129,9 @@ 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
+    token_number := 0;
+    last_pos := 0;
+    state
 
 let coqdoc_unfreeze (lt,tn,lp) =
   Lexer.restore_location_table lt;
@@ -145,7 +145,7 @@ let add_glob loc ref =
   let mod_dp_trunc =  drop_dirpath_prefix lib_dp mod_dp in
   let filepath = string_of_dirpath lib_dp in
   let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in
-  dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname)
+    dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname)
 
 let loc_of_notation f loc args ntn =
   if args=[] or ntn.[0] <> '_' then fst (unloc loc)
@@ -158,15 +158,15 @@ let dump_notation_location pos ((path,df),sc) =
   let rec next growing =
     let loc = Lexer.location_function !token_number in
     let (bp,_) = unloc loc in
-    if growing then if bp >= pos then loc else (incr token_number;next true)
-    else if bp = pos then loc
-    else if bp > pos then (decr token_number;next false)
-    else (incr token_number;next true) in
+      if growing then if bp >= pos then loc else (incr token_number;next true)
+      else if bp = pos then loc
+      else if bp > pos then (decr token_number;next false)
+      else (incr token_number;next true) in
   let loc = next (pos >= !last_pos) in
-  last_pos := pos;
-  let path = string_of_dirpath path in
-  let sc = match sc with Some sc -> " "^sc | None -> "" in
-  dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
+    last_pos := pos;
+    let path = string_of_dirpath path in
+    let sc = match sc with Some sc -> " "^sc | None -> "" in
+      dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
@@ -494,20 +494,20 @@ let find_constructor ref =
     try extended_locate qid
     with Not_found ->
       raise (InternalisationError (loc,NotAConstructor ref)) in
-  match gref with
-    | SyntacticDef sp ->
-        let sdef = Syntax_def.search_syntactic_definition loc sp in
-        patt_of_rawterm loc sdef
-    | TrueGlobal r ->
-        let rec unf = function
-          | ConstRef cst ->
-	      let v = Environ.constant_value (Global.env()) cst in
-              unf (global_of_constr v)
-          | ConstructRef c -> 
-	      if !dump then add_glob loc r; 
-	      c, []
-          | _ -> raise Not_found
-        in unf r
+    match gref with
+      | SyntacticDef sp ->
+          let sdef = Syntax_def.search_syntactic_definition loc sp in
+            patt_of_rawterm loc sdef
+      | TrueGlobal r ->
+          let rec unf = function
+            | ConstRef cst ->
+		let v = Environ.constant_value (Global.env()) cst in
+		  unf (global_of_constr v)
+            | ConstructRef c -> 
+		if !dump then add_glob loc r; 
+		c, []
+            | _ -> raise Not_found
+          in unf r
 
 let find_pattern_variable = function
   | Ident (loc,id) -> id