diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 41 |
1 files changed, 21 insertions, 20 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 80167686aa..deaf603ef0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -274,10 +274,11 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro in let hook = Lemmas.mk_hook (hook new_principle_type) in begin + let evd,_ = Typing.e_type_of ~refresh:true (Global.env ()) Evd.empty new_principle_type in Lemmas.start_proof new_princ_name (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) - (*FIXME*) Evd.empty + evd new_principle_type hook ; @@ -323,7 +324,7 @@ let generate_functional_principle let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let value = change_property_sort s new_principle_type new_princ_name in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *) + let ce = Declare.definition_entry value in ignore( Declare.declare_constant name @@ -447,7 +448,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis let first_fun = List.hd funs in - let funs_mp,funs_dp,_ = Names.repr_con first_fun in + let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical first_fun) in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind @@ -498,27 +499,27 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis 0 (prove_princ_for_struct false 0 (Array.of_list funs)) (fun _ _ _ -> ()) - with e when Errors.noncritical e -> - begin - begin - try - let id = Pfedit.get_current_proof_name () in - let s = Id.to_string id in - let n = String.length "___________princ_________" in - if String.length s >= n - then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () - else () - else () - with e when Errors.noncritical e -> () - end; - raise (Defining_principle e) - end + with e when Errors.noncritical e -> + begin + begin + try + let id = Pfedit.get_current_proof_name () in + let s = Id.to_string id in + let n = String.length "___________princ_________" in + if String.length s >= n + then if String.equal (String.sub s 0 n) "___________princ_________" + then Pfedit.delete_current_proof () + else () + else () + with e when Errors.noncritical e -> () + end; + raise (Defining_principle e) + end in incr i; let opacity = - let finfos = find_Function_infos this_block_funs.(0) in + let finfos = find_Function_infos first_fun in try let equation = Option.get finfos.equation_lemma in Declareops.is_opaque (Global.lookup_constant equation) |