diff options
Diffstat (limited to 'plugins')
30 files changed, 139 insertions, 155 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index ac0a875229..07f50f6cd5 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -10,9 +10,7 @@ open Constr -let contrib_name = "btauto" - -let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n) +let bt_lib_constr n = lazy (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref n) let decomp_term sigma (c : Constr.t) = Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) @@ -23,7 +21,6 @@ let (===) = Constr.equal module CoqList = struct - let typ = bt_lib_constr "core.list.type" let _nil = bt_lib_constr "core.list.nil" let _cons = bt_lib_constr "core.list.cons" @@ -32,12 +29,10 @@ module CoqList = struct let rec of_list ty = function | [] -> nil ty | t::q -> cons ty t (of_list ty q) - let type_of_list ty = lapp typ [|ty|] end module CoqPositive = struct - let typ = bt_lib_constr "num.pos.type" let _xH = bt_lib_constr "num.pos.xH" let _xO = bt_lib_constr "num.pos.xO" let _xI = bt_lib_constr "num.pos.xI" diff --git a/plugins/btauto/refl_btauto.mli b/plugins/btauto/refl_btauto.mli new file mode 100644 index 0000000000..5478fddba5 --- /dev/null +++ b/plugins/btauto/refl_btauto.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +module Btauto : sig val tac : unit Proofview.tactic end diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 7b4fd280bd..f6eea3c5c4 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -446,7 +446,7 @@ let error_MPfile_as_mod mp b = let argnames_of_global r = let env = Global.env () in - let typ, _ = Global.type_of_global_in_context env r in + let typ, _ = Typeops.type_of_global_in_context env r in let rels,_ = decompose_prod (Reduction.whd_all env typ) in List.rev_map fst rels @@ -878,7 +878,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in + let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 8fa676de44..b0c4785d7a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -233,12 +233,11 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) -let constant str = UnivGen.constr_of_global - @@ Coqlib.lib_ref str +let constant str = Coqlib.lib_ref str let defined_connectives = lazy - [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type"))); - AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))] + [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type")); + AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 98d68d3db7..ad1114b733 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -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 (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in - let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in - let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in + let coq_False = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type") in + let coq_True = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.type") in + let coq_I = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.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 @@ -1605,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 (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9ca91d62da..d57b931785 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -676,11 +676,15 @@ let build_case_scheme fa = (* in *) let funs = let (_,f,_) = fa in - try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) + try (let open GlobRef in + match Smartlocate.global_with_alias f with + | ConstRef c -> c + | IndRef _ | ConstructRef _ | VarRef _ -> assert false) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_qualid f) in - let first_fun,u = destConst funs in + 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 this_block_funs_indexes = get_funs_constant funs_mp first_fun in @@ -688,7 +692,7 @@ let build_case_scheme fa = let prop_sort = InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes + List.assoc_f Constant.equal funs this_block_funs_indexes in let (ind, sf) = let ind = first_fun_kn,funs_indexes in @@ -700,7 +704,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) -> - UnivGen.new_sort_in_family x + fst @@ UnivGen.fresh_sort_in_family x ) fa in @@ -718,7 +722,7 @@ let build_case_scheme fa = (Some princ_name) this_block_funs 0 - (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|]) + (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|]) in () diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 03a64988e4..28a9542167 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -116,7 +116,7 @@ let def_of_const t = [@@@ocaml.warning "-3"] let coq_constant s = - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -311,7 +311,7 @@ let pr_info f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr_env env sigma - (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) + (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ @@ -441,7 +441,7 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) @@ -449,7 +449,7 @@ let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) @@ -463,7 +463,7 @@ let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") [@@@ocaml.warning "-3"] -let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ +let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" [@@@ocaml.warning "+3"] diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b8973a18dc..b0842c3721 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")) + EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) with _ -> assert false (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] @@ -511,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune index 002eb28eea..9f583234d8 100644 --- a/plugins/funind/plugin_base.dune +++ b/plugins/funind/plugin_base.dune @@ -2,4 +2,5 @@ (name recdef_plugin) (public_name coq.plugins.recdef) (synopsis "Coq's functional induction plugin") + (flags :standard -open Gramlib) (libraries coq.plugins.extraction)) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 9fa333c629..f9df3aed45 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -24,6 +24,7 @@ open Globnames open Nameops open CErrors open Util +open UnivGen open Tacticals open Tacmach open Tactics @@ -50,7 +51,7 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) [@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "RecursiveDefinition" m s let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] @@ -62,7 +63,7 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) [@@@ocaml.warning "+3"] @@ -96,10 +97,7 @@ let type_of_const sigma t = Typeops.type_of_constant_in (Global.env()) (sp, u) |_ -> assert false -let constr_of_global x = - fst (Global.constr_of_global_in_context (Global.env ()) x) - -let constant sl s = constr_of_global (find_reference sl s) +let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s) let const_of_ref = function ConstRef kn -> kn @@ -1243,7 +1241,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in + let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune index 5611f5ba16..1b31655310 100644 --- a/plugins/ltac/plugin_base.dune +++ b/plugins/ltac/plugin_base.dune @@ -3,6 +3,7 @@ (public_name coq.plugins.ltac) (synopsis "Coq's LTAC tactic language") (modules :standard \ tauto) + (flags :standard -open Gramlib) (libraries coq.stm)) (library diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9dd98a4ab7..9f7669f1d5 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -89,8 +89,8 @@ let goalevars evars = fst evars let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = - let s = Typeclasses.set_resolvable Evd.Store.empty false in - let (evd', t) = Evarutil.new_evar ~store:s env evd t in + (** We handle the typeclass resolution of constraints ourselves *) + let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in let ev, _ = destEvar evd' t in (evd', Evar.Set.add ev cstrs), t @@ -632,9 +632,6 @@ let solve_remaining_by env sigma holes by = let no_constraints cstrs = fun ev _ -> not (Evar.Set.mem ev cstrs) -let all_constraints cstrs = - fun ev _ -> Evar.Set.mem ev cstrs - let poly_inverse sort = if sort then PropGlobal.inverse else TypeGlobal.inverse @@ -1453,10 +1450,11 @@ let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars = res let solve_constraints env (evars,cstrs) = - let filter = all_constraints cstrs in - Typeclasses.resolve_typeclasses env ~filter ~split:false ~fail:true - (Typeclasses.mark_resolvables ~filter evars) - + let oldtcs = Evd.get_typeclass_evars evars in + let evars' = Evd.set_typeclass_evars evars cstrs in + let evars' = Typeclasses.resolve_typeclasses env ~filter:all_evars ~split:false ~fail:true evars' in + Evd.set_typeclass_evars evars' oldtcs + let nf_zeta = Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 1f2c722b34..a88285c9ee 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -115,7 +115,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = (* Summary and Object declaration *) -open Nametab open Libobject type ltac_entry = { @@ -153,19 +152,19 @@ let tac_deprecation kn = let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Until i) sp kn in + let () = if not local then push_tactic (Nametab.Until i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Exactly i) sp kn in + let () = if not local then push_tactic (Nametab.Exactly i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with | None -> - let () = push_tactic (Until 1) sp kn in + let () = push_tactic (Nametab.Until 1) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 5501cf92a5..55412c74bb 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -19,7 +19,6 @@ open Util open Names open Libnames open Globnames -open Nametab open Smartlocate open Constrexpr open Termops @@ -98,7 +97,7 @@ let intern_global_reference ist qid = ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) else try ArgArg (qid.CAst.loc,locate_global_with_alias qid) - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid let intern_ltac_variable ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then @@ -150,7 +149,7 @@ let intern_isolated_tactic_reference strict ist qid = try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Internalize an applied tactic reference *) @@ -169,7 +168,7 @@ let intern_applied_tactic_reference ist qid = try intern_applied_global_tactic_reference qid with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Intern a reference parsed in a non-tactic entry *) @@ -190,7 +189,7 @@ let intern_non_tactic_reference strict ist qid = TacGeneric ipat else (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -302,7 +301,7 @@ let intern_evaluable_global_reference ist qid = try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) with Not_found -> if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) - else error_global_not_found qid + else Nametab.error_global_not_found qid let intern_evaluable_reference_or_by_notation ist = function | {v=AN r} -> intern_evaluable_global_reference ist r @@ -377,7 +376,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f90e889678..b60b77595b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -23,7 +23,6 @@ open Names open Nameops open Libnames open Globnames -open Nametab open Refiner open Tacmach.New open Tactic_debug @@ -358,7 +357,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -374,14 +373,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (qualid_of_ident ?loc id) + | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -640,7 +639,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found (qualid_of_ident ?loc id)) + Nametab.error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/plugin_base.dune index 0ae0e6855d..c2d396f0f9 100644 --- a/plugins/micromega/plugin_base.dune +++ b/plugins/micromega/plugin_base.dune @@ -5,3 +5,11 @@ (modules (:standard \ csdpcert)) (synopsis "Coq's micromega plugin") (libraries num coq.plugins.ltac)) + +(executable + (name csdpcert) + (public_name csdpcert) + (package coq) + (modules csdpcert) + (flags :standard -open Micromega_plugin) + (libraries coq.plugins.micromega)) diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 11d0a4a44d..ef60a23e80 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -135,7 +135,7 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) let tpexpr = gen_constant "plugins.setoid_ring.pexpr" let ttconst = gen_constant "plugins.setoid_ring.const" @@ -540,7 +540,7 @@ let nsatz lpol = let return_term t = let a = - mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in + mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index 9593e1225c..81bf1fb83d 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -229,17 +229,11 @@ Definition fast_Zmult_comm (x y : Z) (P : Z -> Prop) Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop) (H : P (- x + - y)) := eq_ind_r P H (Z.opp_add_distr x y). -Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) := - eq_ind_r P H (Z.opp_involutive x). - Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop) (H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y). Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop) (H : P (n * p + m * p)) := eq_ind_r P H (Z.mul_add_distr_r n m p). -Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop) - (H : P (x * - y)) := eq_ind_r P H (Z.mul_opp_comm x y). - Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop) (H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p). @@ -305,11 +299,9 @@ Register fast_Zred_factor5 as plugins.omega.fast_Zred_factor5. Register fast_Zred_factor6 as plugins.omega.fast_Zred_factor6. Register fast_Zmult_plus_distr_l as plugins.omega.fast_Zmult_plus_distr_l. -Register fast_Zmult_opp_comm as plugins.omega.fast_Zmult_opp_comm. Register fast_Zopp_plus_distr as plugins.omega.fast_Zopp_plus_distr. Register fast_Zopp_mult_distr_r as plugins.omega.fast_Zopp_mult_distr_r. Register fast_Zopp_eq_mult_neg_1 as plugins.omega.fast_Zopp_eq_mult_neg_1. -Register fast_Zopp_involutive as plugins.omega.fast_Zopp_involutive. Register new_var as plugins.omega.new_var. Register intro_Z as plugins.omega.intro_Z. diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index f55458de8d..d8adb17710 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -42,7 +42,6 @@ let elim_id id = simplest_elim (mkVar id) let resolve_id id = apply (mkVar id) -let display_time_flag = ref false let display_system_flag = ref false let display_action_flag = ref false let old_style_flag = ref false @@ -114,10 +113,6 @@ let new_identifier = let cpt = intref 0 in (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s) -let new_identifier_state = - let cpt = intref 0 in - (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s) - let new_identifier_var = let cpt = intref 0 in (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s) @@ -153,7 +148,6 @@ let mk_then tacs = tclTHENLIST tacs let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) let generalize_tac t = generalize t -let elim t = simplest_elim t let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let pf_nf gl c = pf_apply Tacred.simpl gl c @@ -165,10 +159,9 @@ let rev_assoc k = in loop -let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags = +let tag_hypothesis, hyp_of_tag, clear_tags = let l = ref ([]:(Id.t * int) list) in (fun h id -> l := (h,id):: !l), - (fun h -> try Id.List.assoc h !l with Not_found -> failwith "tag_hypothesis"), (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"), (fun () -> l := []) @@ -193,7 +186,8 @@ let reset_all () = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_global |> EConstr.of_constr) +let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global + |> EConstr.of_constr) (* Zarith *) @@ -259,11 +253,9 @@ let coq_fast_Zred_factor4 = gen_constant "plugins.omega.fast_Zred_factor4" let coq_fast_Zred_factor5 = gen_constant "plugins.omega.fast_Zred_factor5" let coq_fast_Zred_factor6 = gen_constant "plugins.omega.fast_Zred_factor6" let coq_fast_Zmult_plus_distr_l = gen_constant "plugins.omega.fast_Zmult_plus_distr_l" -let coq_fast_Zmult_opp_comm = gen_constant "plugins.omega.fast_Zmult_opp_comm" let coq_fast_Zopp_plus_distr = gen_constant "plugins.omega.fast_Zopp_plus_distr" let coq_fast_Zopp_mult_distr_r = gen_constant "plugins.omega.fast_Zopp_mult_distr_r" let coq_fast_Zopp_eq_mult_neg_1 = gen_constant "plugins.omega.fast_Zopp_eq_mult_neg_1" -let coq_fast_Zopp_involutive = gen_constant "plugins.omega.fast_Zopp_involutive" let coq_Zegal_left = gen_constant "plugins.omega.Zegal_left" let coq_Zne_left = gen_constant "plugins.omega.Zne_left" let coq_Zlt_left = gen_constant "plugins.omega.Zlt_left" @@ -363,23 +355,18 @@ let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus) let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle) let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt) -let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge) -let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt) let sp_not = lazy (evaluable_ref_of_constr "not" coq_not) -let mk_var v = mkVar (Id.of_string v) let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |]) let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2 -let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |]) let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |]) let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |]) let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |]) let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |]) let mk_not t = mkApp (Lazy.force coq_not, [| t |]) -let mk_eq_rel t1 t2 = mk_gen_eq (Lazy.force coq_comparison) t1 t2 let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) let mk_integer n = @@ -403,10 +390,6 @@ type omega_constant = | Le | Lt | Ge | Gt | Other of string -type omega_proposition = - | Keq of constr * constr * constr - | Kn - type result = | Kvar of Id.t | Kapp of omega_constant * constr list @@ -503,12 +486,7 @@ let recognize_number sigma t = type constr_path = | P_APP of int (* Abstraction and product *) - | P_BODY | P_TYPE - (* Case *) - | P_BRANCH of int - | P_ARITY - | P_ARG let context sigma operation path (t : constr) = let rec loop i p0 t = @@ -518,25 +496,10 @@ let context sigma operation path (t : constr) = | ((P_APP n :: p), App (f,v)) -> let v' = Array.copy v in v'.(pred n) <- loop i p v'.(pred n); mkApp (f, v') - | ((P_BRANCH n :: p), Case (ci,q,c,v)) -> - (* avant, y avait mkApp... anyway, BRANCH seems nowhere used *) - let v' = Array.copy v in - v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v')) - | ((P_ARITY :: p), App (f,l)) -> - mkApp (loop i p f,l) - | ((P_ARG :: p), App (f,v)) -> - let v' = Array.copy v in - v'.(0) <- loop i p v'.(0); mkApp (f,v') | (p, Fix ((_,n as ln),(tys,lna,v))) -> let l = Array.length v in let v' = Array.copy v in v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) - | ((P_BODY :: p), Prod (n,t,c)) -> - (mkProd (n,t,loop (succ i) p c)) - | ((P_BODY :: p), Lambda (n,t,c)) -> - (mkLambda (n,t,loop (succ i) p c)) - | ((P_BODY :: p), LetIn (n,b,t,c)) -> - (mkLetIn (n,b,t,loop (succ i) p c)) | ((P_TYPE :: p), Prod (n,t,c)) -> (mkProd (n,loop i p t,c)) | ((P_TYPE :: p), Lambda (n,t,c)) -> @@ -553,13 +516,7 @@ let occurrence sigma path (t : constr) = | (p, Cast (c,_,_)) -> loop p c | ([], _) -> t | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n) - | ((P_BRANCH n :: p), Case (_,_,_,v)) -> loop p v.(n) - | ((P_ARITY :: p), App (f,_)) -> loop p f - | ((P_ARG :: p), App (f,v)) -> loop p v.(0) | (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n) - | ((P_BODY :: p), Prod (n,t,c)) -> loop p c - | ((P_BODY :: p), Lambda (n,t,c)) -> loop p c - | ((P_BODY :: p), LetIn (n,b,t,c)) -> loop p c | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term @@ -584,7 +541,6 @@ let focused_simpl path = focused_simpl path type oformula = | Oplus of oformula * oformula - | Oinv of oformula | Otimes of oformula * oformula | Oatom of Id.t | Oz of bigint @@ -594,7 +550,6 @@ let rec oprint = function | Oplus(t1,t2) -> print_string "("; oprint t1; print_string "+"; oprint t2; print_string ")" - | Oinv t -> print_string "~"; oprint t | Otimes (t1,t2) -> print_string "("; oprint t1; print_string "*"; oprint t2; print_string ")" @@ -605,7 +560,6 @@ let rec oprint = function let rec weight = function | Oatom c -> intern_id c | Oz _ -> -1 - | Oinv c -> weight c | Otimes(c,_) -> weight c | Oplus _ -> failwith "weight" | Oufo _ -> -1 @@ -613,7 +567,6 @@ let rec weight = function let rec val_of = function | Oatom c -> mkVar c | Oz c -> mk_integer c - | Oinv c -> mkApp (Lazy.force coq_Zopp, [| val_of c |]) | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |]) | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |]) | Oufo c -> c @@ -908,10 +861,6 @@ let rec scalar p n = function clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zmult_plus_distr_l) :: (tac1 @ tac2), Oplus(t1',t2') - | Oinv t -> - [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zmult_opp_comm); - focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(neg n)) | Otimes(t1,Oz x) -> [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zmult_assoc_reverse); @@ -963,8 +912,6 @@ let rec negate p = function (Lazy.force coq_fast_Zopp_plus_distr) :: (tac1 @ tac2), Oplus(t1',t2') - | Oinv t -> - [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_involutive)], t | Otimes(t1,Oz x) -> [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] (Lazy.force coq_fast_Zopp_mult_distr_r); diff --git a/plugins/omega/coq_omega.mli b/plugins/omega/coq_omega.mli new file mode 100644 index 0000000000..a657826caa --- /dev/null +++ b/plugins/omega/coq_omega.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +val omega_solver : unit Proofview.tactic diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 79418da27c..840a05e02b 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -26,11 +26,11 @@ let step_count = ref 0 let node_count = ref 0 -let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -let li_and = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type")) -let li_or = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type")) +let li_False = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) +let li_and = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type")) +let li_or = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.or.type")) -let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) let l_xI = gen_constant "num.pos.xI" let l_xO = gen_constant "num.pos.xO" diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 85e759d152..a2dce621d9 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +module CVars = Vars open Ltac_plugin open Pp open Util @@ -150,8 +151,8 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let vars = Univops.universes_of_constr c in - let univs = Univops.restrict_universe_context univs vars in + let vars = CVars.universes_of_constr c in + let univs = UState.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~univs c), @@ -163,7 +164,7 @@ let ltac_call tac (args:glob_tactic_arg list) = let dummy_goal env sigma = let (gl,_,sigma) = - Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in + Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in {Evd.it = gl; Evd.sigma = sigma} let constr_of evd v = match Value.to_constr v with @@ -205,7 +206,7 @@ let exec_tactic env evd n f args = let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd -let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n))) +let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))) let gen_reference n = lazy (Coqlib.lib_ref n) let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory" @@ -250,7 +251,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) [@@ocaml.warning "-3"] let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) @@ -900,7 +901,7 @@ let ftheory_to_obj : field_info -> obj = let field_equality evd r inv req = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in + let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune index de9053f1a0..a13524bb52 100644 --- a/plugins/ssr/plugin_base.dune +++ b/plugins/ssr/plugin_base.dune @@ -3,4 +3,5 @@ (public_name coq.plugins.ssreflect) (synopsis "Coq's ssreflect plugin") (modules_without_implementation ssrast) + (flags :standard -open Gramlib) (libraries coq.plugins.ssrmatching)) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 1492cfb4e4..a284c3bfc7 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -730,13 +730,10 @@ let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project (** look up a name in the ssreflect internals module *) let ssrdirpath = DirPath.make [Id.of_string "ssreflect"] let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name) -let ssrtopqid name = Libnames.qualid_of_ident (Id.of_string name) -let locate_reference qid = - Smartlocate.global_of_extended_global (Nametab.locate_extended qid) let mkSsrRef name = - try locate_reference (ssrqid name) with Not_found -> - try locate_reference (ssrtopqid name) with Not_found -> - CErrors.user_err (Pp.str "Small scale reflection library not loaded") + let qn = Format.sprintf "plugins.ssreflect.%s" name in + if Coqlib.has_ref qn then Coqlib.lib_ref qn else + CErrors.user_err Pp.(str "Small scale reflection library not loaded (" ++ str name ++ str ")") let mkSsrRRef name = (DAst.make @@ GRef (mkSsrRef name,None)), None let mkSsrConst name env sigma = EConstr.fresh_global env sigma (mkSsrRef name) @@ -1220,7 +1217,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) + (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) @@ -1365,7 +1362,7 @@ let tacTYPEOF c = Goal.enter_one ~__LOC__ (fun g -> (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) -let unsafe_intro env store decl b = +let unsafe_intro env decl b = let open Context.Named.Declaration in Refine.refine ~typecheck:false begin fun sigma -> let ctx = Environ.named_context_val env in @@ -1374,7 +1371,7 @@ let unsafe_intro env store decl b = let ninst = EConstr.mkRel 1 :: inst in let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in let sigma, ev = - Evarutil.new_evar_instance nctx sigma nb ~principal:true ~store ninst in + Evarutil.new_evar_instance nctx sigma nb ~principal:true ninst in sigma, EConstr.mkNamedLambda_or_LetIn decl ev end @@ -1418,7 +1415,7 @@ let-in even after reduction, it fails. In case of success, the original name and final id are passed to the continuation [k] which gets evaluated. *) let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl -> let open Context in - let env, sigma, extra, g = Goal.(env gl, sigma gl, extra gl, concl gl) in + let env, sigma, g = Goal.(env gl, sigma gl, concl gl) in let decl, t, no_red = decompose_assum env sigma g in let original_name = Rel.Declaration.get_name decl in let already_used = Tacmach.New.pf_ids_of_hyps gl in @@ -1433,7 +1430,7 @@ let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl -> in if List.mem id already_used then errorstrm Pp.(Id.print id ++ str" already used"); - unsafe_intro env extra (set_decl_id id decl) t <*> + unsafe_intro env (set_decl_id id decl) t <*> (if no_red then tclUNIT () else tclFULL_BETAIOTA) <*> k ~orig_name:original_name ~new_name:id end diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 9ba23467e7..566a933522 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -212,8 +212,7 @@ val pf_abs_prod : EConstr.t -> Goal.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option -val mkSsrRef : string -> GlobRef.t -val mkSsrConst : +val mkSsrConst : string -> env -> evar_map -> evar_map * EConstr.t val pf_mkSsrConst : diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 460bdc6d23..e43cab094b 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -159,6 +159,10 @@ Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) := Notation "<hidden n >" := (abstract _ n _). Notation "T (* n *)" := (abstract T n abstract_key). +Register abstract_lock as plugins.ssreflect.abstract_lock. +Register abstract_key as plugins.ssreflect.abstract_key. +Register abstract as plugins.ssreflect.abstract. + (* Constants for tactic-views *) Inductive external_view : Type := tactic_view of Type. @@ -287,6 +291,8 @@ Variant phant (p : Type) := Phant. Definition protect_term (A : Type) (x : A) : A := x. +Register protect_term as plugins.ssreflect.protect_term. + (* The ssreflect idiom for a non-keyed pattern: *) (* - unkeyed t wiil match any subterm that unifies with t, regardless of *) (* whether it displays the same head symbol as t. *) @@ -336,6 +342,9 @@ Notation nosimpl t := (let: tt := tt in t). Lemma master_key : unit. Proof. exact tt. Qed. Definition locked A := let: tt := master_key in fun x : A => x. +Register master_key as plugins.ssreflect.master_key. +Register locked as plugins.ssreflect.locked. + Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed. (* Needed for locked predicates, in particular for eqType's. *) @@ -395,12 +404,18 @@ Definition ssr_have_let Pgoal Plemma step (rest : let x : Plemma := step in Pgoal) : Pgoal := rest. Arguments ssr_have_let [Pgoal]. +Register ssr_have as plugins.ssreflect.ssr_have. +Register ssr_have_let as plugins.ssreflect.ssr_have_let. + Definition ssr_suff Plemma Pgoal step (rest : Plemma) : Pgoal := step rest. Arguments ssr_suff Plemma [Pgoal]. Definition ssr_wlog := ssr_suff. Arguments ssr_wlog Plemma [Pgoal]. +Register ssr_suff as plugins.ssreflect.ssr_suff. +Register ssr_wlog as plugins.ssreflect.ssr_wlog. + (* Internal N-ary congruence lemmas for the congr tactic. *) Fixpoint nary_congruence_statement (n : nat) @@ -425,6 +440,9 @@ Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. Proof. by move->. Qed. Arguments ssr_congr_arrow : clear implicits. +Register nary_congruence as plugins.ssreflect.nary_congruence. +Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow. + (* View lemmas that don't use reflection. *) Section ApplyIff. diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 7f9a9e125e..5067d8af31 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -16,7 +16,6 @@ open Printer open Term open Constr open Termops -open Globnames open Tactypes open Tacmach @@ -98,6 +97,11 @@ let subgoals_tys sigma (relctx, concl) = * generalize the equality in case eqid is not None * 4. build the tactic handle intructions and clears as required in ipats and * by eqid *) + +let get_eq_type gl = + let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in + gl, EConstr.of_constr eq + let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac gl = (* some sanity checks *) let oc, orig_clr, occ, c_gen, gl = match what with @@ -115,8 +119,6 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM=="))); let fire_subst gl t = Reductionops.nf_evar (project gl) t in - let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in - let eq = EConstr.of_constr eq in let is_undef_pat = function | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t) | _ -> false in @@ -322,6 +324,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let k = List.length deps in let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in let gl, t = pfe_type_of gl c in + let gl, eq = get_eq_type gl in let gen_eq_tac, gl = let refl = EConstr.mkApp (eq, [|t; c; c|]) in let new_concl = EConstr.mkArrow refl (EConstr.Vars.lift 1 (pf_concl orig_gl)) in @@ -421,7 +424,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with let is_injection_case c gl = let gl, cty = pfe_type_of gl c in let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in - GlobRef.equal (IndRef mind) Coqlib.(lib_ref "core.eq.type") + Coqlib.check_ind_ref "core.eq.type" mind let perform_injection c gl = let gl, cty = pfe_type_of gl c in diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 876751911b..940defb743 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -360,7 +360,7 @@ let coerce_search_pattern_to_sort hpat = Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = - let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in + let hr, _ = Typeops.type_of_global_in_context env hr (** FIXME *) in Reductionops.splay_prod env sigma (EConstr.of_constr hr) in let np = List.length dc in if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune index 06f67c3774..1450a94de1 100644 --- a/plugins/ssrmatching/plugin_base.dune +++ b/plugins/ssrmatching/plugin_base.dune @@ -2,4 +2,5 @@ (name ssrmatching_plugin) (public_name coq.plugins.ssrmatching) (synopsis "Coq ssrmatching plugin") + (flags :standard -open Gramlib) (libraries coq.plugins.ltac)) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 4a63dd4708..7f67487f5d 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -356,8 +356,10 @@ let nf_open_term sigma0 ise c = let unif_end env sigma0 ise0 pt ok = let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in + let tcs = Evd.get_typeclass_evars ise in let s, uc, t = nf_open_term sigma0 ise pt in let ise1 = create_evar_defs s in + let ise1 = Evd.set_typeclass_evars ise1 (Evar.Set.filter (fun ev -> Evd.is_undefined ise1 ev) tcs) in let ise1 = Evd.set_universe_context ise1 uc in let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in if not (ok ise) then raise NoProgress else @@ -1045,7 +1047,7 @@ let thin id sigma goal = match ans with | None -> sigma | Some (sigma, hyps, concl) -> - let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in sigma |