diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/functional_principles_types.ml | 10 | ||||
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 2 |
2 files changed, 4 insertions, 8 deletions
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index ec98e0df98..89ebb75a96 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 5f2ba15782..7404722370 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -1140,7 +1140,7 @@ let (com_eqn : identifier -> ) ) ); - defined (); + Options.silently defined (); );; |