From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/funind/functional_principles_proofs.ml | 60 ++++++++++++------------ plugins/funind/functional_principles_types.ml | 36 ++++++++------- plugins/funind/functional_principles_types.mli | 4 +- plugins/funind/g_indfun.ml4 | 15 +++--- plugins/funind/glob_term_to_relation.ml | 11 ++--- plugins/funind/glob_termops.ml | 25 +++++----- plugins/funind/glob_termops.mli | 2 +- plugins/funind/indfun.ml | 63 +++++++++++--------------- plugins/funind/indfun.mli | 5 +- plugins/funind/indfun_common.ml | 38 ++++++++-------- plugins/funind/indfun_common.mli | 14 +++--- plugins/funind/invfun.ml | 32 ++++++------- plugins/funind/invfun.mli | 4 +- plugins/funind/recdef.ml | 52 ++++++++++----------- plugins/funind/recdef.mli | 2 +- 15 files changed, 179 insertions(+), 184 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index d04887a4..268a012b 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 @@ -243,7 +243,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in + let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) 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"; @@ -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 @@ -638,11 +638,11 @@ let my_orelse tac1 tac2 g = (* observe (str "using snd tac since : " ++ CErrors.print e); *) tac2 g -let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = +let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = let args = Array.of_list (List.map mkVar args_id) in - let instanciate_one_hyp hid = + let instantiate_one_hyp hid = my_orelse - ( (* we instanciate the hyp if possible *) + ( (* we instantiate the hyp if possible *) fun g -> let prov_hid = pf_get_new_id hid g in let c = mkApp(mkVar hid,args) in @@ -678,7 +678,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = tclTHENLIST [ tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; - tclMAP instanciate_one_hyp hyps; + tclMAP instantiate_one_hyp hyps; (fun g -> let all_g_hyps_id = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty @@ -722,11 +722,11 @@ let build_proof tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); (fun g' -> let g'_nb_prod = nb_prod (project g') (pf_concl g') in - let nb_instanciate_partial = g'_nb_prod - g_nb_prod in + let nb_instantiate_partial = g'_nb_prod - g_nb_prod in observe_tac "treat_new_case" (treat_new_case ptes_infos - nb_instanciate_partial + nb_instantiate_partial (build_proof do_finalize) t dyn_infos) @@ -760,7 +760,7 @@ let build_proof nb_rec_hyps = List.length new_hyps } in -(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' +(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' (* build_proof do_finalize new_infos g' *) ) g | _ -> @@ -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 @@ -1050,9 +1050,9 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a (Global.env ()) !evd (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in - let res = EConstr.of_constr res in - evd:=evd'; - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in + evd:=evd'; + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in + evd := sigma; res in let nb_intro_to_do = nb_prod (project g) (pf_concl g) in @@ -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 @@ -1118,7 +1120,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in (full_params, (* real params *) princ_params, (* the params of the principle which are not params of the function *) - substl (* function instanciated with real params *) + substl (* function instantiated with real params *) (List.map var_of_decl full_params) f_body ) @@ -1128,7 +1130,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let f_body = compose_lam f_ctxt_other f_body in (princ_info.params, (* real params *) [],(* all params are full params *) - substl (* function instanciated with real params *) + substl (* function instantiated with real params *) (List.map var_of_decl princ_info.params) f_body ) @@ -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) @@ -1319,7 +1321,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) (* ); *) - (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac + (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id)) ] @@ -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) @@ -1369,7 +1371,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam do_prove dyn_infos in - instanciate_hyps_with_args prove_tac + instantiate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev 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)); @@ -1726,8 +1728,8 @@ let prove_principle_for_gen ptes_info (body_info rec_hyps) in - (* observe_tac "instanciate_hyps_with_args" *) - (instanciate_hyps_with_args + (* observe_tac "instantiate_hyps_with_args" *) + (instantiate_hyps_with_args make_proof (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) (List.rev args_ids) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 804548ce..b2a528a1 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -266,7 +266,7 @@ let change_property_sort evd toSort princ princName = (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) in let init = let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in - mkApp(princName_as_constr, + mkApp(EConstr.Unsafe.to_constr princName_as_constr, Array.init nargs (fun i -> mkRel (nargs - i ))) in @@ -291,7 +291,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in + evd := sigma; let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof @@ -321,8 +322,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) try let f = funs.(i) in - let env = Global.env () in - let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in + let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in let new_sorts = match sorts with | None -> Array.make (Array.length funs) (type_sort) @@ -343,7 +343,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = let evd' = Evd.from_env (Global.env ()) in - let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in + let evd',s = Evd.fresh_sort_in_family evd' fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in @@ -353,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Evd.const_univ_entry ~poly evd' in let ce = Declare.definition_entry ~univs value in - ignore( + ignore( Declare.declare_constant name (DefinitionEntry ce, @@ -507,8 +507,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x - ) + Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x + ) fas in (* We create the first priciple by tactic *) @@ -626,15 +626,19 @@ let build_scheme fas = Smartlocate.global_with_alias f with Not_found -> user_err ~hdr:"FunInd.build_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) + (str "Cannot find " ++ Libnames.pr_qualid f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in - if isConst f - then (destConst f,sort) - else user_err Pp.(pr_constr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function") - ) + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in + evd := sigma; + let c, u = + try EConstr.destConst !evd f + with DestKO -> + user_err Pp.(pr_econstr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function") + in + (c, EConstr.EInstance.kind !evd u), sort + ) fas ) in let bodies_types = @@ -663,7 +667,7 @@ let build_case_scheme fa = try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) in + (str "Cannot find " ++ Libnames.pr_qualid f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Constant.repr3 first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in @@ -684,7 +688,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/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 33aeafef..97f9acdb 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -36,5 +36,5 @@ exception No_graph_found val make_scheme : Evd.evar_map ref -> (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list -val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit -val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit +val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit +val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 90af20b4..a2d31780 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -15,7 +15,8 @@ open Indfun_common open Indfun open Genarg open Stdarg -open Misctypes +open Tacarg +open Tactypes open Pcoq open Pcoq.Prim open Pcoq.Constr @@ -38,7 +39,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 +126,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 @@ -165,7 +168,7 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ - Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ + Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++ Termops.pr_sort_family s VERNAC ARGUMENT EXTEND fun_scheme_arg @@ -178,11 +181,11 @@ let warning_error names e = let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in warn_cannot_define_graph (names,error) | Defining_principle e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then CErrors.print e else mt () in warn_cannot_define_principle (names,error) | _ -> raise e diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 04006453..926a2056 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -10,7 +10,6 @@ open Indfun_common open CErrors open Util open Glob_termops -open Misctypes module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -883,7 +882,7 @@ let is_res r = match DAst.get r with | _ -> false let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false let is_gvar c = match DAst.get c with @@ -892,7 +891,7 @@ let is_gvar c = match DAst.get c with let same_raw_term rt1 rt2 = match DAst.get rt1, DAst.get rt2 with - | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 + | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2 | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = @@ -1498,7 +1497,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> @@ -1510,7 +1509,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1525,7 +1524,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 769fcc1c..f81de82d 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,10 +1,10 @@ open Pp +open Constr open Glob_term open CErrors open Util open Names open Decl_kinds -open Misctypes (* Some basic functions to rebuild glob_constr @@ -16,8 +16,8 @@ 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 mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl) +let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) (* Some basic functions to decompose glob_constrs @@ -108,7 +108,7 @@ let change_vars = | GHole _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, - Miscops.map_cast_type (change_vars mapping) c) + Glob_ops.map_cast_type (change_vars mapping) c) ) rt and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in @@ -288,7 +288,7 @@ let rec alpha_rt excluded rt = | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, - Miscops.map_cast_type (alpha_rt excluded) c) + Glob_ops.map_cast_type (alpha_rt excluded) c) | GApp(f,args) -> GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args @@ -436,7 +436,7 @@ let replace_var_by_term x_id term = | GHole _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, - Miscops.map_cast_type replace_var_by_pattern c) + Glob_ops.map_cast_type replace_var_by_pattern c) ) x and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl @@ -536,7 +536,7 @@ let expand_as = | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,c) -> GCast(expand_as map b, - Miscops.map_cast_type (expand_as map) c) + Glob_ops.map_cast_type (expand_as map) c) | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) @@ -557,7 +557,8 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in - let ctx, f = Evarutil.nf_evars_and_universes ctx in + let ctx = Evd.minimize_universes ctx in + let f c = EConstr.of_constr (Evarutil.nf_evars_universes ctx (EConstr.Unsafe.to_constr c)) in (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = @@ -569,7 +570,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas (fun _ evi _ -> match evi.evar_source with | (loc_evi,ImplicitArg(gr_evi,p_evi,b_evi)) -> - if Globnames.eq_gr grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi + if GlobRef.equal grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi then raise (Found evi) | _ -> () ) @@ -580,8 +581,8 @@ If someone knows how to prevent solved existantial removal in understand, pleas with Found evi -> (* we found the evar corresponding to this hole *) match evi.evar_body with | Evar_defined c -> - (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) + (* we just have to lift the solution in glob_term *) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -603,7 +604,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 7088ae59..481a8be3 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -13,7 +13,7 @@ val pattern_to_term : cases_pattern -> glob_constr Some basic functions to rebuild glob_constr In each of them the location is Util.Loc.ghost *) -val mkGRef : Globnames.global_reference -> glob_constr +val mkGRef : GlobRef.t -> glob_constr val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 57863ee6..9eda19a8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -10,7 +10,7 @@ open Libnames open Globnames open Glob_term open Declarations -open Misctypes +open Tactypes open Decl_kinds module RelDecl = Context.Rel.Declaration @@ -77,8 +77,7 @@ let functional_induction with_clean c princl pat = user_err (str "Cannot find induction principle for " ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in - let princ = EConstr.of_constr princ in - (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') + (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') | _ -> raise (UserError(None,str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> @@ -99,7 +98,7 @@ let functional_induction with_clean c princl pat = List.map2 (fun c pat -> ((None, - Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))), + Tactics.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))), (None,pat), None)) (args@c_list) @@ -260,7 +259,6 @@ let derive_inversion fix_names = let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in - let c = EConstr.of_constr c in let (cst, u) = destConst evd c in evd, (cst, EInstance.kind evd u) :: l ) @@ -282,8 +280,7 @@ let derive_inversion fix_names = (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id))) in - let id = EConstr.of_constr id in - evd,(fst (destInd evd id))::l + evd,(fst (destInd evd id))::l ) fix_names (evd',[]) @@ -364,17 +361,17 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built i*) - let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in + let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in let ind_kn = fst (locate_with_msg - (pr_reference f_R_mut++str ": Not an inductive type!") + (pr_qualid f_R_mut++str ": Not an inductive type!") locate_ind f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = CAst.map (fun n -> Ident n) fname in - locate_with_msg - (pr_reference f_ref++str ": Not an inductive type!") + let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in + locate_with_msg + (pr_qualid f_ref++str ": Not an inductive type!") locate_constant f_ref in @@ -387,7 +384,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let evd = ref (Evd.from_env env) in let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in - let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in + let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in + evd := sigma; let princ_type = EConstr.Unsafe.to_constr princ_type in Functional_principles_types.generate_functional_principle evd @@ -424,7 +422,6 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in - let c = EConstr.of_constr c in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -441,7 +438,6 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in - let c = EConstr.of_constr c in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -480,7 +476,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,CAst.make @@ Ident fname,None) , + (None,qualid_of_ident fname,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -490,7 +486,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -547,9 +543,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = DirPath.make (List.rev_map Id.of_string l) in - CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path - (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) - in + Libnames.qualid_of_path + (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")) + in let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in @@ -730,12 +726,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof () let rec add_args id new_args = CAst.map (function - | CRef (r,_) as b -> - begin match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((None,r,None),new_args) - | _ -> b - end + | CRef (qid,_) as b -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((None,qid,None),new_args) + else b | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) @@ -749,13 +743,10 @@ let rec add_args id new_args = CAst.map (function add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) - | CAppExpl((pf,r,us),exprl) -> - begin - match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl)) - | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl) - end + | CAppExpl((pf,qid,us),exprl) -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl)) + else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl) | CApp((pf,b),bl) -> CApp((pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) @@ -785,7 +776,7 @@ let rec add_args id new_args = CAst.map (function | CSort _ as b -> b | CCast(b1,b2) -> CCast(add_args id new_args b1, - Miscops.map_cast_type (add_args id new_args) b2) + Glob_ops.map_cast_type (add_args id new_args) b2) | CRecord pars -> CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") @@ -849,7 +840,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph (f_ref:global_reference) = +let make_graph (f_ref : GlobRef.t) = let c,c_body = match f_ref with | ConstRef c -> @@ -890,7 +881,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None)) + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) nal | Constrexpr.CLocalPattern _ -> assert false ) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index dcc1c2ea..f209fb19 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,4 +1,5 @@ -open Misctypes +open Names +open Tactypes val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit @@ -18,4 +19,4 @@ val functional_induction : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val make_graph : Globnames.global_reference -> unit +val make_graph : GlobRef.t -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a0b9217c..4eee2c7a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -31,9 +31,7 @@ let id_of_name = function Name id -> id | _ -> raise Not_found -let locate ref = - let {CAst.v=qid} = qualid_of_reference ref in - Nametab.locate qid +let locate qid = Nametab.locate qid let locate_ind ref = match locate ref with @@ -109,7 +107,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 +115,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 +267,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 +300,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 +469,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 +477,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 +490,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/indfun_common.mli b/plugins/funind/indfun_common.mli index 5cc7163a..7e52ee22 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -20,11 +20,11 @@ val array_get_start : 'a array -> 'a array val id_of_name : Name.t -> Id.t -val locate_ind : Libnames.reference -> inductive -val locate_constant : Libnames.reference -> Constant.t +val locate_ind : Libnames.qualid -> inductive +val locate_constant : Libnames.qualid -> Constant.t val locate_with_msg : - Pp.t -> (Libnames.reference -> 'a) -> - Libnames.reference -> 'a + Pp.t -> (Libnames.qualid -> 'a) -> + Libnames.qualid -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list val list_union_eq : @@ -41,7 +41,7 @@ val chop_rprod_n : int -> Glob_term.glob_constr -> val def_of_const : Constr.t -> Constr.t val eq : EConstr.constr Lazy.t val refl_equal : EConstr.constr Lazy.t -val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) +val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr @@ -107,11 +107,11 @@ val h_intros: Names.Id.t list -> Tacmach.tactic val h_id : Names.Id.t val hrec_id : Names.Id.t val acc_inv_id : EConstr.constr Util.delayed -val ltof_ref : Globnames.global_reference Util.delayed +val ltof_ref : GlobRef.t Util.delayed val well_founded_ltof : EConstr.constr Util.delayed val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed -val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference +val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_reference val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index bed95740..ad11f853 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -23,7 +23,7 @@ open Tacticals open Tactics open Indfun_common open Tacmach -open Misctypes +open Tactypes open Termops open Context.Rel.Declaration @@ -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 @@ -102,9 +102,9 @@ let generate_type evd g_to_f f graph i = let evd',graph = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph))) in - let graph = EConstr.of_constr graph in evd:=evd'; - let graph_arity = Typing.e_type_of (Global.env ()) evd graph in + let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in + evd := sigma; let ctxt,_ = decompose_prod_assum !evd graph_arity in let fun_ctxt,res_type = match ctxt with @@ -172,7 +172,6 @@ let find_induction_principle evd f = | None -> raise Not_found | Some rect_lemma -> let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in - let rect_lemma = EConstr.of_constr rect_lemma in let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in evd:=evd'; rect_lemma,typ @@ -240,7 +239,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.map (fun decl -> List.map - (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id)) + (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches @@ -258,7 +257,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.fold_right (fun {CAst.v=pat} acc -> match pat with - | IntroNaming (IntroIdentifier id) -> id::acc + | IntroNaming (Namegen.IntroIdentifier id) -> id::acc | _ -> anomaly (Pp.str "Not an identifier.") ) (List.nth intro_pats (pred i)) @@ -513,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[ @@ -771,7 +770,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in + let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in + evd := sigma; let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info @@ -818,13 +818,12 @@ 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 (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in - let lem_cst_constr = EConstr.of_constr lem_cst_constr in - let (lem_cst,_) = destConst !evd lem_cst_constr in + let (lem_cst,_) = destConst !evd lem_cst_constr in update_Function {finfo with correctness_lemma = Some lem_cst}; ) @@ -880,12 +879,11 @@ 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 - let lem_cst_constr = EConstr.of_constr lem_cst_constr in - let (lem_cst,_) = destConst !evd lem_cst_constr in + let (lem_cst,_) = destConst !evd lem_cst_constr in update_Function {finfo with completeness_lemma = Some lem_cst} ) funs) @@ -969,7 +967,7 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic = Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]); thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); - Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); + Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid)); (fun g -> let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli index ad306ab2..3ddc6092 100644 --- a/plugins/funind/invfun.mli +++ b/plugins/funind/invfun.mli @@ -9,8 +9,8 @@ (************************************************************************) val invfun : - Misctypes.quantified_hypothesis -> - Globnames.global_reference option -> + Tactypes.quantified_hypothesis -> + Names.GlobRef.t option -> Evar.t Evd.sigma -> Evar.t list Evd.sigma val derive_correctness : (Evd.evar_map ref -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fb9ae64b..e9e8fcb6 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -37,7 +37,7 @@ open Glob_term open Pretyping open Termops open Constrintern -open Misctypes +open Tactypes open Genredexpr open Equality @@ -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) @@ -181,7 +181,7 @@ let simpl_iter clause = clause (* Others ugly things ... *) -let (value_f: Constr.t list -> global_reference -> Constr.t) = +let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = let open Term in let open Constr in fun al fterm -> @@ -215,7 +215,7 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) = let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) = +let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -356,7 +356,7 @@ type 'a infos = f_id : Id.t; (* function name *) f_constr : constr; (* function term *) f_terminate : constr; (* termination proof term *) - func : global_reference; (* functional reference *) + func : GlobRef.t; (* functional reference *) info : 'a; is_main_branch : bool; (* on the main branch or on a matched expression *) is_final : bool; (* final first order term or not *) @@ -713,7 +713,7 @@ let mkDestructEq : observe_tclTHENLIST (str "mkDestructEq") [Proofview.V82.of_tactic (generalize new_hyps); (fun g2 -> - let changefun patvars sigma = + let changefun patvars env sigma = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in Proofview.V82.of_tactic (change_in_concl None changefun) g2); @@ -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); *) @@ -1318,14 +1318,14 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | None -> try add_suffix current_proof_name "_subproof" with e when CErrors.noncritical e -> - anomaly (Pp.str "open_new_goal with an unamed theorem.") + anomaly (Pp.str "open_new_goal with an unnamed theorem.") in 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 opacity = - let na_ref = CAst.make @@ Libnames.Ident na in + let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1456,7 +1456,7 @@ let com_terminate -let start_equation (f:global_reference) (term_f:global_reference) +let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = let sigma = project g in let ids = pf_ids_of_hyps g in @@ -1473,7 +1473,7 @@ let start_equation (f:global_reference) (term_f:global_reference) observe_tac (str "prove_eq") (cont_tactic x)]) g;; let (com_eqn : int -> Id.t -> - global_reference -> global_reference -> global_reference + GlobRef.t -> GlobRef.t -> GlobRef.t -> Constr.t -> unit) = fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> let open CVars in @@ -1533,14 +1533,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let env = Global.env() in let evd = Evd.from_env env in let evd, function_type = interp_type_evars env evd type_of_f in - let function_type = EConstr.Unsafe.to_constr function_type in - let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in + let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in - let ty = EConstr.Unsafe.to_constr ty in - let evd, nf = Evarutil.nf_evars_and_universes evd in - let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in - let function_type = nf function_type in + let evd = Evd.minimize_universes evd in + let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in + let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in @@ -1579,7 +1577,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num 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 [CAst.make @@ Ident term_id] in + let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index b95d64ce..549f1fc0 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -14,6 +14,6 @@ bool -> int -> Constrexpr.constr_expr -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit -- cgit v1.2.3