Fix wrong order for building library, add informative messages.

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

2 files changed, 9 insertions, 8 deletions

diff --git a/Makefile b/Makefile
index ed029f4eb3..385d8322e4 100644
--- a/Makefile
+++ b/Makefile
@@ -295,8 +295,9 @@ CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \
 SUBTACCMO=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \
   contrib/subtac/g_eterm.cmo contrib/subtac/context.cmo \
   contrib/subtac/subtac_errors.cmo contrib/subtac/subtac_coercion.cmo \
+  contrib/subtac/subtac_obligations.cmo \
   contrib/subtac/subtac_pretyping_F.cmo contrib/subtac/subtac_pretyping.cmo \
-  contrib/subtac/subtac_interp_fixpoint.cmo contrib/subtac/subtac_obligations.cmo \
+  contrib/subtac/subtac_interp_fixpoint.cmo \
   contrib/subtac/subtac_command.cmo contrib/subtac/subtac.cmo \
   contrib/subtac/g_subtac.cmo
 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index ede7537114..64a29ff2f6 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -42,10 +42,6 @@ let map_first m =
     ProgMap.iter (fun _ v -> raise (Found v)) m;
     assert(false)
   with Found x -> x
-      
-let map_single m = 
-  if map_cardinal m = 1 then map_first m
-  else raise (Invalid_argument "map_single") 
     
 let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 
@@ -59,7 +55,8 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section = false }
     
-let add_entry _ e =
+let add_entry n e =
+  ppnl (str (string_of_id e.prg_name) ++ str " has type-checked, generating " ++ int (snd e.prg_obligations) ++ str " obligation(s)");
   from_prg := ProgMap.add e.prg_name e !from_prg
     
 let (theory_to_obj, obj_to_theory) = 
@@ -97,8 +94,11 @@ let subtac_obligation (user_num, name) =
     match name with
 	Some n -> ProgMap.find n prg_infos
       | None -> 
-	  (try map_single prg_infos 
-	   with _ -> error "More than one program with unsolved obligations")
+	  (let n = map_cardinal prg_infos in
+	     match n with 
+		 0 -> error "No obligations remaining"
+	       | 1 -> map_first prg_infos
+	       | _ -> error "More than one program with unsolved obligations")
   in
   let obls, rem = prg.prg_obligations in
     if num < Array.length obls then