* kernel/Safe_typing.LightenLibrary:

  Fix an incorrect initialization of the index counter.

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

1 files changed, 6 insertions, 6 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 51850eaab..222714217 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -905,7 +905,7 @@ end = struct
     let ((insert    : constr_substituted -> constr_substituted), 
 	 (get_table : unit -> table)) = 
       (* We use an integer as a key inside the table. *)
-      let counter = ref 0 in
+      let counter = ref (-1) in
       (* ... but it is wrapped inside a [constr_substituted]. *)
       let key_as_constr key = Declarations.from_val (Term.mkRel key) in
 
@@ -940,11 +940,11 @@ end = struct
       if load_proof then 
 	let table = get_table () in
 	function Some cterm -> 
-	  Some (table.(
-	    try 
-	      Term.destRel (Declarations.force cterm)
-	    with _ -> assert false
-	  ))
+	  Some (try 
+		  table.(Term.destRel (Declarations.force cterm))
+	    with _ -> 
+	      assert false
+	  )
 	  | _ -> None
       else 
 	fun _ -> None