Fix 0 obligations bug

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

3 files changed, 28 insertions, 18 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index d664fe5c29..6725edecaa 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -552,7 +552,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 			 (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
 	    lnameargsardef
 	in
-	  build_mutrec lnameargsardef boxed;
-	  assert(false)
+	  build_mutrec lnameargsardef boxed
+	  
       
       
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 64a29ff2f6..bc4f4cab4d 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -54,21 +54,6 @@ let _ =
         (fun () -> from_prg := ProgMap.empty);
       Summary.survive_module = false;
       Summary.survive_section = false }
-    
-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) = 
-  let cache_th (name,th) = add_entry name th
-  and export_th x = Some x in
-  declare_object
-    {(default_object "program-tcc") with
-      open_function = (fun i o -> if i=1 then cache_th o);
-      cache_function = cache_th;
-      subst_function = (fun _ -> assert(false));
-      classify_function = (fun (_,x) -> Dispose);
-      export_function = export_th }
 
 let declare_definition prg = 
   let obls_constrs = 
@@ -84,6 +69,31 @@ let declare_definition prg =
     prg.prg_name (DefinitionEntry ce,IsDefinition Definition)
   in
     Subtac_utils.definition_message prg.prg_name
+    
+let add_entry n e =
+  Options.if_verbose pp (str (string_of_id e.prg_name) ++ str " has type-checked");
+  let nobls = snd e.prg_obligations in
+    match nobls with
+	0 -> Options.if_verbose ppnl (str ".");
+	  declare_definition e
+      | 1 -> 
+	  Options.if_verbose ppnl (str ", generating one obligation");
+	  from_prg := ProgMap.add e.prg_name e !from_prg
+      | n -> 
+	  Options.if_verbose ppnl (str ", generating " ++ int n ++ str " obligations");
+	  from_prg := ProgMap.add e.prg_name e !from_prg
+	        
+let (theory_to_obj, obj_to_theory) = 
+  let cache_th (name,th) = add_entry name th
+  and export_th x = Some x in
+  declare_object
+    {(default_object "program-tcc") with
+      open_function = (fun i o -> if i=1 then cache_th o);
+      cache_function = cache_th;
+      subst_function = (fun _ -> assert(false));
+      classify_function = (fun (_,x) -> Dispose);
+      export_function = export_th }
+
 
 let error s = Util.error s
 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 672c86e905..5fbbbc2be1 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -89,7 +89,7 @@ let my_print_tycon_type = Evarutil.pr_tycon_type
 
 let debug_level = 2
 
-let debug_on = false
+let debug_on = true
 
 let debug n s = 
   if debug_on then