diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
4 files changed, 11 insertions, 8 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 55d361e3d..f8c7f98f6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -409,9 +409,9 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (Coqlib.build_coq_False ()) in - let coq_True = EConstr.of_constr (Coqlib.build_coq_True ()) in - let coq_I = EConstr.of_constr (Coqlib.build_coq_I ()) in + let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in + let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in + let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in @@ -1596,7 +1596,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> error "No tcc proof !!" | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ()) + | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 257f02b70..90a082d1e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -120,7 +120,8 @@ let def_of_const t = |_ -> assert false let coq_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; let find_reference sl s = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8c972cd7c..8eaa9b0f5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -546,7 +546,7 @@ and intros_with_rewrite_aux : tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENSEQ[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index eabad955e..00020609e 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -54,7 +54,9 @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["Arith";"Lt"] let coq_init_constant s = - EConstr.of_constr (Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s) + EConstr.of_constr ( + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -1223,7 +1225,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = Coqlib.build_coq_and () in + let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in let conj_constr = coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in |