Message modification in Function

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

2 files changed, 4 insertions, 8 deletions

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index ec98e0df9..89ebb75a9 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -394,6 +394,9 @@ let generate_functional_principle
 	     Decl_kinds.IsDefinition (Decl_kinds.Scheme)
 	    )
 	);
+	Options.if_verbose 
+	  (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) 
+	  name;
 	names := name :: !names
       in
       register_with_sort InProp;
@@ -605,13 +608,6 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
     const::other_result
 
 let build_scheme fas = 
-(*         (fun (f,_) ->  *)
-(* 	 try Libnames.constr_of_global (Nametab.global f) *)
-(* 	 with Not_found ->  *)
-(* 	   Util.error ("Cannot find "^ Libnames.string_of_reference f) *)
-(*       ) *)
-(*       fas *)
-
   let bodies_types = 
     make_scheme 
       (List.map 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 5f2ba1578..740472237 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1140,7 +1140,7 @@ let (com_eqn : identifier ->
 	       )
 	  )
        );
-     defined (); 
+     Options.silently defined (); 
     );;