diff options
Diffstat (limited to 'plugins')
39 files changed, 418 insertions, 408 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5a939b4adf..ca33e4e757 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -941,7 +941,11 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = let equation_lemma = try - let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) in + let finfos = + match find_Function_infos (fst (destConst !evd f)) (*FIXME*) with + | None -> raise Not_found + | Some finfos -> finfos + in mkConst (Option.get finfos.equation_lemma) with (Not_found | Option.IsNone as e) -> let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in @@ -953,14 +957,18 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a let _ = match e with | Option.IsNone -> - let finfos = find_Function_infos (fst (destConst !evd f)) in - update_Function - {finfos with - equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with - GlobRef.ConstRef c -> c - | _ -> CErrors.anomaly (Pp.str "Not a constant.") - ) - } + let finfos = match find_Function_infos (fst (destConst !evd f)) with + | None -> raise Not_found + | Some finfos -> finfos + in + update_Function + {finfos with + equation_lemma = Some ( + match Nametab.locate (qualid_of_ident equation_lemma_id) with + | GlobRef.ConstRef c -> c + | _ -> CErrors.anomaly (Pp.str "Not a constant.") + ) + } | _ -> () in (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *) diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index d220058120..2b990400e3 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -91,7 +91,7 @@ END { let functional_induction b c x pat = - Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat)) + functional_induction true c x (Option.map out_disjunctive pat) } @@ -180,7 +180,7 @@ let is_proof_termination_interactively_checked recsl = let classify_as_Fixpoint recsl = Vernac_classifier.classify_vernac - (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl)))) + (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacFixpoint(NoDischarge, List.map snd recsl)})) let classify_funind recsl = match classify_as_Fixpoint recsl with diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 730ae48393..570b72136c 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt = let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') -let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = +let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in (* let time1 = System.get_time () in *) @@ -199,10 +199,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> - name, entry, hook + entry, hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") @@ -234,6 +234,23 @@ let change_property_sort evd toSort princ princName = ) (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params) +(* XXX: To be cleaned up soon in favor of common save path. *) +let save name const ?hook uctx scope kind = + let open Declare in + let open DeclareDef in + let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in + let r = match scope with + | Discharge -> + let c = SectionLocalDef const in + let () = declare_variable ~name ~kind c in + GlobRef.VarRef name + | Global local -> + let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in + GlobRef.ConstRef kn + in + DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); + definition_message name + let generate_functional_principle (evd: Evd.evar_map ref) interactive_proof old_princ_type sorts new_princ_name funs i proof_tac @@ -282,7 +299,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort Sorts.InProp; register_with_sort Sorts.InSet in - let id,entry,hook = + let entry, hook = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -495,14 +512,17 @@ let find_induction_principle evd f = | Constr.Const c' -> c' | _ -> CErrors.user_err Pp.(str "Must be used with a function") in - let infos = find_Function_infos f_as_constant in - match infos.rect_lemma with - | None -> raise Not_found - | Some rect_lemma -> - let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (GlobRef.ConstRef rect_lemma) in - let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in - evd:=evd'; - rect_lemma,typ + match find_Function_infos f_as_constant with + | None -> + raise Not_found + | Some infos -> + match infos.rect_lemma with + | None -> raise Not_found + | Some rect_lemma -> + let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (GlobRef.ConstRef rect_lemma) in + let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in + evd:=evd'; + rect_lemma,typ (* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ] is the tactic used to prove correctness lemma. @@ -1016,12 +1036,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti *) let rewrite_tac j ids : Tacmach.tactic = let graph_def = graphs.(j) in - let infos = - try find_Function_infos (fst (destConst (project g) funcs.(j))) - with Not_found -> CErrors.user_err Pp.(str "No graph found") + let infos = match find_Function_infos (fst (destConst (project g) funcs.(j))) with + | None -> + CErrors.user_err Pp.(str "No graph found") + | Some infos -> infos in - if infos.is_general - || Rtree.is_infinite Declareops.eq_recarg graph_def.Declarations.mind_recargs + if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.Declarations.mind_recargs then let eq_lemma = try Option.get (infos).equation_lemma @@ -1167,16 +1187,16 @@ let get_funs_constant mp = in l_const -let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list = +let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Declare.proof_entry list = let exception Found_type of int in let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in let first_fun_kn = - try - fst (find_Function_infos (fst first_fun)).graph_ind - with Not_found -> raise No_graph_found + match find_Function_infos (fst first_fun) with + | None -> raise No_graph_found + | Some finfos -> fst finfos.graph_ind in let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in @@ -1216,9 +1236,21 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef s::l_schemes -> s,l_schemes | _ -> CErrors.anomaly (Pp.str "") in - let _,const,_ = + let opaque = + let finfos = + match find_Function_infos (fst first_fun) with + | None -> raise Not_found + | Some finfos -> finfos + in + let open Proof_global in + match finfos.equation_lemma with + | None -> Transparent (* non recursive definition *) + | Some equation -> + if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent + in + let entry, _hook = try - build_functional_principle evd false + build_functional_principle ~opaque evd false first_type (Array.of_list sorts) this_block_funs @@ -1230,27 +1262,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef in incr i; - let opacity = - let finfos = find_Function_infos (fst first_fun) in - try - let equation = Option.get finfos.equation_lemma in - Declareops.is_opaque (Global.lookup_constant equation) - with Option.IsNone -> (* non recursive definition *) - false - in - let const = {const with Proof_global.proof_entry_opaque = opacity } in (* The others are just deduced *) if List.is_empty other_princ_types - then - [const] + then [entry] else let other_fun_princ_types = let funs = Array.map Constr.mkConstU this_block_funs in let sorts = Array.of_list sorts in List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types in - let open Proof_global in - let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in + let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in let other_result = @@ -1277,7 +1298,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let _,const,_ = + let entry, _hook = build_functional_principle evd false @@ -1288,20 +1309,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef (Functional_principles_proofs.prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) (fun _ _ -> ()) in - const + entry with Found_type i -> let princ_body = Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt in - {const with - proof_entry_body = - (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); - proof_entry_type = Some scheme_type - } + Declare.definition_entry ~types:scheme_type princ_body ) other_fun_princ_types in - const::other_result + entry::other_result (* [derive_correctness funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] @@ -1352,7 +1369,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = Array.of_list (List.map (fun entry -> - (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type )) + (EConstr.of_constr (fst (fst (Future.force entry.Declare.proof_entry_body))), + EConstr.of_constr (Option.get entry.Declare.proof_entry_type )) ) (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) @@ -1381,7 +1399,11 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma in let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in - let finfo = find_Function_infos (fst f_as_constant) in + let finfo = + match find_Function_infos (fst f_as_constant) with + | None -> raise Not_found + | Some finfo -> finfo + 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 @@ -1443,7 +1465,11 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) lemma) in let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in - let finfo = find_Function_infos (fst f_as_constant) in + let finfo = + match find_Function_infos (fst f_as_constant) with + | None -> raise Not_found + | Some finfo -> finfo + in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in let (lem_cst,_) = destConst !evd lem_cst_constr in @@ -1600,7 +1626,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w let b = Names.Id.of_string "___b" in Constrexpr_ops.mkLambdaC( [CAst.make @@ Name a; CAst.make @@ Name b], - Constrexpr.Default Decl_kinds.Explicit, + Constrexpr.Default Glob_term.Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, [ @@ -2028,7 +2054,11 @@ let build_case_scheme fa = let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in let first_fun = funs in let funs_mp = Constant.modpath first_fun in - let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in + let first_fun_kn = + match find_Function_infos first_fun with + | None -> raise No_graph_found + | Some finfos -> fst finfos.graph_ind + in let this_block_funs_indexes = get_funs_constant funs_mp first_fun in let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in let prop_sort = Sorts.InProp in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 798c62d549..7c17ecdba0 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1252,7 +1252,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function | GSort _ -> params | GHole _ -> params | GIf _ | GRec _ | GCast _ -> - raise (UserError(Some "compute_cst_params", str "Not handled case")) + CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case") ) gt and compute_cst_params_from_app acc (params,rtl) = let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in @@ -1300,7 +1300,7 @@ let rec rebuild_return_type rt = | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], - Constrexpr.Default Decl_kinds.Explicit, rt)], + Constrexpr.Default Explicit, rt)], CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true})) let do_build_inductive @@ -1517,7 +1517,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)}) ++ fnl () ++ msg in @@ -1532,7 +1532,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = 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 d36d86a65b..8abccabae6 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,10 +1,18 @@ -open Pp +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Constr open Glob_term open CErrors open Util open Names -open Decl_kinds (* Some basic functions to rebuild glob_constr @@ -434,7 +442,8 @@ let replace_var_by_term x_id term = replace_var_by_pattern lhs, replace_var_by_pattern rhs ) - | GRec _ -> raise (UserError(None,str "Not handled GRec")) + | GRec _ -> + CErrors.user_err (Pp.str "Not handled GRec") | GSort _ | GHole _ as rt -> rt | GInt _ as rt -> rt diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 24b3690138..70211a1860 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Names open Glob_term diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index eeb2f246c2..a205c0744a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -8,15 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open CErrors -open Sorts +open Pp open Util +open CErrors open Names +open Sorts open Constr open EConstr -open Pp + +open Tacmach.New +open Tacticals.New +open Tactics + open Indfun_common -open Tactypes module RelDecl = Context.Rel.Declaration @@ -37,111 +41,107 @@ let choose_dest_or_ind scheme_info args = Tactics.induction_destruct (is_rec_info sigma scheme_info) false args) let functional_induction with_clean c princl pat = - let res = - fun g -> - let sigma = Tacmach.project g in + let open Proofview.Notations in + Proofview.Goal.enter_one (fun gl -> + let sigma = project gl in let f,args = decompose_app sigma c in - let princ,bindings, princ_type,g' = - match princl with - | None -> (* No principle is given let's find the good one *) - begin - match EConstr.kind sigma f with - | Const (c',u) -> - let princ_option = - let finfo = (* we first try to find out a graph on f *) - try find_Function_infos c' - with Not_found -> - user_err (str "Cannot find induction information on "++ - Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) - in - match Tacticals.elimination_sort_of_goal g with - | InSProp -> finfo.sprop_lemma - | InProp -> finfo.prop_lemma - | InSet -> finfo.rec_lemma - | InType -> finfo.rect_lemma + match princl with + | None -> (* No principle is given let's find the good one *) + begin + match EConstr.kind sigma f with + | Const (c',u) -> + let princ_option = + let finfo = (* we first try to find out a graph on f *) + match find_Function_infos c' with + | Some finfo -> finfo + | None -> + user_err (str "Cannot find induction information on "++ + Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') ) + in + match elimination_sort_of_goal gl with + | InSProp -> finfo.sprop_lemma + | InProp -> finfo.prop_lemma + | InSet -> finfo.rec_lemma + | InType -> finfo.rect_lemma + in + let princ = (* then we get the principle *) + match princ_option with + | Some princ -> + let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT princ + | None -> + (*i If there is not default lemma defined then, + we cross our finger and try to find a lemma named f_ind + (or f_rec, f_rect) i*) + let princ_name = + Indrec.make_elimination_ident + (Label.to_id (Constant.label c')) + (elimination_sort_of_goal gl) in - let princ,g' = (* then we get the principle *) + let princ_ref = try - let g',princ = - Tacmach.pf_eapply (Evd.fresh_global) g (GlobRef.ConstRef (Option.get princ_option )) in - princ,g' - with Option.IsNone -> - (*i If there is not default lemma defined then, - we cross our finger and try to find a lemma named f_ind - (or f_rec, f_rect) i*) - let princ_name = - Indrec.make_elimination_ident - (Label.to_id (Constant.label c')) - (Tacticals.elimination_sort_of_goal g) - in - try - let princ_ref = const_of_id princ_name in - let (a,b) = Tacmach.pf_eapply (Evd.fresh_global) g princ_ref in - (b,a) - (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) - with Not_found -> (* This one is neither defined ! *) - user_err (str "Cannot find induction principle for " - ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) + Constrintern.locate_reference (Libnames.qualid_of_ident princ_name) + with + | Not_found -> + user_err (str "Cannot find induction principle for " + ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') ) in - (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)) -> - princ,binding,Tacmach.pf_unsafe_type_of g princ,g - in - let sigma = Tacmach.project g' in - let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in - let args_as_induction_constr = - let c_list = - if princ_infos.Tactics.farg_in_concl - then [c] else [] - in - if List.length args + List.length c_list = 0 - then user_err Pp.(str "Cannot recognize a valid functional scheme" ); - let encoded_pat_as_patlist = - List.make (List.length args + List.length c_list - 1) None @ [pat] - in - List.map2 - (fun c pat -> - ((None, - Tactics.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))), - (None,pat), - None)) - (args@c_list) - encoded_pat_as_patlist - in - let princ' = Some (princ,bindings) in - let princ_vars = - List.fold_right - (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc) - args - Id.Set.empty + let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) princ_ref in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT princ + in + princ >>= fun princ -> + (* We need to refresh gl due to the updated evar_map in princ *) + Proofview.Goal.enter_one (fun gl -> + Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args)) + | _ -> + CErrors.user_err (str "functional induction must be used with a function" ) + end + | Some ((princ,binding)) -> + Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args) + ) >>= fun (princ, bindings, princ_type, args) -> + Proofview.Goal.enter (fun gl -> + let sigma = project gl in + let princ_infos = compute_elim_sig (project gl) princ_type in + let args_as_induction_constr = + let c_list = + if princ_infos.Tactics.farg_in_concl + then [c] else [] in - let old_idl = List.fold_right Id.Set.add (Tacmach.pf_ids_of_hyps g) Id.Set.empty in - let old_idl = Id.Set.diff old_idl princ_vars in - let subst_and_reduce g = - if with_clean - then - let idl = - List.filter (fun id -> not (Id.Set.mem id old_idl)) - (Tacmach.pf_ids_of_hyps g) - in - let flag = - Genredexpr.Cbv - {Redops.all_flags - with Genredexpr.rDelta = false; - } - in - Tacticals.tclTHEN - (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl ) - (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl)) - g - else Tacticals.tclIDTAC g + if List.length args + List.length c_list = 0 + then user_err Pp.(str "Cannot recognize a valid functional scheme" ); + let encoded_pat_as_patlist = + List.make (List.length args + List.length c_list - 1) None @ [pat] in - Tacticals.tclTHEN - (Proofview.V82.of_tactic (choose_dest_or_ind - princ_infos - (args_as_induction_constr,princ'))) - subst_and_reduce - g' - in res + List.map2 + (fun c pat -> + ((None, ElimOnConstr (fun env sigma -> (sigma,(c,Tactypes.NoBindings)))), + (None,pat), None)) + (args@c_list) + encoded_pat_as_patlist + in + let princ' = Some (princ,bindings) in + let princ_vars = + List.fold_right + (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc) + args + Id.Set.empty + in + let old_idl = List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty in + let old_idl = Id.Set.diff old_idl princ_vars in + let subst_and_reduce gl = + if with_clean + then + let idl = List.filter (fun id -> not (Id.Set.mem id old_idl))(pf_ids_of_hyps gl) in + let flag = Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false } in + tclTHEN + (tclMAP (fun id -> tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl) + (reduce flag Locusops.allHypsAndConcl) + else tclIDTAC + in + tclTHEN + (choose_dest_or_ind + princ_infos + (args_as_induction_constr,princ')) + (Proofview.Goal.enter subst_and_reduce)) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 97a840e950..476d74b3f8 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -8,9 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val functional_induction : - bool -> - EConstr.constr -> - (EConstr.constr * EConstr.constr Tactypes.bindings) option -> - Ltac_plugin.Tacexpr.or_and_intro_pattern option -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma +val functional_induction + : bool + -> EConstr.constr + -> (EConstr.constr * EConstr.constr Tactypes.bindings) option + -> Ltac_plugin.Tacexpr.or_and_intro_pattern option + -> unit Proofview.tactic diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 52a29fb559..80fc64fe65 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -40,7 +40,9 @@ let locate_constant ref = let locate_with_msg msg f x = try f x - with Not_found -> raise (CErrors.UserError(None, msg)) + with + | Not_found -> + CErrors.user_err msg let filter_map filter f = @@ -64,8 +66,7 @@ let chop_rlambda_n = | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> - raise (CErrors.UserError(Some "chop_rlambda_n", - str "chop_rlambda_n: Not enough Lambdas")) + CErrors.user_err ~hdr:"chop_rlambda_n" (str "chop_rlambda_n: Not enough Lambdas") in chop_lambda_n [] @@ -76,7 +77,8 @@ let chop_rprod_n = else match DAst.get rt with | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) + | _ -> + CErrors.user_err ~hdr:"chop_rprod_n" (str "chop_rprod_n: Not enough products") in chop_prod_n [] @@ -92,13 +94,6 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l -let const_of_id id = - let princ_ref = qualid_of_ident id in - try Constrintern.locate_reference princ_ref - with Not_found -> - CErrors.user_err ~hdr:"IndFun.const_of_id" - (str "cannot find " ++ Id.print id) - [@@@ocaml.warning "-3"] let coq_constant s = UnivGen.constr_of_monomorphic_global @@ @@ -112,29 +107,6 @@ let find_reference sl s = let eq = lazy(EConstr.of_constr (coq_constant "eq")) let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) -(*****************************************************************) -(* Copy of the standard save mechanism but without the much too *) -(* slow reduction function *) -(*****************************************************************) -open Declare -open DeclareDef - -let definition_message = Declare.definition_message - -let save name const ?hook uctx scope kind = - let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in - let r = match scope with - | Discharge -> - let c = SectionLocalDef const in - let () = declare_variable ~name ~kind c in - GlobRef.VarRef name - | Global local -> - let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in - GlobRef.ConstRef kn - in - DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); - definition_message name - let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () @@ -301,20 +273,16 @@ let find_or_none id = ) with Not_found -> None - - let find_Function_infos f = - Cmap_env.find f !from_function - + Cmap_env.find_opt f !from_function let find_Function_of_graph ind = - Indmap.find ind !from_graph + Indmap.find_opt ind !from_graph let update_Function finfo = (* Pp.msgnl (pr_info finfo); *) Lib.add_anonymous_leaf (in_Function finfo) - let add_Function is_general f = let f_id = Label.to_id (Constant.label f) in let equation_lemma = find_or_none (mk_equation_id f_id) diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index fff4711044..cd5202a6c7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -38,20 +38,10 @@ val chop_rprod_n : int -> Glob_term.glob_constr -> val eq : EConstr.constr Lazy.t val refl_equal : EConstr.constr Lazy.t -val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr val make_eq : unit -> EConstr.constr -val save - : Id.t - -> Evd.side_effects Proof_global.proof_entry - -> ?hook:DeclareDef.Hook.t - -> UState.t - -> DeclareDef.locality - -> Decls.logical_kind - -> unit - (* [with_full_print f a] applies [f] to [a] in full printing environment. This function preserves the print settings @@ -75,8 +65,8 @@ type function_info = is_general : bool; } -val find_Function_infos : Constant.t -> function_info -val find_Function_of_graph : inductive -> function_info +val find_Function_infos : Constant.t -> function_info option +val find_Function_of_graph : inductive -> function_info option (* WARNING: To be used just after the graph definition !!! *) val add_Function : bool -> Constant.t -> unit val update_Function : function_info -> unit diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 38fdd789a3..d72319d078 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -34,9 +34,10 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl -> let ((kn',num) as ind'),u = destInd sigma i in if MutInd.equal kn kn' then (* We have generated a graph hypothesis so that we must change it if we can *) - let info = - try find_Function_of_graph ind' - with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) + let info = match find_Function_of_graph ind' with + | Some info -> info + | None -> + (* The graphs are mutually recursive but we cannot find one of them !*) CErrors.anomaly (Pp.str "Cannot retrieve infos about a mutual block.") in (* if we can find a completeness lemma for this function @@ -108,18 +109,20 @@ let invfun qhyp f = | _ -> CErrors.user_err Pp.(str "Not a function") in - try - let finfos = find_Function_infos f in - let f_correct = mkConst(Option.get finfos.correctness_lemma) - and kn = fst finfos.graph_ind in - Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp - with - | Not_found -> CErrors.user_err (Pp.str "No graph found") - | Option.IsNone -> CErrors.user_err (Pp.str "Cannot use equivalence with graph!") - -exception NoFunction + match find_Function_infos f with + | None -> + CErrors.user_err (Pp.str "No graph found") + | Some finfos -> + match finfos.correctness_lemma with + | None -> + CErrors.user_err (Pp.str "Cannot use equivalence with graph!") + | Some f_correct -> + let f_correct = mkConst f_correct + and kn = fst finfos.graph_ind in + Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp let invfun qhyp f = + let exception NoFunction in match f with | Some f -> invfun qhyp f | None -> @@ -132,31 +135,33 @@ let invfun qhyp f = let f1,_ = decompose_app sigma args.(1) in try if not (isConst sigma f1) then raise NoFunction; - let finfos = find_Function_infos (fst (destConst sigma f1)) in + let finfos = Option.get (find_Function_infos (fst (destConst sigma f1))) in let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f1 f_correct - with | NoFunction | Option.IsNone | Not_found -> - try - let f2,_ = decompose_app sigma args.(2) in - if not (isConst sigma f2) then raise NoFunction; - let finfos = find_Function_infos (fst (destConst sigma f2)) in - let f_correct = mkConst(Option.get finfos.correctness_lemma) - and kn = fst finfos.graph_ind - in - functional_inversion kn hid f2 f_correct with - | NoFunction -> - CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") - | Option.IsNone -> - if do_observe () - then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality") - else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) - | Not_found -> - if do_observe () - then CErrors.user_err (Pp.str "No graph found for any side of equality") - else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + | NoFunction | Option.IsNone -> + let f2,_ = decompose_app sigma args.(2) in + if isConst sigma f2 then + match find_Function_infos (fst (destConst sigma f2)) with + | None -> + if do_observe () + then CErrors.user_err (Pp.str "No graph found for any side of equality") + else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + | Some finfos -> + match finfos.correctness_lemma with + | None -> + if do_observe () + then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality") + else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + | Some f_correct -> + let f_correct = mkConst f_correct + and kn = fst finfos.graph_ind + in + functional_inversion kn hid f2 f_correct + else (* NoFunction *) + CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") end | _ -> CErrors.user_err Pp.(Ppconstr.pr_id hid ++ str " must be an equality ") in diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 7cd43cb5cd..9b52b710c1 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -24,7 +24,6 @@ open Tactypes open Tactics open Inv open Locus -open Decl_kinds open Pcoq @@ -450,9 +449,9 @@ GRAMMAR EXTEND Gram | -> { true } ] ] ; simple_binder: - [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@ + [ [ na=name -> { ([na],Default Glob_term.Explicit, CAst.make ~loc @@ CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) } - | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) } + | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Glob_term.Explicit,c) } ] ] ; fixdecl: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 0e38ce575b..6df068883c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -20,7 +20,6 @@ open Stdarg open Notation_gram open Tactypes open Locus -open Decl_kinds open Genredexpr open Ppconstr open Pputils @@ -1097,7 +1096,7 @@ let pr_goal_selector ~toplevel s = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else match DAst.get ty with - Glob_term.GProd(na,Explicit,a,b) -> + Glob_term.GProd(na,Glob_term.Explicit,a,b) -> strip_ty (([CAst.make na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 726752a2bf..1493092f2f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -546,7 +546,7 @@ let rewrite_core_unif_flags = { Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = Evar.Set.empty; + Unification.allowed_evars = Unification.AllowAll; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 94af4a3151..ba759441e5 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -189,31 +189,32 @@ let flatten_contravariant_disj _ ist = tclTHEN (tclTHENLIST tacs) tac0 | _ -> fail -let make_unfold name = - let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in - let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in - Locus.(AllOccurrences, ArgArg (EvalConstRef const, None)) +let evalglobref_of_globref = + function + | GlobRef.VarRef v -> EvalVarRef v + | GlobRef.ConstRef c -> EvalConstRef c + | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> assert false -let u_not = make_unfold "not" +let make_unfold name = + let const = evalglobref_of_globref (Coqlib.lib_ref name) in + Locus.(AllOccurrences, ArgArg (const, None)) let reduction_not_iff _ ist = let make_reduce c = TacAtom (CAst.make @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in let tac = match !negation_unfolding with - | true -> make_reduce [u_not] + | true -> make_reduce [make_unfold "core.not.type"] | false -> TacId [] in eval_tactic_ist ist tac -let coq_nnpp_path = - let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in - Libnames.make_path (DirPath.make dir) (Id.of_string "NNPP") - let apply_nnpp _ ist = + let nnpp = "core.nnpp.type" in Proofview.tclBIND (Proofview.tclUNIT ()) - begin fun () -> try - Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply - with Not_found -> tclFAIL 0 (Pp.mt ()) + begin fun () -> + if Coqlib.has_ref nnpp + then Tacticals.New.pf_constr_of_global (Coqlib.lib_ref nnpp) >>= apply + else tclFAIL 0 (Pp.mt ()) end (* This is the uniform mode dealing with ->, not, iff and types isomorphic to diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 78bfe480b3..2762bb6b32 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -19,6 +19,47 @@ Require Export Ring_theory. Local Open Scope positive_scope. Import RingSyntax. +(** Definition of polynomial expressions *) +#[universes(template)] +Inductive PExpr {C} : Type := +| PEc : C -> PExpr +| PEX : positive -> PExpr +| PEadd : PExpr -> PExpr -> PExpr +| PEsub : PExpr -> PExpr -> PExpr +| PEmul : PExpr -> PExpr -> PExpr +| PEopp : PExpr -> PExpr +| PEpow : PExpr -> N -> PExpr. +Arguments PExpr : clear implicits. + + (* Definition of multivariable polynomials with coefficients in C : + Type [Pol] represents [X1 ... Xn]. + The representation is Horner's where a [n] variable polynomial + (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients + are polynomials with [n-1] variables (C[X2..Xn]). + There are several optimisations to make the repr compacter: + - [Pc c] is the constant polynomial of value c + == c*X1^0*..*Xn^0 + - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables. + variable indices are shifted of j in Q. + == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn} + - [PX P i Q] is an optimised Horner form of P*X^i + Q + with P not the null polynomial + == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn} + + In addition: + - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden + since they can be represented by the simpler form (PX P (i+j) Q) + - (Pinj i (Pinj j P)) is (Pinj (i+j) P) + - (Pinj i (Pc c)) is (Pc c) + *) + +#[universes(template)] +Inductive Pol {C} : Type := +| Pc : C -> Pol +| Pinj : positive -> Pol -> Pol +| PX : Pol -> positive -> Pol -> Pol. +Arguments Pol : clear implicits. + Section MakeRingPol. (* Ring elements *) @@ -96,33 +137,11 @@ Section MakeRingPol. match goal with |- ?t == _ => mul_permut_rec t end). - (* Definition of multivariable polynomials with coefficients in C : - Type [Pol] represents [X1 ... Xn]. - The representation is Horner's where a [n] variable polynomial - (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients - are polynomials with [n-1] variables (C[X2..Xn]). - There are several optimisations to make the repr compacter: - - [Pc c] is the constant polynomial of value c - == c*X1^0*..*Xn^0 - - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables. - variable indices are shifted of j in Q. - == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn} - - [PX P i Q] is an optimised Horner form of P*X^i + Q - with P not the null polynomial - == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn} + Notation PExpr := (PExpr C). + Notation Pol := (Pol C). - In addition: - - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden - since they can be represented by the simpler form (PX P (i+j) Q) - - (Pinj i (Pinj j P)) is (Pinj (i+j) P) - - (Pinj i (Pc c)) is (Pc c) - *) - - #[universes(template)] - Inductive Pol : Type := - | Pc : C -> Pol - | Pinj : positive -> Pol -> Pol - | PX : Pol -> positive -> Pol -> Pol. + Implicit Types pe : PExpr. + Implicit Types P : Pol. Definition P0 := Pc cO. Definition P1 := Pc cI. @@ -152,7 +171,7 @@ Section MakeRingPol. | _ => Pinj j P end. - Definition mkPinj_pred j P:= + Definition mkPinj_pred j P := match j with | xH => P | xO j => Pinj (Pos.pred_double j) P @@ -938,18 +957,6 @@ Qed. rewrite <- IHm; auto. Qed. - (** Definition of polynomial expressions *) - - #[universes(template)] - Inductive PExpr : Type := - | PEc : C -> PExpr - | PEX : positive -> PExpr - | PEadd : PExpr -> PExpr -> PExpr - | PEsub : PExpr -> PExpr -> PExpr - | PEmul : PExpr -> PExpr -> PExpr - | PEopp : PExpr -> PExpr - | PEpow : PExpr -> N -> PExpr. - (** evaluation of polynomial expressions towards R *) Definition mk_X j := mkPinj_pred j mkX. diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index a99f21ad47..3c72d3268f 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -68,7 +68,7 @@ Require Import EnvRing. Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q := match e with | PEc c => c - | PEX _ j => env j + | PEX j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) @@ -80,7 +80,7 @@ Lemma Qeval_expr_simpl : forall env e, Qeval_expr env e = match e with | PEc c => c - | PEX _ j => env j + | PEX j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 75801162a7..cddc140f51 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -289,7 +289,6 @@ destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor). now apply (Rplus_nonneg_nonneg sor). Qed. -#[universes(template)] Inductive Psatz : Type := | PsatzIn : nat -> Psatz | PsatzSquare : PolC -> Psatz @@ -892,7 +891,7 @@ Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C := | Pc c => PEc c | Pinj j p => xdenorm (Pos.add j jmp ) p | PX p j q => PEadd - (PEmul (xdenorm jmp p) (PEpow (PEX _ jmp) (Npos j))) + (PEmul (xdenorm jmp p) (PEpow (PEX jmp) (Npos j))) (xdenorm (Pos.succ jmp) q) end. @@ -961,7 +960,7 @@ Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c). Fixpoint map_PExpr (e : PExpr S) : PExpr C := match e with | PEc c => PEc (C_of_S c) - | PEX _ p => PEX _ p + | PEX p => PEX p | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2) | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2) | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2) diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index 56032befba..d6ccf582ae 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -27,7 +27,6 @@ Section S. Context {AA : Type}. (* type of annotations for atoms *) Context {AF : Type}. (* type of formulae identifiers *) - #[universes(template)] Inductive GFormula : Type := | TT : GFormula | FF : GFormula diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index 79cb6a3a3e..f93fe021f9 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -27,16 +27,18 @@ Set Implicit Arguments. * As a side note, by dropping the polymorphism, one gets small, yet noticeable, speed-up. *) +Inductive t {A} : Type := +| Empty : t +| Elt : A -> t +| Branch : t -> A -> t -> t . +Arguments t : clear implicits. + Section MakeVarMap. Variable A : Type. Variable default : A. - #[universes(template)] - Inductive t : Type := - | Empty : t - | Elt : A -> t - | Branch : t -> A -> t -> t . + Notation t := (t A). Fixpoint find (vm : t) (p:positive) {struct vm} : A := match vm with @@ -49,7 +51,6 @@ Section MakeVarMap. end end. - Fixpoint singleton (x:positive) (v : A) : t := match x with | xH => Elt v diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 3ea7635244..c0d22486b5 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -65,7 +65,7 @@ Qed. Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z := match e with | PEc c => c - | PEX _ x => env x + | PEX x => env x | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2 | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2 | PEpow e1 n => Z.pow (Zeval_expr env e1) (Z.of_N n) @@ -78,7 +78,7 @@ Definition eval_expr := eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x Fixpoint Zeval_const (e: PExpr Z) : option Z := match e with | PEc c => Some c - | PEX _ x => None + | PEX x => None | PEadd e1 e2 => map_option2 (fun x y => Some (x + y)) (Zeval_const e1) (Zeval_const e2) | PEmul e1 e2 => map_option2 (fun x y => Some (x * y)) @@ -742,7 +742,7 @@ Module Vars. Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t := match e with | PEc _ => Vars.empty - | PEX _ x => Vars.singleton x + | PEX x => Vars.singleton x | PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 => let v1 := vars_of_pexpr e1 in let v2 := vars_of_pexpr e2 in @@ -774,10 +774,10 @@ Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type} end. Definition bound_var (v : positive) : Formula Z := - Build_Formula (PEX _ v) OpGe (PEc 0). + Build_Formula (PEX v) OpGe (PEc 0). Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z := - Build_Formula (PEX _ x) OpEq (PEsub (PEX _ y) (PEX _ t)). + Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)). Section BOUND. Context {TX TG ID : Type}. diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index a64a5a84b3..2e97dfea19 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -556,6 +556,15 @@ let zeq_bool x y = | Eq -> true | _ -> false +type 'c pExpr = +| PEc of 'c +| PEX of positive +| PEadd of 'c pExpr * 'c pExpr +| PEsub of 'c pExpr * 'c pExpr +| PEmul of 'c pExpr * 'c pExpr +| PEopp of 'c pExpr +| PEpow of 'c pExpr * n + type 'c pol = | Pc of 'c | Pinj of positive * 'c pol @@ -868,15 +877,6 @@ let rec psquare cO cI cadd cmul ceqb = function let p3 = psquare cO cI cadd cmul ceqb p2 in mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2 -type 'c pExpr = -| PEc of 'c -| PEX of positive -| PEadd of 'c pExpr * 'c pExpr -| PEsub of 'c pExpr * 'c pExpr -| PEmul of 'c pExpr * 'c pExpr -| PEopp of 'c pExpr -| PEpow of 'c pExpr * n - (** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **) let mk_X cO cI j = diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 0ca0d0c12d..6b92445326 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -77,20 +77,24 @@ Lget i (l ++ delta) = Some a. induction l;destruct i;simpl;try congruence;auto. Qed. -Section Store. - -Variable A:Type. - -#[universes(template)] -Inductive Poption : Type:= +Inductive Poption {A} : Type:= PSome : A -> Poption | PNone : Poption. +Arguments Poption : clear implicits. -#[universes(template)] -Inductive Tree : Type := +Inductive Tree {A} : Type := Tempty : Tree | Branch0 : Tree -> Tree -> Tree | Branch1 : A -> Tree -> Tree -> Tree. +Arguments Tree : clear implicits. + +Section Store. + +Variable A:Type. + +Notation Poption := (Poption A). +Notation Tree := (Tree A). + Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption := match T with @@ -179,7 +183,6 @@ generalize i;clear i;induction j;destruct T;simpl in H|-*; destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence. Qed. -#[universes(template)] Record Store : Type := mkStore {index:positive;contents:Tree}. @@ -194,7 +197,6 @@ Lemma get_empty : forall i, get i empty = PNone. intro i; case i; unfold empty,get; simpl;reflexivity. Qed. -#[universes(template)] Inductive Full : Store -> Type:= F_empty : Full empty | F_push : forall a S, Full S -> Full (push a S). diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index b4300da4d5..3736bc47a5 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -730,7 +730,6 @@ Qed. (* The input: syntax of a field expression *) -#[universes(template)] Inductive FExpr : Type := | FEO : FExpr | FEI : FExpr @@ -763,7 +762,6 @@ Strategy expand [FEeval]. (* The result of the normalisation *) -#[universes(template)] Record linear : Type := mk_linear { num : PExpr C; denum : PExpr C; @@ -946,7 +944,6 @@ induction e2; intros p1 p2; now rewrite <- PEpow_mul_r. Qed. -#[universes(template)] Record rsplit : Type := mk_rsplit { rsplit_left : PExpr C; rsplit_common : PExpr C; diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index b024f65988..a98a963207 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -740,7 +740,6 @@ Ltac abstract_ring_morphism set ext rspec := | _ => fail 1 "bad ring structure" end. -#[universes(template)] Record hypo : Type := mkhypo { hypo_type : Type; hypo_proof : hypo_type diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 6a8c514a7b..048c8eecf9 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -32,7 +32,6 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. with coefficients in C : *) -#[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | PX : Pol -> positive -> positive -> Pol -> Pol. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 9d56084fd4..092114ff0b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -121,7 +121,6 @@ Section MakeRingPol. - (Pinj i (Pc c)) is (Pc c) *) - #[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol @@ -909,7 +908,6 @@ Section MakeRingPol. (** Definition of polynomial expressions *) - #[universes(template)] Inductive PExpr : Type := | PEO : PExpr | PEI : PExpr diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 8f24b281c6..dc45853458 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -540,7 +540,6 @@ Section AddRing. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). Variable req : R -> R -> Prop. *) -#[universes(template)] Inductive ring_kind : Type := | Abstract | Computational diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index eb75fca0a1..b456d2eed2 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -151,7 +151,7 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in - let univs = UState.restrict_universe_context univs vars in + let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in let () = Declare.declare_universe_context ~poly:false univs in let types = (Typeops.infer (Global.env ()) c).uj_type in let univs = Monomorphic_entry Univ.ContextSet.empty in diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index bf0761d3ae..376410658a 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -1323,7 +1323,6 @@ Proof. by move=> x y r2xy; apply/orP; right. Qed. (** Variant of simpl_pred specialised to the membership operator. **) -#[universes(template)] Variant mem_pred T := Mem of pred T. (** @@ -1464,7 +1463,6 @@ Implicit Types (mp : mem_pred T). Definition Acoll : collective_pred T := [pred x | ...]. as the collective_pred_of_simpl is _not_ convertible to pred_of_simpl. **) -#[universes(template)] Structure registered_applicative_pred p := RegisteredApplicativePred { applicative_pred_value :> pred T; _ : applicative_pred_value = p @@ -1473,21 +1471,18 @@ Definition ApplicativePred p := RegisteredApplicativePred (erefl p). Canonical applicative_pred_applicative sp := ApplicativePred (applicative_pred_of_simpl sp). -#[universes(template)] Structure manifest_simpl_pred p := ManifestSimplPred { simpl_pred_value :> simpl_pred T; _ : simpl_pred_value = SimplPred p }. Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)). -#[universes(template)] Structure manifest_mem_pred p := ManifestMemPred { mem_pred_value :> mem_pred T; _ : mem_pred_value = Mem [eta p] }. Canonical expose_mem_pred p := ManifestMemPred (erefl (Mem [eta p])). -#[universes(template)] Structure applicative_mem_pred p := ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}. Canonical check_applicative_mem_pred p (ap : registered_applicative_pred p) := @@ -1538,7 +1533,6 @@ End PredicateSimplification. (** Qualifiers and keyed predicates. **) -#[universes(template)] Variant qualifier (q : nat) T := Qualifier of {pred T}. Coercion has_quality n T (q : qualifier n T) : {pred T} := @@ -1573,7 +1567,6 @@ Variable T : Type. Variant pred_key (p : {pred T}) := DefaultPredKey. Variable p : {pred T}. -#[universes(template)] Structure keyed_pred (k : pred_key p) := PackKeyedPred {unkey_pred :> {pred T}; _ : unkey_pred =i p}. @@ -1605,7 +1598,6 @@ Section KeyedQualifier. Variables (T : Type) (n : nat) (q : qualifier n T). -#[universes(template)] Structure keyed_qualifier (k : pred_key q) := PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}. Definition KeyedQualifier k := PackKeyedQualifier k (erefl q). diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 33e9f871fd..473612fda7 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -181,7 +181,6 @@ let option_assert_get o msg = (** Constructors for rawconstr *) open Glob_term -open Decl_kinds let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 71abafc22f..9ebdf71329 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -209,7 +209,6 @@ Register abstract_key as plugins.ssreflect.abstract_key. Register abstract as plugins.ssreflect.abstract. (** Constants for tactic-views **) -#[universes(template)] Inductive external_view : Type := tactic_view of Type. (** diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index aa1316f15e..4c6b7cdcb6 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -128,10 +128,9 @@ let newssrcongrtac arg ist gl = x, re_sig si sigma in let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in let ssr_congr lr = EConstr.mkApp (arr, lr) in + let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in (* here the two cases: simple equality or arrow *) - let equality, _, eq_args, gl' = - let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in - pf_saturate gl (EConstr.of_constr eq) 3 in + let equality, _, eq_args, gl' = pf_saturate gl (EConstr.of_constr eq) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist) (fun () -> @@ -336,17 +335,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ let sigma, p = (* The resulting goal *) Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in - let elim, gl = - let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in + let sigma, elim = let sort = elimination_sort_of_goal gl in - let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in - if dir = R2L then elim, gl else (* taken from Coq's rewrite *) - let elim, _ = destConst elim in - let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in - let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in - mkConst c1', gl in - let elim = EConstr.of_constr elim in + match Equality.eq_elimination_ref (dir = L2R) sort with + | Some r -> Evd.fresh_global env sigma r + | None -> + let ((kn, i) as ind, _), unfolded_c_ty = Tacred.reduce_to_quantified_ind env sigma c_ty in + let sort = elimination_sort_of_goal gl in + let sigma, elim = Evd.fresh_global env sigma (Indrec.lookup_eliminator env ind sort) in + if dir = R2L then sigma, elim else + let elim, _ = EConstr.destConst sigma elim in + let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in + let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in + let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in + sigma, EConstr.of_constr (mkConst c1') + in let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in (* We check the proof is well typed *) let sigma, proof_ty = @@ -491,7 +494,8 @@ let rwprocess_rule dir rule gl = | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in EConstr.mkApp (pi2, ra), sigma in - if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then + let sigma,trty = Evd.fresh_global env sigma Coqlib.(lib_ref "core.True.type") in + if EConstr.eq_constr sigma a.(0) trty then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 5e600362b4..0ce3752a51 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -391,19 +391,19 @@ Notation "@^~ x" := (fun f => f x) : fun_scope. Definitions and notation for explicit functions with simplification, i.e., which simpl and /= beta expand (this is complementary to nosimpl). **) +#[universes(template)] +Variant simpl_fun (aT rT : Type) := SimplFun of aT -> rT. + Section SimplFun. Variables aT rT : Type. -#[universes(template)] -Variant simpl_fun := SimplFun of aT -> rT. +Definition fun_of_simpl (f : simpl_fun aT rT) := fun x => let: SimplFun lam := f in lam x. -Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. +End SimplFun. Coercion fun_of_simpl : simpl_fun >-> Funclass. -End SimplFun. - Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : fun_scope. Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : fun_scope. Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : fun_scope. diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 175a863ad8..a1f707ffa8 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -32,7 +32,6 @@ open Ppconstr open Namegen open Tactypes -open Decl_kinds open Constrexpr open Constrexpr_ops @@ -1337,20 +1336,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde | [ ssrbvar(bv) ] -> { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ")" ] -> { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> { let x = bvar_lname bv in (FwdPose, [BFdecl 1]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] -> { let xs = List.map bvar_lname (bv :: bvs) in let n = List.length xs in (FwdPose, [BFdecl n]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] -> { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] -> @@ -1362,7 +1361,7 @@ GRAMMAR EXTEND Gram ssrbinder: [ [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> { (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ] ]; END @@ -1391,7 +1390,7 @@ let push_binders c2 bs = let rec fix_binders = let open CAst in function | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs -> - CLocalAssum (xs, Default Explicit, t) :: fix_binders bs + CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs | (_, { v = CLetIn (x, v, oty, _) } ) :: bs -> CLocalDef (x, v, oty) :: fix_binders bs | _ -> [] @@ -1521,7 +1520,7 @@ let intro_id_to_binder = List.map (function | IPatId id -> let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), - CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], + CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)], mkCHole None) | _ -> anomaly "non-id accepted as binder") diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 0adabb0673..f3f1d713e9 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -27,7 +27,6 @@ open Notation_ops open Notation_term open Glob_term open Stdarg -open Decl_kinds open Pp open Ppconstr open Printer diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 17db25660f..4d7a04f5ee 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -36,7 +36,6 @@ open Ppconstr open Printer open Globnames open Namegen -open Decl_kinds open Evar_kinds open Constrexpr open Constrexpr_ops diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index a148a3bc73..9808c61255 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -112,7 +112,7 @@ let vernac_numeral_notation local ty f g scope opts = let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in let arrow x y = - mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) in let opt r = app (mkRefC (q_option ())) r in let constructors = get_constructors tyc in diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index 8c0f9a3339..c92acb0f55 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -61,7 +61,7 @@ let vernac_string_notation local ty f g scope = let of_ty = Smartlocate.global_with_alias g in let cty = cref ty in let arrow x y = - mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) in let constructors = get_constructors tyc in (* Check the type of f *) |