diff options
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 26 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 6 | ||||
-rw-r--r-- | plugins/funind/glob_termops.ml | 3 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 34 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 10 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 22 |
7 files changed, 54 insertions, 49 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 44fa0740d..533694864 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -230,7 +230,7 @@ let isAppConstruct ?(env=Global.env ()) sigma t = with Not_found -> false let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty + Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env exception NoChange @@ -414,9 +414,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 (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 coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ()) in + let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ()) in + let coq_I = EConstr.of_constr (UnivGen.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 @@ -598,7 +598,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = Proofview.V82.of_tactic (intro_using heq_id); onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) - tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps; + tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in @@ -1013,7 +1013,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); - Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); + Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))); evd @@ -1099,10 +1099,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let get_body const = match Global.body_of_constant const with | Some (body, _) -> + let env = Global.env () in + let sigma = Evd.from_env env in Tacred.cbv_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - (Global.env ()) - (Evd.empty) + env + sigma (EConstr.of_constr body) | None -> user_err Pp.(str "Cannot define a principle over an axiom ") in @@ -1242,7 +1244,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam if this_fix_info.idx + 1 = 0 then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) else - observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1))) + observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1))) else Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos 0) @@ -1340,7 +1342,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam nb_rec_hyps = -100; rec_hyps = []; info = - Reductionops.nf_betaiota (pf_env g) Evd.empty + Reductionops.nf_betaiota (pf_env g) (project g) (applist(fbody_with_full_params, (List.rev_map var_of_decl princ_params)@ (List.rev_map mkVar args_id) @@ -1603,7 +1605,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in (* let rec list_diff del_list check_list = *) (* match del_list with *) @@ -1657,7 +1659,7 @@ let prove_principle_for_gen (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) - (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1))); + (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index dc0f240bd..a158fc8ff 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -689,7 +689,7 @@ let build_case_scheme fa = let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> - Universes.new_sort_in_family x + UnivGen.new_sort_in_family x ) fa in diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 90af20b4c..0a2741ad1 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -38,7 +38,9 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () | Some b -> - let (_, b) = b (Global.env ()) Evd.empty in + let env = Global.env () in + let evd = Evd.from_env env in + let (_, b) = b env evd in spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) @@ -123,7 +125,7 @@ ARGUMENT EXTEND auto_using' END module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ +module Vernac = Pvernac.Vernac_ module Tactic = Pltac type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index ae238b846..bb1587507 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,4 +1,5 @@ open Pp +open Constr open Glob_term open CErrors open Util @@ -16,7 +17,7 @@ let mkGApp(rt,rtl) = DAst.make @@ GApp(rt,rtl) let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) -let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl) +let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl) let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) (* diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a0b9217c7..c6faa142a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -109,7 +109,7 @@ let const_of_id id = let def_of_const t = match Constr.kind t with - Term.Const sp -> + Const sp -> (try (match Environ.constant_opt_value_in (Global.env()) sp with | Some c -> c | _ -> assert false) @@ -117,7 +117,7 @@ let def_of_const t = |_ -> assert false let coq_constant s = - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -269,12 +269,12 @@ let subst_Function (subst,finfos) = in let function_constant' = do_subst_con finfos.function_constant in let graph_ind' = do_subst_ind finfos.graph_ind in - let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in - let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in - let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in - let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in - let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in - let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in + let equation_lemma' = Option.Smart.map do_subst_con finfos.equation_lemma in + let correctness_lemma' = Option.Smart.map do_subst_con finfos.correctness_lemma in + let completeness_lemma' = Option.Smart.map do_subst_con finfos.completeness_lemma in + let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in + let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in + let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -302,12 +302,12 @@ let classify_Function infos = Libobject.Substitute infos let discharge_Function (_,finfos) = let function_constant' = Lib.discharge_con finfos.function_constant and graph_ind' = Lib.discharge_inductive finfos.graph_ind - and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma - and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma - and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma - and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma - and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma - and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma + and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma + and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma + and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma + and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma + and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma + and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && @@ -471,7 +471,7 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" with e when CErrors.noncritical e -> raise (ToShow e) @@ -479,7 +479,7 @@ let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" with e when CErrors.noncritical e -> raise (ToShow e) @@ -492,7 +492,7 @@ 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 () = EConstr.of_constr @@ Universes.constr_of_global @@ +let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 094f54156..cc92a73f0 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -67,7 +67,7 @@ let observe_tac s tac g = let nf_zeta = Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) Environ.empty_env - Evd.empty + (Evd.from_env Environ.empty_env) let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl @@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) + EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ())) with _ -> assert false @@ -512,7 +512,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ @@ -818,7 +818,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); - (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); let finfo = find_Function_infos (fst f_as_constant) in (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global @@ -879,7 +879,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; - (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2a3a85fcc..72bb8253d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -49,7 +49,7 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) -let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ Coqlib.coq_reference "RecursiveDefinition" m s let arith_Nat = ["Arith";"PeanoNat";"Nat"] @@ -61,7 +61,7 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) let find_reference sl s = @@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) +let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Proof_global.Transparent,None))) let def_of_const t = match (Constr.kind t) with @@ -106,12 +106,12 @@ let const_of_ref = function let nf_zeta env = Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - env - Evd.empty + env (Evd.from_env env) let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty + Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env + (Evd.from_env Environ.empty_env) @@ -1152,7 +1152,7 @@ let termination_proof_header is_mes input_type ids args_id relation tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) )) ; - observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1))); + observe_tac (str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1))); h_intros args_id; Proofview.V82.of_tactic (Simple.intro wf_rec_arg); observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) @@ -1241,7 +1241,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in + let and_constr = UnivGen.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 @@ -1306,9 +1306,9 @@ let build_new_goal_type () = let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> Vernacexpr.Opaque - | Declarations.Undef _ -> Vernacexpr.Opaque - | Declarations.Def _ -> Vernacexpr.Transparent + | Declarations.OpaqueDef _ -> Proof_global.Opaque + | Declarations.Undef _ -> Proof_global.Opaque + | Declarations.Def _ -> Proof_global.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) |