diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 9 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 10 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 9 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
6 files changed, 24 insertions, 16 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8da30bd9c9..6fd2f7c2bc 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in + let eq_constr c1 c2 = + try ignore(Evarconv.unify_delay env sigma c1 c2); true + with Evarconv.UnableToUnify _ -> false in if not (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp sigma t) then nochange "not an equality"; diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 25a7675113..ca09cad1f3 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -353,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) in let names = ref [new_princ_name] in let hook = - fun new_principle_type _ _ -> + fun new_principle_type _ _ _ _ -> if Option.is_empty sorts then (* let id_of_f = Label.to_id (con_label f) in *) @@ -385,7 +385,8 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) - save false new_princ_name entry g_kind ~hook + let uctx = Evd.evar_universe_context sigma in + save false new_princ_name entry ~hook uctx g_kind with e when CErrors.noncritical e -> begin begin @@ -539,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ this_block_funs 0 (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) - (fun _ _ _ -> ()) + (fun _ _ _ _ _ -> ()) with e when CErrors.noncritical e -> begin begin @@ -614,7 +615,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ this_block_funs !i (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) - (fun _ _ _ -> ()) + (fun _ _ _ _ _ -> ()) in const with Found_type i -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 02964d7ba5..ba0a3bbb5c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl = construct in let argl = - if List.is_empty argl - then - Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) - ) - else argl + if List.is_empty argl then + List.make cst_narg (mkGHole ()) + else + List.make npar (mkGHole ()) @ argl in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f9938c0356..cba3cc3d42 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -129,7 +129,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const ?hook (locality,_,kind) = +let save with_clean id const ?hook uctx (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> @@ -144,7 +144,7 @@ let save with_clean id const ?hook (locality,_,kind) = (locality, ConstRef kn) in if with_clean then Proof_global.discard_current (); - Lemmas.call_hook ?hook ~fix_exn l r; + Lemmas.call_hook ?hook ~fix_exn uctx [] l r; definition_message id let with_full_print f a = diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 9584649cff..1e0b95df34 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -42,7 +42,14 @@ val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr -val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit +val save + : bool + -> Id.t + -> Safe_typing.private_constants Entries.definition_entry + -> ?hook:Lemmas.declaration_hook + -> UState.t + -> Decl_kinds.goal_kind + -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a8517e9ab1..8746c37309 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1310,7 +1310,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); - let hook _ _ = + let hook _ _ _ _ = let opacity = let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in @@ -1560,7 +1560,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook _ _ = + let hook _ _ _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in |