correction of bug #2002

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

2 files changed, 69 insertions, 22 deletions

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 1607647991..b03bdf31af 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -552,13 +552,31 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
       | _ -> anomaly ""
   in
   let (_,(const,_,_)) = 
-    build_functional_principle false
-      first_type
-      (Array.of_list sorts)
-      this_block_funs
-      0
-      (prove_princ_for_struct false 0 (Array.of_list funs))
-      (fun _ _ _ -> ())
+    try
+      build_functional_principle false
+	first_type
+	(Array.of_list sorts)
+	this_block_funs
+	0
+	(prove_princ_for_struct false 0 (Array.of_list funs))
+	(fun _ _ _ -> ())
+  with e -> 
+    begin
+      begin 
+	try 
+	  let id = Pfedit.get_current_proof_name () in 
+	  let s = string_of_id id in 
+	  let n = String.length "___________princ_________" in
+	  if String.length s >= n 
+	  then if String.sub s 0 n = "___________princ_________" 
+	  then Pfedit.delete_current_proof ()
+	  else ()
+	  else ()
+	with _ -> ()
+      end;
+      raise (Defining_principle e)
+    end
+
   in      
   incr i;
   let opacity = 
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index 020d67f0c5..a8ad2498d7 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*i camlp4deps: "parsing/grammar.cma" i*)
+open Util
 open Term
 open Names
 open Pp
@@ -201,24 +202,52 @@ VERNAC ARGUMENT EXTEND fun_scheme_args
 | [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas]
 END 
 
+
+let warning_error names e = 
+  match e with 
+    | Building_graph e -> 
+	Pp.msg_warning 
+	  (str "Cannot define graph(s) for " ++ 
+	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
+	     if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+    | Defining_principle e -> 
+	Pp.msg_warning
+	  (str "Cannot define principle(s) for "++ 
+	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
+	     if do_observe () then Cerrors.explain_exn e else mt ())
+    | _ -> anomaly ""
+
+
 VERNAC COMMAND EXTEND NewFunctionalScheme
    ["Functional" "Scheme" fun_scheme_args(fas) ] ->
     [
-      try 
-	Functional_principles_types.build_scheme fas
-      with Functional_principles_types.No_graph_found -> 
-	match fas with 
-	  | (_,fun_name,_)::_ -> 
-	      begin
-		begin
-		    make_graph (Nametab.global fun_name)
-		end
-		;
-		try Functional_principles_types.build_scheme fas
-		with Functional_principles_types.No_graph_found -> 
-		  Util.error ("Cannot generate induction principle(s)")
-	      end
-	  | _ -> assert false (* we can only have non empty  list *)
+      begin
+	try 
+	  Functional_principles_types.build_scheme fas
+	with Functional_principles_types.No_graph_found -> 
+	  begin
+	    match fas with 
+	      | (_,fun_name,_)::_ -> 
+		  begin
+		    begin
+		      make_graph (Nametab.global fun_name)
+		    end
+		    ;
+		    try Functional_principles_types.build_scheme fas
+		    with Functional_principles_types.No_graph_found -> 
+		      Util.error ("Cannot generate induction principle(s)")
+    		      | e -> 
+			  let names = List.map (fun (_,na,_) -> na) fas in 
+			  warning_error names e
+			    
+		  end
+	      | _ -> assert false (* we can only have non empty  list *)
+	  end
+    	  | e -> 
+	      let names = List.map (fun (_,na,_) -> na) fas in 
+	      warning_error names e
+
+      end
     ]
 END
 (***** debug only ***)