New version of recdef :

 + Allowing much more function to be defined.
 + Using completely new algorithm to define non structural fixpoints

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

1 files changed, 17 insertions, 10 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4546ff08d..97a49d6f0 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -262,20 +262,27 @@ let warning_error names e =
   let e = Cerrors.process_vernac_interp_error e in
   let e_explain e =
     match e with
-      | ToShow e -> spc () ++ Errors.print e
-      | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
+      | ToShow e -> 
+	let e = Cerrors.process_vernac_interp_error e in
+	spc () ++ Errors.print e
+      | _ -> 
+	if do_observe () 
+	then 
+	  let e = Cerrors.process_vernac_interp_error e in 
+	  (spc () ++ Errors.print e) 
+	else mt ()
   in
   match e with
     | Building_graph e ->
-	Pp.msg_warning
-	  (str "Cannot define graph(s) for " ++
-	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	     e_explain e)
+      Pp.msg_warning
+	(str "Cannot define graph(s) for " ++
+	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	   e_explain e)
     | Defining_principle e ->
-	Pp.msg_warning
-	  (str "Cannot define principle(s) for "++
-	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	     e_explain e)
+      Pp.msg_warning
+	(str "Cannot define principle(s) for "++
+	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	   e_explain e)
     | _ -> raise e
 
 let error_error names e =