diff options
36 files changed, 90 insertions, 84 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 2aeb1ea202..4778bf1121 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -340,15 +340,6 @@ let subst_retro_action subst action = let c' = subst_constant subst c in if c == c' then action else Register_type(prim, c') -(* Here the semantics is completely unclear. - What does "Hint Unfold t" means when "t" is a parameter? - Does the user mean "Unfold X.t" or does she mean "Unfold y" - where X.t is later on instantiated with y? I choose the first - interpretation (i.e. an evaluable reference is never expanded). *) -let subst_evaluable_reference subst = function - | EvalVarRef id -> EvalVarRef id - | EvalConstRef kn -> EvalConstRef (subst_constant subst kn) - let rec map_kn f f' c = let func = map_kn f f' in match kind c with diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index bc5816dafb..9cf270cff7 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -146,14 +146,6 @@ val subst_proj : substitution -> Projection.t -> Projection.t val subst_retro_action : substitution -> Retroknowledge.action -> Retroknowledge.action -(** Here the semantics is completely unclear. - What does "Hint Unfold t" means when "t" is a parameter? - Does the user mean "Unfold X.t" or does she mean "Unfold y" - where X.t is later on instantiated with y? I choose the first - interpretation (i.e. an evaluable reference is never expanded). *) -val subst_evaluable_reference : - substitution -> evaluable_global_reference -> evaluable_global_reference - (** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t diff --git a/kernel/names.ml b/kernel/names.ml index be65faf234..60c6c7bd67 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1100,16 +1100,6 @@ module GlobRef = struct end -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -(* Better to have it here that in closure, since used in grammar.cma *) -let eq_egr e1 e2 = match e1, e2 with - EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 - | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 - | _, _ -> false - (** Located identifiers and objects with syntax. *) type lident = Id.t CAst.t diff --git a/kernel/names.mli b/kernel/names.mli index 747299bb12..09885396c0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -714,14 +714,6 @@ module GlobRef : sig end -(** Better to have it here that in Closure, since required in grammar.cma *) -(* XXX: Move to a module *) -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool - (** Located identifiers and objects with syntax. *) type lident = Id.t CAst.t diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 73eb943418..67b6839b6e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1260,7 +1260,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num tclTHENLIST [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalConstRef (fst fname) ) ] + , Tacred.EvalConstRef (fst fname) ) ] ; (let do_prove = build_proof interactive_proof (Array.to_list fnames) diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 314c8abcaf..c344fdd611 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -917,13 +917,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic = tclTHENLIST [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(1)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(1)) ) ] ; tclMAP (fun id -> tclTRY (unfold_in_hyp [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(1)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(1)) ) ] (destVar sigma args.(1), Locus.InHyp))) (pf_ids_of_hyps g) ; intros_with_rewrite () ] @@ -936,13 +936,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic = tclTHENLIST [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(2)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(2)) ) ] ; tclMAP (fun id -> tclTRY (unfold_in_hyp [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(2)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(2)) ) ] (destVar sigma args.(2), Locus.InHyp))) (pf_ids_of_hyps g) ; intros_with_rewrite () ] @@ -1158,7 +1158,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : else unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalConstRef + , Tacred.EvalConstRef (fst (destConst (Proofview.Goal.sigma g) f)) ) ] in (* The proof of each branche itself *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6464556e4e..266345a324 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -418,6 +418,7 @@ let make_eq () = with _ -> assert false let evaluable_of_global_reference r = + let open Tacred in (* Tacred.evaluable_of_global_reference (Global.env ()) *) match r with | GlobRef.ConstRef sp -> EvalConstRef sp diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 7b7044fdaf..e25f413fe4 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -100,7 +100,7 @@ val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed val evaluable_of_global_reference : - GlobRef.t -> Names.evaluable_global_reference + GlobRef.t -> Tacred.evaluable_global_reference val list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index faad792ea9..6ebb01703f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -191,8 +191,8 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_and_short_name pr (c,_) = pr c let pr_evaluable_reference = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (GlobRef.ConstRef sp) + | Tacred.EvalVarRef id -> pr_id id + | Tacred.EvalConstRef sp -> pr_global (GlobRef.ConstRef sp) let pr_quantified_hypothesis = function | AnonHyp n -> int n @@ -381,8 +381,8 @@ let string_of_genarg_arg (ArgumentType arg) = str "<" ++ KerName.print kn ++ str ">" let pr_evaluable_reference_env env = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> + | Tacred.EvalVarRef id -> pr_id id + | Tacred.EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef sp) let pr_as_disjunctive_ipat prc ipatl = diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 79e0adf9f7..4f58eceb59 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -106,7 +106,7 @@ val pr_may_eval : val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t -val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t +val pr_evaluable_reference_env : env -> Tacred.evaluable_global_reference -> Pp.t val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9abdc2ddbe..5e88bf7c79 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -276,6 +276,7 @@ let coerce_to_closed_constr env v = c let coerce_to_evaluable_ref env sigma v = + let open Tacred in let fail () = raise (CannotCoerceTo "an evaluable reference") in let ev = match is_intro_pattern v with diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index b8592c5c76..8ca2510459 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -69,7 +69,7 @@ val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr val coerce_to_closed_constr : Environ.env -> Value.t -> constr val coerce_to_evaluable_ref : - Environ.env -> Evd.evar_map -> Value.t -> evaluable_global_reference + Environ.env -> Evd.evar_map -> Value.t -> Tacred.evaluable_global_reference val coerce_to_constr_list : Environ.env -> Value.t -> constr list diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 7b2c8e1d04..a880a3305e 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -270,7 +270,7 @@ constraint 'a = < type g_trm = Genintern.glob_constr_and_expr type g_pat = Genintern.glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var +type g_cst = Tacred.evaluable_global_reference Genredexpr.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -324,7 +324,7 @@ type raw_tactic_arg = type t_trm = EConstr.constr type t_pat = constr_pattern -type t_cst = evaluable_global_reference +type t_cst = Tacred.evaluable_global_reference type t_ref = ltac_constant located type t_nam = Id.t diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 2382dcfbb9..3bb20b9d19 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -269,7 +269,7 @@ constraint 'a = < type g_trm = Genintern.glob_constr_and_expr type g_pat = Genintern.glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var +type g_cst = Tacred.evaluable_global_reference Genredexpr.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -323,7 +323,7 @@ type raw_tactic_arg = type t_trm = EConstr.constr type t_pat = constr_pattern -type t_cst = evaluable_global_reference +type t_cst = Tacred.evaluable_global_reference type t_ref = ltac_constant located type t_nam = Id.t diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 8bee7afa2c..ae7a10ce52 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -308,8 +308,8 @@ let short_name qid = else None let evalref_of_globref ?loc ?short = function - | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short) - | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short) + | GlobRef.ConstRef cst -> ArgArg (Tacred.EvalConstRef cst, short) + | GlobRef.VarRef id -> ArgArg (Tacred.EvalVarRef id, short) | r -> let tpe = match r with | GlobRef.IndRef _ -> "inductive" diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 90546ea939..6148f0d23f 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -89,7 +89,7 @@ let subst_global_reference subst = Locusops.or_var_map (subst_located (subst_global_reference subst)) let subst_evaluable subst = - let subst_eval_ref = subst_evaluable_reference subst in + let subst_eval_ref = Tacred.subst_evaluable_reference subst in Locusops.or_var_map (subst_and_short_name subst_eval_ref) let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index a7b571d3db..7d959aa788 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -189,6 +189,7 @@ let flatten_contravariant_disj _ ist = | _ -> fail let evalglobref_of_globref = + let open Tacred in function | GlobRef.VarRef v -> EvalVarRef v | GlobRef.ConstRef c -> EvalConstRef c diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4f7b3fbe74..9d92ffde74 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -354,8 +354,9 @@ let coq_True = gen_constant "core.True.type" let evaluable_ref_of_constr s c = let env = Global.env () in let evd = Evd.from_env env in + let open Tacred in match EConstr.kind evd (Lazy.force c) with - | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) -> + | Const (kn,u) when is_evaluable env (EvalConstRef kn) -> EvalConstRef kn | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant.")) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index fdfba48024..723c786b4f 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -223,11 +223,11 @@ let simplintac occ rdx sim = end let rec get_evalref env sigma c = match EConstr.kind sigma c with - | Var id -> EvalVarRef id - | Const (k,_) -> EvalConstRef k + | Var id -> Tacred.EvalVarRef id + | Const (k,_) -> Tacred.EvalConstRef k | App (c', _) -> get_evalref env sigma c' | Cast (c', _, _) -> get_evalref env sigma c' - | Proj(c,_) -> EvalConstRef(Projection.constant c) + | Proj(c,_) -> Tacred.EvalConstRef(Projection.constant c) | _ -> errorstrm Pp.(str "The term " ++ pr_econstr_pat (Global.env ()) sigma c ++ str " is not unfoldable") (* Strip a pattern generated by a prenex implicit to its constant. *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index c705ac16e7..411fb0cd89 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -43,6 +43,25 @@ exception ReductionTacticError of reduction_tactic_error exception Elimconst exception Redelimination +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +(* Better to have it here that in closure, since used in grammar.cma *) +let eq_egr e1 e2 = match e1, e2 with + EvalConstRef con1, EvalConstRef con2 -> Constant.CanOrd.equal con1 con2 + | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 + | _, _ -> false + +(* Here the semantics is completely unclear. + What does "Hint Unfold t" means when "t" is a parameter? + Does the user mean "Unfold X.t" or does she mean "Unfold y" + where X.t is later on instantiated with y? I choose the first + interpretation (i.e. an evaluable reference is never expanded). *) +let subst_evaluable_reference subst = function + | EvalVarRef id -> EvalVarRef id + | EvalConstRef kn -> EvalConstRef (Mod_subst.subst_constant subst kn) + let error_not_evaluable r = user_err ~hdr:"error_not_evaluable" (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 65e3421736..aa232175bb 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -18,6 +18,21 @@ open Locus open Univ open Ltac_pretype +(* XXX: Move to a module *) +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool + +(** Here the semantics is completely unclear. + What does "Hint Unfold t" means when "t" is a parameter? + Does the user mean "Unfold X.t" or does she mean "Unfold y" + where X.t is later on instantiated with y? I choose the first + interpretation (i.e. an evaluable reference is never expanded). *) +val subst_evaluable_reference : + Mod_subst.substitution -> evaluable_global_reference -> evaluable_global_reference + type reduction_tactic_error = InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) diff --git a/printing/printer.mli b/printing/printer.mli index 732af5570d..524c715455 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -154,7 +154,7 @@ val pr_existential_key : evar_map -> Evar.t -> Pp.t val pr_existential : env -> evar_map -> existential -> Pp.t val pr_constructor : env -> constructor -> Pp.t val pr_inductive : env -> inductive -> Pp.t -val pr_evaluable_reference : evaluable_global_reference -> Pp.t +val pr_evaluable_reference : Tacred.evaluable_global_reference -> Pp.t val pr_pconstant : env -> evar_map -> pconstant -> Pp.t val pr_pinductive : env -> evar_map -> pinductive -> Pp.t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 08f88d46c1..6a6dd783e4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -69,7 +69,7 @@ val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInst [@@ocaml.deprecated "Use Tacred.pf_reduce_to_atomic_ind"] val pf_compute : Goal.goal sigma -> constr -> constr [@@ocaml.deprecated "Use the version in Tacmach.New"] -val pf_unfoldn : (occurrences * evaluable_global_reference) list +val pf_unfoldn : (occurrences * Tacred.evaluable_global_reference) list -> Goal.goal sigma -> constr -> constr [@@ocaml.deprecated "Use Tacred.unfoldn"] diff --git a/tactics/auto.ml b/tactics/auto.ml index 369508c2a3..353e138599 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -277,8 +277,8 @@ let hintmap_of env sigma secvars hdc concl = else Hint_db.map_auto env sigma ~secvars hdc concl let exists_evaluable_reference env = function - | EvalConstRef _ -> true - | EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false + | Tacred.EvalConstRef _ -> true + | Tacred.EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false let dbg_intro dbg = tclLOG dbg (fun _ _ -> str "intro") intro let dbg_assumption dbg = tclLOG dbg (fun _ _ -> str "assumption") assumption diff --git a/tactics/eauto.ml b/tactics/eauto.ml index e920093648..20c557b282 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -386,6 +386,7 @@ let make_dimension n = function | Some d -> (false,d) let autounfolds ids csts gl cls = + let open Tacred in let hyps = Tacmach.New.pf_ids_of_hyps gl in let env = Tacmach.New.pf_env gl in let ids = List.filter (fun id -> List.mem id hyps && Tacred.is_evaluable env (EvalVarRef id)) ids in diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml index 9939490e79..a9100efddb 100644 --- a/tactics/genredexpr.ml +++ b/tactics/genredexpr.ml @@ -76,7 +76,7 @@ type 'a and_short_name = 'a * Names.lident option let wit_red_expr : ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, - (Genintern.glob_constr_and_expr,Names.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen, - (EConstr.t,Names.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen) + (Genintern.glob_constr_and_expr,Tacred.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen, + (EConstr.t,Tacred.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen) Genarg.genarg_type = make0 "redexpr" diff --git a/tactics/hints.mli b/tactics/hints.mli index 54f4716652..f5947bb946 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -36,7 +36,7 @@ type 'a hint_ast = | ERes_pf of 'a (* Hint EApply *) | Give_exact of 'a | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *) - | Unfold_nth of evaluable_global_reference (* Hint Unfold *) + | Unfold_nth of Tacred.evaluable_global_reference (* Hint Unfold *) | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *) type hint = private { @@ -173,8 +173,8 @@ type hints_entry = | HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list | HintsImmediateEntry of (hints_path_atom * hint_term) list | HintsCutEntry of hints_path - | HintsUnfoldEntry of evaluable_global_reference list - | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool + | HintsUnfoldEntry of Tacred.evaluable_global_reference list + | HintsTransparencyEntry of Tacred.evaluable_global_reference hints_transparency_target * bool | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index 9c2df71f82..b415b30de8 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -81,7 +81,7 @@ let subst_strategy (subs,(local,obj)) = local, List.Smart.map (fun (k,ql as entry) -> - let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in + let ql' = List.Smart.map (Tacred.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj @@ -344,7 +344,7 @@ let subst_red_expr subs = let sigma = Evd.from_env env in Redops.map_red_expr_gen (subst_mps subs) - (Mod_subst.subst_evaluable_reference subs) + (Tacred.subst_evaluable_reference subs) (Patternops.subst_pattern env sigma subs) let inReduction : bool * string * red_expr -> obj = diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli index 5f3a7b689b..fb0043db8d 100644 --- a/tactics/redexpr.mli +++ b/tactics/redexpr.mli @@ -10,7 +10,6 @@ (** Interpretation layer of redexprs such as hnf, cbv, etc. *) -open Names open Constr open EConstr open Pattern @@ -19,7 +18,7 @@ open Reductionops open Locus type red_expr = - (constr, evaluable_global_reference, constr_pattern) red_expr_gen + (constr, Tacred.evaluable_global_reference, constr_pattern) red_expr_gen type red_expr_val @@ -50,7 +49,7 @@ val declare_red_expr : bool -> string -> red_expr -> unit true, the effect is non-synchronous (i.e. it does not survive section and module closure). *) val set_strategy : - bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit + bool -> (Conv_oracle.level * Tacred.evaluable_global_reference list) list -> unit (** call by value normalisation function using the virtual machine *) val cbv_vm : reduction_function diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0fd2f1253f..a6471be549 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -179,11 +179,11 @@ val normalise_in_hyp : hyp_location -> unit Proofview.tactic val normalise_option : goal_location -> unit Proofview.tactic val normalise_vm_in_concl : unit Proofview.tactic val unfold_in_concl : - (occurrences * evaluable_global_reference) list -> unit Proofview.tactic + (occurrences * Tacred.evaluable_global_reference) list -> unit Proofview.tactic val unfold_in_hyp : - (occurrences * evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic + (occurrences * Tacred.evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic val unfold_option : - (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic + (occurrences * Tacred.evaluable_global_reference) list -> goal_location -> unit Proofview.tactic val change : check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic val pattern_option : diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml index 69758b3f37..54f5a2cf68 100644 --- a/user-contrib/Ltac2/tac2tactics.ml +++ b/user-contrib/Ltac2/tac2tactics.ml @@ -209,13 +209,13 @@ let letin_pat_tac ev ipat na c cl = Instead, we parse indifferently any pattern and dispatch when the tactic is called. *) let map_pattern_with_occs (pat, occ) = match pat with -| Pattern.PRef (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst)) -| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id)) +| Pattern.PRef (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (Tacred.EvalConstRef cst)) +| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (Tacred.EvalVarRef id)) | _ -> (mk_occurrences_expr occ, Inr pat) let get_evaluable_reference = function -| GlobRef.VarRef id -> Proofview.tclUNIT (EvalVarRef id) -| GlobRef.ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst) +| GlobRef.VarRef id -> Proofview.tclUNIT (Tacred.EvalVarRef id) +| GlobRef.ConstRef cst -> Proofview.tclUNIT (Tacred.EvalConstRef cst) | r -> Tacticals.New.tclZEROMSG (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ spc () ++ diff --git a/vernac/classes.mli b/vernac/classes.mli index e1816fb138..89ff4e6939 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -81,7 +81,7 @@ val add_class : env -> Evd.evar_map -> typeclass -> unit (** Setting opacity *) -val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit +val set_typeclass_transparency : Tacred.evaluable_global_reference -> bool -> bool -> unit (** For generation on names based on classes only *) diff --git a/vernac/comHints.ml b/vernac/comHints.ml index f642411fa4..1c36e10e83 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -76,6 +76,7 @@ let warn_deprecated_hint_constr = *) let soft_evaluable = let open GlobRef in + let open Tacred in function | ConstRef c -> EvalConstRef c | VarRef id -> EvalVarRef id diff --git a/vernac/declare.ml b/vernac/declare.ml index fafee13bf6..c715304419 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -883,7 +883,7 @@ let shrink_body c ty = (* Saving an obligation *) (***********************************************************************) -let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] +let unfold_entry cst = Hints.HintsUnfoldEntry [Tacred.EvalConstRef cst] let add_hint local prg cst = let locality = if local then Goptions.OptLocal else Goptions.OptExport in diff --git a/vernac/record.ml b/vernac/record.ml index 583164a524..68219603b4 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -625,7 +625,7 @@ let build_class_constant ~univs ~rdata field implfs params paramimpls coers bind let cref = GlobRef.ConstRef cst in Impargs.declare_manual_implicits false cref paramimpls; Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs); - Classes.set_typeclass_transparency (EvalConstRef cst) false false; + Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false; let sub = List.hd coers in let m = { meth_name = Name proj_name; @@ -744,7 +744,7 @@ let add_constant_class env sigma cst = } in Classes.add_class env sigma tc; - Classes.set_typeclass_transparency (EvalConstRef cst) false false + Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false let add_inductive_class env sigma ind = let mind, oneind = Inductive.lookup_mind_specif env ind in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a3726daf63..e8cb1d65a9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1628,6 +1628,7 @@ let () = } let vernac_set_strategy ~local l = + let open Tacred in let local = Option.default false local in let glob_ref r = match smart_global r with @@ -1639,6 +1640,7 @@ let vernac_set_strategy ~local l = Redexpr.set_strategy local l let vernac_set_opacity ~local (v,l) = + let open Tacred in let local = Option.default true local in let glob_ref r = match smart_global r with |