diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index ea985ddecd..2476478abe 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 = @@ -469,13 +470,17 @@ exception ToShow of exn let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; - EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq") + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; - EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl") + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = @@ -486,7 +491,10 @@ let hrec_id = Id.of_string "hrec" let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded") let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") -let well_founded_ltof = function () -> EConstr.of_constr (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof") + +let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@ + Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" + let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *) @@ -502,13 +510,13 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; let decompose_lam_n sigma n = - if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive"; + if n < 0 then CErrors.user_err Pp.(str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match EConstr.kind sigma c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | _ -> CErrors.error "decompose_lam_n: not enough abstractions" + | _ -> CErrors.user_err Pp.(str "decompose_lam_n: not enough abstractions") in lamdec_rec [] n |