diff options
Diffstat (limited to 'contrib/funind/functional_principles_types.ml')
| -rw-r--r-- | contrib/funind/functional_principles_types.ml | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index 8ad2e72b..16076479 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -115,7 +115,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = it_mkProd_or_LetIn ~init: (it_mkProd_or_LetIn - ~init:(option_fold_right + ~init:(Option.fold_right mkProd_or_LetIn princ_type_info.indarg princ_type_info.concl @@ -384,7 +384,7 @@ let generate_functional_principle { const_entry_body = value; const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() + const_entry_boxed = Flags.boxed_definitions() } in ignore( @@ -394,7 +394,7 @@ let generate_functional_principle Decl_kinds.IsDefinition (Decl_kinds.Scheme) ) ); - Options.if_verbose + Flags.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) name; names := name :: !names @@ -561,6 +561,15 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent (fun _ _ _ -> ()) in incr i; + let opacity = + let finfos = find_Function_infos this_block_funs.(0) in + try + let equation = Option.get finfos.equation_lemma in + (Global.lookup_constant equation).Declarations.const_opaque + with Option.IsNone -> (* non recursive definition *) + false + in + let const = {const with const_entry_opaque = opacity } in (* The others are just deduced *) if other_princ_types = [] then @@ -642,10 +651,12 @@ let build_scheme fas = in List.iter2 (fun (princ_id,_,_) def_entry -> - ignore (Declare.declare_constant - princ_id - (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); - Options.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id + ignore + (Declare.declare_constant + princ_id + (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + Flags.if_verbose + (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id ) fas bodies_types |