From 733cb74a2038ff92156b7209713fc2ea741ccca6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Mon, 19 Nov 2018 08:12:28 +0100 Subject: [PATCH] Rename TranspState into TransparentState. --- dev/doc/changes.md | 2 +- dev/top_printers.mli | 2 +- kernel/cClosure.ml | 12 ++-- kernel/cClosure.mli | 4 +- kernel/conv_oracle.ml | 2 +- kernel/conv_oracle.mli | 2 +- kernel/kernel.mllib | 2 +- kernel/reduction.ml | 8 +-- kernel/reduction.mli | 8 +-- .../{transpState.ml => transparentState.ml} | 0 .../{transpState.mli => transparentState.mli} | 0 kernel/vconv.ml | 4 +- plugins/firstorder/ground.ml | 4 +- .../funind/functional_principles_proofs.ml | 2 +- plugins/funind/recdef.ml | 2 +- plugins/ltac/rewrite.ml | 10 ++-- pretyping/cases.ml | 2 +- pretyping/evarconv.ml | 14 ++--- pretyping/evarconv.mli | 16 +++--- pretyping/reductionops.ml | 12 ++-- pretyping/reductionops.mli | 16 +++--- pretyping/typeclasses.mli | 4 +- pretyping/unification.ml | 56 +++++++++---------- pretyping/unification.mli | 8 +-- printing/printer.ml | 4 +- printing/printer.mli | 2 +- proofs/clenvtac.ml | 6 +- proofs/evar_refiner.ml | 2 +- proofs/redexpr.ml | 2 +- tactics/auto.ml | 10 ++-- tactics/auto.mli | 2 +- tactics/btermdn.ml | 10 ++-- tactics/btermdn.mli | 8 +-- tactics/class_tactics.ml | 12 ++-- tactics/class_tactics.mli | 4 +- tactics/eauto.ml | 6 +- tactics/equality.ml | 16 +++--- tactics/hints.ml | 26 ++++----- tactics/hints.mli | 10 ++-- tactics/tactics.ml | 8 +-- tactics/tactics.mli | 2 +- vernac/assumptions.ml | 2 +- vernac/assumptions.mli | 2 +- vernac/vernacentries.ml | 2 +- 44 files changed, 164 insertions(+), 164 deletions(-) rename kernel/{transpState.ml => transparentState.ml} (100%) rename kernel/{transpState.mli => transparentState.mli} (100%) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 9c5785758d50..30a2967259cc 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -19,7 +19,7 @@ Names Constant.make3 has been removed, use Constant.make2 Constant.repr3 has been removed, use Constant.repr2 -- `Names.transparent_state` has been moved to its own module `TranspState`. +- `Names.transparent_state` has been moved to its own module `TransparentState`. This module gathers utility functions that used to be defined in several places. diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 5876b7c5c637..eaa12ff702a4 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -101,7 +101,7 @@ val ppdelta : Mod_subst.delta_resolver -> unit val pp_idpred : Names.Id.Pred.t -> unit val pp_cpred : Names.Cpred.t -> unit -val pp_transparent_state : TranspState.t -> unit +val pp_transparent_state : TransparentState.t -> unit val pp_stack_t : Constr.t Reductionops.Stack.t -> unit val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 625a9a7277d3..7e73609996bf 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -72,8 +72,8 @@ let with_stats c = end else Lazy.force c -let all_opaque = TranspState.empty -let all_transparent = TranspState.full +let all_opaque = TransparentState.empty +let all_transparent = TransparentState.full module type RedFlagsSig = sig type reds @@ -90,8 +90,8 @@ module type RedFlagsSig = sig val no_red : reds val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds - val red_add_transparent : reds -> TranspState.t -> reds - val red_transparent : reds -> TranspState.t + val red_add_transparent : reds -> TransparentState.t -> reds + val red_transparent : reds -> TransparentState.t val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> Projection.t -> bool @@ -103,13 +103,13 @@ module RedFlags = (struct (* [r_const=(false,cl)] means only those in [cl] *) (* [r_delta=true] just mean [r_const=(true,[])] *) - open TranspState + open TransparentState type reds = { r_beta : bool; r_delta : bool; r_eta : bool; - r_const : TranspState.t; + r_const : TransparentState.t; r_zeta : bool; r_match : bool; r_fix : bool; diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 26710a64d00d..b6c87b37325c 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -52,10 +52,10 @@ module type RedFlagsSig = sig val red_sub : reds -> red_kind -> reds (** Adds a reduction kind to a set *) - val red_add_transparent : reds -> TranspState.t -> reds + val red_add_transparent : reds -> TransparentState.t -> reds (** Retrieve the transparent state of the reduction flags *) - val red_transparent : reds -> TranspState.t + val red_transparent : reds -> TransparentState.t (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index c66beb49b889..fe82353b7037 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -82,7 +82,7 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu = Cmap.fold fcst cst_opacity accu let get_transp_state { var_trstate; cst_trstate; _ } = - { TranspState.tr_var = var_trstate; tr_cst = cst_trstate } + { TransparentState.tr_var = var_trstate; tr_cst = cst_trstate } let dep_order l2r k1 k2 = match k1, k2 with | RelKey _, RelKey _ -> l2r diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 3b5151535235..bc06cc21b62c 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -41,5 +41,5 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle (** Fold over the non-transparent levels of the oracle. Order unspecified. *) val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a -val get_transp_state : oracle -> TranspState.t +val get_transp_state : oracle -> TransparentState.t diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index e716972ebeb3..54c239349d7b 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,5 +1,5 @@ Names -TranspState +TransparentState Uint31 Univ UGraph diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a45a5b3247e6..fbb481424fb4 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -177,7 +177,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit (* functions of this type can be called from outside the kernel *) type 'a extended_conversion_function = - ?l2r:bool -> ?reds:TranspState.t -> env -> + ?l2r:bool -> ?reds:TransparentState.t -> env -> ?evars:((existential->constr option) * UGraph.t) -> 'a -> 'a -> unit @@ -758,7 +758,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = () (* Profiling *) -let gen_conv cv_pb ?(l2r=false) ?(reds=TranspState.full) env ?(evars=(fun _->None), universes env) = +let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in @@ -792,11 +792,11 @@ let infer_conv_universes = CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes -let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full) +let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) env univs t1 t2 = infer_conv_universes CONV l2r evars ts env univs t1 t2 -let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full) +let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9b26e7b3dcd8..0408dbf05705 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -31,7 +31,7 @@ exception NotConvertibleVect of int type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = - ?l2r:bool -> ?reds:TranspState.t -> env -> + ?l2r:bool -> ?reds:TransparentState.t -> env -> ?evars:((existential->constr option) * UGraph.t) -> 'a -> 'a -> unit @@ -77,15 +77,15 @@ val conv_leq : types extended_conversion_function (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:TranspState.t -> constr infer_conversion_function + ?ts:TransparentState.t -> constr infer_conversion_function val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:TranspState.t -> types infer_conversion_function + ?ts:TransparentState.t -> types infer_conversion_function (** Depending on the universe state functions, this might raise [UniverseInconsistency] in addition to [NotConvertible] (for better error messages). *) val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> - TranspState.t -> (constr,'a) generic_conversion_function + TransparentState.t -> (constr,'a) generic_conversion_function val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function val default_conv_leq : ?l2r:bool -> types kernel_conversion_function diff --git a/kernel/transpState.ml b/kernel/transparentState.ml similarity index 100% rename from kernel/transpState.ml rename to kernel/transparentState.ml diff --git a/kernel/transpState.mli b/kernel/transparentState.mli similarity index 100% rename from kernel/transpState.mli rename to kernel/transparentState.mli diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 46e52121c76e..246c90c09d1b 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -191,7 +191,7 @@ let warn_bytecode_compiler_failed = let vm_conv_gen cv_pb env univs t1 t2 = if not (typing_flags env).Declarations.enable_VM then Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - TranspState.full env univs t1 t2 + TransparentState.full env univs t1 t2 else try let v1 = val_of_constr env t1 in @@ -200,7 +200,7 @@ let vm_conv_gen cv_pb env univs t1 t2 = with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - TranspState.full env univs t1 t2 + TransparentState.full env univs t1 t2 let vm_conv cv_pb env t1 t2 = let univs = Environ.universes env in diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 820dd9704387..6a8052520008 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -18,12 +18,12 @@ open Tacticals.New open Globnames let update_flags ()= - let open TranspState in + let open TransparentState in let f accu coe = match coe.Classops.coe_value with | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst } | _ -> accu in - let flags = List.fold_left f TranspState.full (Classops.coercions ()) in + let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in red_flags:= CClosure.RedFlags.red_add_transparent CClosure.betaiotazeta diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e81335037a30..92fa94d6dcdb 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1487,7 +1487,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = Eauto.eauto_with_bases (true,5) [(fun _ sigma -> (sigma, Lazy.force refl_equal))] - [Hints.Hint_db.empty TranspState.empty false] + [Hints.Hint_db.empty TransparentState.empty false] ) ) ) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 84c5b4fbe4af..6e5e3f935341 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1359,7 +1359,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp Eauto.eauto_with_bases (true,5) [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))] - [Hints.Hint_db.empty TranspState.empty false] + [Hints.Hint_db.empty TransparentState.empty false] ] ) ) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index d66184227e43..4142fb2412fb 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -528,7 +528,7 @@ let decompose_applied_relation env sigma (c,l) = let rewrite_db = "rewrite" -let conv_transparent_state = TranspState.cst_full +let conv_transparent_state = TransparentState.cst_full let rewrite_transparent_state () = Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db) @@ -537,8 +537,8 @@ let rewrite_core_unif_flags = { Unification.modulo_conv_on_closed_terms = None; Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.use_evars_eagerly_in_conv_on_closed_terms = true; - Unification.modulo_delta = TranspState.empty; - Unification.modulo_delta_types = TranspState.full; + Unification.modulo_delta = TransparentState.empty; + Unification.modulo_delta_types = TransparentState.full; Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; @@ -585,12 +585,12 @@ let general_rewrite_unif_flags () = Unification.modulo_conv_on_closed_terms = Some ts; Unification.use_evars_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; - Unification.modulo_delta_types = TranspState.full; + Unification.modulo_delta_types = TransparentState.full; Unification.modulo_betaiota = true } in { Unification.core_unify_flags = core_flags; Unification.merge_unify_flags = core_flags; - Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = TranspState.empty }; + Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = TransparentState.empty }; Unification.allow_K_in_toplevel_higher_order_unification = true; Unification.resolve_evars = true } diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 647ef5092f19..e02fb332767d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1698,7 +1698,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context !!env) in let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in - begin match solve_simple_eqn (evar_conv_x TranspState.full) !!env sigma (None,ev,substl inst ev') with + begin match solve_simple_eqn (evar_conv_x TransparentState.full) !!env sigma (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false end; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0c9ad5d09445..f370ad7ae236 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -29,7 +29,7 @@ open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -type unify_fun = TranspState.t -> +type unify_fun = TransparentState.t -> env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result let debug_unification = ref (false) @@ -73,14 +73,14 @@ let coq_unit_judge = let unfold_projection env evd ts p c = let cst = Projection.constant p in - if TranspState.is_transparent_constant ts cst then + if TransparentState.is_transparent_constant ts cst then Some (mkProj (Projection.unfold p, c)) else None let eval_flexible_term ts env evd c = match EConstr.kind evd c with | Const (c, u) -> - if TranspState.is_transparent_constant ts c + if TransparentState.is_transparent_constant ts c then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u)) else None | Rel n -> @@ -90,7 +90,7 @@ let eval_flexible_term ts env evd c = with Not_found -> None) | Var id -> (try - if TranspState.is_transparent_variable ts id then + if TransparentState.is_transparent_variable ts id then env |> lookup_named id |> NamedDecl.get_value else None with Not_found -> None) @@ -1210,7 +1210,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | [] -> let evd = try Evarsolve.check_evar_instance evd evk rhs - (evar_conv_x TranspState.full) + (evar_conv_x TransparentState.full) with IllTypedInstance _ -> raise (TypingFailed evd) in Evd.define evk rhs evd @@ -1353,7 +1353,7 @@ let solve_unconstrained_impossible_cases env evd = let j, ctx = coq_unit_judge env in let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in - let conv_algo = evar_conv_x TranspState.full in + let conv_algo = evar_conv_x TransparentState.full in let evd' = check_evar_instance evd' evk ty conv_algo in Evd.define evk ty evd' | _ -> evd') evd evd @@ -1392,7 +1392,7 @@ let solve_unif_constraints_with_heuristics env exception UnableToUnify of evar_map * unification_error -let default_transparent_state env = TranspState.full +let default_transparent_state env = TransparentState.full (* Conv_oracle.get_transp_state (Environ.oracle env) *) let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd = diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 721a6fad8e2e..4585fac25244 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -21,20 +21,20 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error (** {6 Main unification algorithm for type inference. } *) (** returns exception NotUnifiable with best known evar_map if not unifiable *) -val the_conv_x : env -> ?ts:TranspState.t -> constr -> constr -> evar_map -> evar_map -val the_conv_x_leq : env -> ?ts:TranspState.t -> constr -> constr -> evar_map -> evar_map +val the_conv_x : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map +val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map (** The same function resolving evars by side-effect and catching the exception *) -val conv : env -> ?ts:TranspState.t -> evar_map -> constr -> constr -> evar_map option -val cumul : env -> ?ts:TranspState.t -> evar_map -> constr -> constr -> evar_map option +val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option +val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option (** {6 Unification heuristics. } *) (** Try heuristics to solve pending unification problems and to solve evars with candidates *) -val solve_unif_constraints_with_heuristics : env -> ?ts:TranspState.t -> evar_map -> evar_map +val solve_unif_constraints_with_heuristics : env -> ?ts:TransparentState.t -> evar_map -> evar_map (** Check all pending unification problems are solved and raise an error otherwise *) @@ -54,14 +54,14 @@ val check_conv_record : env -> evar_map -> (** Try to solve problems of the form ?x[args] = c by second-order matching, using typing to select occurrences *) -val second_order_matching : TranspState.t -> env -> evar_map -> +val second_order_matching : TransparentState.t -> env -> evar_map -> EConstr.existential -> occurrences option list -> constr -> evar_map * bool (** Declare function to enforce evars resolution by using typing constraints *) val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit -type unify_fun = TranspState.t -> +type unify_fun = TransparentState.t -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result (** Override default [evar_conv_x] algorithm. *) @@ -72,7 +72,7 @@ val evar_conv_x : unify_fun (**/**) (* For debugging *) -val evar_eqappr_x : ?rhs_is_already_stuck:bool -> TranspState.t * bool -> +val evar_eqappr_x : ?rhs_is_already_stuck:bool -> TransparentState.t * bool -> env -> evar_map -> conv_pb -> state * Cst_stack.t -> state * Cst_stack.t -> Evarsolve.unification_result diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4fbbf20c1f81..e632976ae50b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1301,13 +1301,13 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_conv ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv reds env sigma -let is_conv_leq ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma -let is_fconv ?(reds=TranspState.full) = function +let is_conv ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv reds env sigma +let is_conv_leq ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma +let is_fconv ?(reds=TransparentState.full) = function | Reduction.CONV -> is_conv ~reds | Reduction.CUMUL -> is_conv_leq ~reds -let check_conv ?(pb=Reduction.CUMUL) ?(ts=TranspState.full) env sigma x y = +let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y = let f = match pb with | Reduction.CONV -> f_conv | Reduction.CUMUL -> f_conv_leq @@ -1341,7 +1341,7 @@ let sigma_univ_state = compare_cumul_instances = sigma_check_inductive_instances; } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) - ?(ts=TranspState.full) env sigma x y = + ?(ts=TransparentState.full) env sigma x y = (** FIXME *) try let ans = match pb with @@ -1374,7 +1374,7 @@ let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> Reduction.generic_conv pb ~l2r (safe_evar_value sigma)) (* This reference avoids always having to link C code with the kernel *) -let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:TranspState.full) +let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:TransparentState.full) let set_vm_infer_conv f = vm_infer_conv := f let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = !vm_infer_conv ~pb env t1 t2 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 749e23bde289..088e898a9976 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -266,21 +266,21 @@ type conversion_test = Constraint.t -> Constraint.t val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val is_conv : ?reds:TranspState.t -> env -> evar_map -> constr -> constr -> bool -val is_conv_leq : ?reds:TranspState.t -> env -> evar_map -> constr -> constr -> bool -val is_fconv : ?reds:TranspState.t -> conv_pb -> env -> evar_map -> constr -> constr -> bool +val is_conv : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr -> bool +val is_conv_leq : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr -> bool +val is_fconv : ?reds:TransparentState.t -> conv_pb -> env -> evar_map -> constr -> constr -> bool (** [check_conv] Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state. *) -val check_conv : ?pb:conv_pb -> ?ts:TranspState.t -> env -> evar_map -> constr -> constr -> bool +val check_conv : ?pb:conv_pb -> ?ts:TransparentState.t -> env -> evar_map -> constr -> constr -> bool (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. @raise UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. *) -val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TranspState.t -> +val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env -> evar_map -> constr -> constr -> evar_map option (** Conversion with inference of universe constraints *) @@ -292,9 +292,9 @@ val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a conversion function. Used to pretype vm and native casts. *) -val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TranspState.t -> +val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t -> (Constr.constr, evar_map) Reduction.generic_conversion_function) -> - ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TranspState.t -> env -> + ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env -> evar_map -> constr -> constr -> evar_map option (** {6 Special-Purpose Reduction Functions } *) @@ -307,7 +307,7 @@ val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr (** {6 Heuristic for Conversion with Evar } *) val whd_betaiota_deltazeta_for_iota_state : - TranspState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> + TransparentState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> state * Cst_stack.t (** {6 Meta-related reduction functions } *) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index c6a58fc1e9a3..8bdac0a575c7 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -119,8 +119,8 @@ val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit -val classes_transparent_state_hook : (unit -> TranspState.t) Hook.t -val classes_transparent_state : unit -> TranspState.t +val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t +val classes_transparent_state : unit -> TransparentState.t val add_instance_hint_hook : (global_reference_or_constr -> GlobRef.t list -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 99b8d8e92abe..490d58fa5226 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -149,7 +149,7 @@ let abstract_list_all_with_dependencies env evd typ c l = let n = List.length l in let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in let evd,b = - Evarconv.second_order_matching TranspState.empty + Evarconv.second_order_matching TransparentState.empty env evd ev' argoccs c in if b then let p = nf_evar evd ev in @@ -247,7 +247,7 @@ let sort_eqns = unify_r2l *) type core_unify_flags = { - modulo_conv_on_closed_terms : TranspState.t option; + modulo_conv_on_closed_terms : TransparentState.t option; (* What this flag controls was activated with all constants transparent, *) (* even for auto, since Coq V5.10 *) @@ -257,11 +257,11 @@ type core_unify_flags = { use_evars_eagerly_in_conv_on_closed_terms : bool; - modulo_delta : TranspState.t; + modulo_delta : TransparentState.t; (* This controls which constants are unfoldable; this is on for apply *) (* (but not simple apply) since Feb 2008 for 8.2 *) - modulo_delta_types : TranspState.t; + modulo_delta_types : TransparentState.t; check_applied_meta_types : bool; (* This controls whether meta's applied to arguments have their *) @@ -322,7 +322,7 @@ type unify_flags = { (* Default flag for unifying a type against a type (e.g. apply) *) (* We set all conversion flags (no flag should be modified anymore) *) let default_core_unify_flags () = - let ts = TranspState.full in { + let ts = TransparentState.full in { modulo_conv_on_closed_terms = Some ts; use_metas_eagerly_in_conv_on_closed_terms = true; use_evars_eagerly_in_conv_on_closed_terms = false; @@ -344,14 +344,14 @@ let default_unify_flags () = let flags = default_core_unify_flags () in { core_unify_flags = flags; merge_unify_flags = flags; - subterm_unify_flags = { flags with modulo_delta = TranspState.var_full }; + subterm_unify_flags = { flags with modulo_delta = TransparentState.var_full }; allow_K_in_toplevel_higher_order_unification = false; (* Why not? *) resolve_evars = false } let set_no_delta_core_flags flags = { flags with modulo_conv_on_closed_terms = None; - modulo_delta = TranspState.empty; + modulo_delta = TransparentState.empty; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; @@ -370,7 +370,7 @@ let set_no_delta_flags flags = { (* For the first phase of keyed unification, restrict to conversion (including beta-iota) only on closed terms *) let set_no_delta_open_core_flags flags = { flags with - modulo_delta = TranspState.empty; + modulo_delta = TransparentState.empty; modulo_betaiota = false; } @@ -388,7 +388,7 @@ let set_no_delta_open_flags flags = { (* We set only the flags available at the time the new "apply" extended *) (* out of "simple apply" *) let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with - modulo_delta = TranspState.empty; + modulo_delta = TransparentState.empty; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; @@ -425,7 +425,7 @@ let elim_flags_evars sigma = let flags = elim_core_flags sigma in { core_unify_flags = flags; merge_unify_flags = flags; - subterm_unify_flags = { flags with modulo_delta = TranspState.empty }; + subterm_unify_flags = { flags with modulo_delta = TransparentState.empty }; allow_K_in_toplevel_higher_order_unification = true; resolve_evars = false } @@ -433,7 +433,7 @@ let elim_flags_evars sigma = let elim_flags () = elim_flags_evars Evd.empty let elim_no_delta_core_flags () = { (elim_core_flags Evd.empty) with - modulo_delta = TranspState.empty; + modulo_delta = TransparentState.empty; check_applied_meta_types = false; use_pattern_unification = false; modulo_betaiota = false; @@ -504,16 +504,16 @@ let key_of env sigma b flags f = if subterm_restriction b flags then None else match EConstr.kind sigma f with | Const (cst, u) when is_transparent env (ConstKey cst) && - (TranspState.is_transparent_constant flags.modulo_delta cst + (TransparentState.is_transparent_constant flags.modulo_delta cst || Recordops.is_primitive_projection cst) -> let u = EInstance.kind sigma u in Some (IsKey (ConstKey (cst, u))) | Var id when is_transparent env (VarKey id) && - TranspState.is_transparent_variable flags.modulo_delta id -> + TransparentState.is_transparent_variable flags.modulo_delta id -> Some (IsKey (VarKey id)) | Proj (p, c) when Projection.unfolded p || (is_transparent env (ConstKey (Projection.constant p)) && - (TranspState.is_transparent_constant flags.modulo_delta (Projection.constant p))) -> + (TransparentState.is_transparent_constant flags.modulo_delta (Projection.constant p))) -> Some (IsProj (p, c)) | _ -> None @@ -550,7 +550,7 @@ let oracle_order env cf1 cf2 = let is_rigid_head sigma flags t = match EConstr.kind sigma t with - | Const (cst,u) -> not (TranspState.is_transparent_constant flags.modulo_delta cst) + | Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst) | Ind (i,u) -> true | Construct _ -> true | Fix _ | CoFix _ -> true @@ -633,11 +633,11 @@ let rec is_neutral env sigma ts t = | Const (c, u) -> not (Environ.evaluable_constant c env) || not (is_transparent env (ConstKey c)) || - not (TranspState.is_transparent_constant ts c) + not (TransparentState.is_transparent_constant ts c) | Var id -> not (Environ.evaluable_named id env) || not (is_transparent env (VarKey id)) || - not (TranspState.is_transparent_variable ts id) + not (TransparentState.is_transparent_variable ts id) | Rel n -> true | Evar _ | Meta _ -> true | Case (_, p, c, cl) -> is_neutral env sigma ts c @@ -935,8 +935,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let ty1 = get_type_of curenv ~lax:true sigma c1 in let ty2 = get_type_of curenv ~lax:true sigma c2 in unify_0_with_initial_metas substn true curenv cv_pb - { flags with modulo_conv_on_closed_terms = Some TranspState.full; - modulo_delta = TranspState.full; + { flags with modulo_conv_on_closed_terms = Some TransparentState.full; + modulo_delta = TransparentState.full; modulo_eta = true; modulo_betaiota = true } ty1 ty2 @@ -1121,9 +1121,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | None -> if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some cv, dl -> - let open TranspState in + let open TransparentState in Id.Pred.subset dl.tr_var cv.tr_var && Cpred.subset dl.tr_cst cv.tr_cst - | None, dl -> TranspState.is_empty dl) + | None, dl -> TransparentState.is_empty dl) then error_cannot_unify env sigma (m, n) else None in let a = match res with @@ -1263,8 +1263,8 @@ let applyHead env evd n c = let is_mimick_head sigma ts f = match EConstr.kind sigma f with - | Const (c,u) -> not (TranspState.is_transparent_constant ts c) - | Var id -> not (TranspState.is_transparent_variable ts id) + | Const (c,u) -> not (TransparentState.is_transparent_constant ts c) + | Var id -> not (TransparentState.is_transparent_variable ts id) | (Rel _|Construct _|Ind _) -> true | _ -> false @@ -1534,11 +1534,11 @@ let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sig (sigma, nf_evar sigma c) let default_matching_core_flags sigma = - let ts = TranspState.full in { - modulo_conv_on_closed_terms = Some TranspState.empty; + let ts = TransparentState.full in { + modulo_conv_on_closed_terms = Some TransparentState.empty; use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; - modulo_delta = TranspState.empty; + modulo_delta = TransparentState.empty; modulo_delta_types = ts; check_applied_meta_types = true; use_pattern_unification = false; @@ -1550,7 +1550,7 @@ let default_matching_core_flags sigma = } let default_matching_merge_flags sigma = - let ts = TranspState.full in + let ts = TransparentState.full in let flags = default_matching_core_flags sigma in { flags with modulo_conv_on_closed_terms = Some ts; @@ -1580,7 +1580,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = if from_prefix_of_ind then let flags = default_matching_flags pending in { flags with core_unify_flags = { flags.core_unify_flags with - modulo_conv_on_closed_terms = Some TranspState.full; + modulo_conv_on_closed_terms = Some TransparentState.full; restrict_conv_on_strict_subterms = true } } else default_matching_flags pending in let n = Array.length (snd (decompose_app_vect sigma c)) in diff --git a/pretyping/unification.mli b/pretyping/unification.mli index b7b525c9fcbd..a45b8f1dd8b3 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -14,11 +14,11 @@ open Environ open Evd type core_unify_flags = { - modulo_conv_on_closed_terms : TranspState.t option; + modulo_conv_on_closed_terms : TransparentState.t option; use_metas_eagerly_in_conv_on_closed_terms : bool; use_evars_eagerly_in_conv_on_closed_terms : bool; - modulo_delta : TranspState.t; - modulo_delta_types : TranspState.t; + modulo_delta : TransparentState.t; + modulo_delta_types : TransparentState.t; check_applied_meta_types : bool; use_pattern_unification : bool; use_meta_bound_pattern_unification : bool; @@ -40,7 +40,7 @@ val default_core_unify_flags : unit -> core_unify_flags val default_no_delta_core_unify_flags : unit -> core_unify_flags val default_unify_flags : unit -> unify_flags -val default_no_delta_unify_flags : TranspState.t -> unify_flags +val default_no_delta_unify_flags : TransparentState.t -> unify_flags val elim_flags : unit -> unify_flags val elim_no_delta_flags : unit -> unify_flags diff --git a/printing/printer.ml b/printing/printer.ml index b7c53c551395..dfe987a6714f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -446,8 +446,8 @@ let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p) let pr_transparent_state ts = - hv 0 (str"VARIABLES: " ++ pr_idpred ts.TranspState.tr_var ++ fnl () ++ - str"CONSTANTS: " ++ pr_cpred ts.TranspState.tr_cst ++ fnl ()) + hv 0 (str"VARIABLES: " ++ pr_idpred ts.TransparentState.tr_var ++ fnl () ++ + str"CONSTANTS: " ++ pr_cpred ts.TransparentState.tr_cst ++ fnl ()) (* display complete goal og_s has goal+sigma on the previous proof step for diffs diff --git a/printing/printer.mli b/printing/printer.mli index fb4e790c10af..cfa1caef00cc 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -134,7 +134,7 @@ val pr_context_of : env -> evar_map -> Pp.t val pr_predicate : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t val pr_cpred : Cpred.t -> Pp.t val pr_idpred : Id.Pred.t -> Pp.t -val pr_transparent_state : TranspState.t -> Pp.t +val pr_transparent_state : TransparentState.t -> Pp.t (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ac3f52c6efc8..c7703b52c7bd 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -101,11 +101,11 @@ let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) let fail_quick_core_unif_flags = { - modulo_conv_on_closed_terms = Some TranspState.full; + modulo_conv_on_closed_terms = Some TransparentState.full; use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; - modulo_delta = TranspState.empty; - modulo_delta_types = TranspState.full; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.full; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index fb42a9cebeeb..6c4193c66b94 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -37,7 +37,7 @@ let define_and_solve_constraints evk c env evd = match List.fold_left (fun p (pbty,env,t1,t2) -> match p with - | Success evd -> Evarconv.evar_conv_x TranspState.full env evd pbty t1 t2 + | Success evd -> Evarconv.evar_conv_x TransparentState.full env evd pbty t1 t2 | UnifFailure _ as x -> x) (Success evd) pbs with diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 1aaf762e3144..0981584bb5fc 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -160,7 +160,7 @@ let make_flag env f = (fun v red -> red_sub red (make_flag_constant v)) f.rConst red else (* Only rConst *) - let red = red_add_transparent (red_add red fDELTA) TranspState.empty in + let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in List.fold_right (fun v red -> red_add red (make_flag_constant v)) f.rConst red diff --git a/tactics/auto.ml b/tactics/auto.ml index a23a085db540..81e487b77d6c 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -45,7 +45,7 @@ let auto_core_unif_flags_of st1 st2 = { use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; - modulo_delta_types = TranspState.full; + modulo_delta_types = TransparentState.full; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; @@ -59,13 +59,13 @@ let auto_unif_flags_of st1 st2 = let flags = auto_core_unif_flags_of st1 st2 in { core_unify_flags = flags; merge_unify_flags = flags; - subterm_unify_flags = { flags with modulo_delta = TranspState.empty }; + subterm_unify_flags = { flags with modulo_delta = TransparentState.empty }; allow_K_in_toplevel_higher_order_unification = false; resolve_evars = true } let auto_unif_flags = - auto_unif_flags_of TranspState.full TranspState.empty + auto_unif_flags_of TransparentState.full TransparentState.empty (* Try unification with the precompiled clause, then use registered Apply *) @@ -291,7 +291,7 @@ let flags_of_state st = auto_unif_flags_of st st let auto_flags_of_state st = - auto_unif_flags_of TranspState.full st + auto_unif_flags_of TransparentState.full st let hintmap_of sigma secvars hdc concl = match hdc with @@ -363,7 +363,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = let l = match hdc with None -> Hint_db.map_none ~secvars db | Some hdc -> - if TranspState.is_empty st + if TransparentState.is_empty st then Hint_db.map_auto sigma ~secvars hdc concl db else Hint_db.map_existential sigma ~secvars hdc concl db in auto_flags_of_state st, l diff --git a/tactics/auto.mli b/tactics/auto.mli index c7acbd4bfb70..72d2292ffb8c 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -22,7 +22,7 @@ val compute_secvars : Proofview.Goal.t -> Id.Pred.t val default_search_depth : int ref -val auto_flags_of_state : TranspState.t -> Unification.unify_flags +val auto_flags_of_state : TransparentState.t -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 04fe6a9fa7e9..2f2bd8d2bc78 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -72,10 +72,10 @@ let constr_pat_discr t = let constr_val_discr_st sigma ts t = let c, l = decomp sigma t in match EConstr.kind sigma c with - | Const (c,u) -> if TranspState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l) + | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l) | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id when not (TranspState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l) + | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l) | Prod (n, d, c) -> Label(ProdLabel, [d; c]) | Lambda (n, d, c) -> if List.is_empty l then @@ -89,11 +89,11 @@ let constr_pat_discr_st ts t = match decomp_pat t with | PRef ((IndRef _) as ref), args | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) - | PRef ((VarRef v) as ref), args when not (TranspState.is_transparent_variable ts v) -> + | PRef ((VarRef v) as ref), args when not (TransparentState.is_transparent_variable ts v) -> Some(GRLabel ref,args) - | PVar v, args when not (TranspState.is_transparent_variable ts v) -> + | PVar v, args when not (TransparentState.is_transparent_variable ts v) -> Some(GRLabel (VarRef v),args) - | PRef ((ConstRef c) as ref), args when not (TranspState.is_transparent_constant ts c) -> + | PRef ((ConstRef c) as ref), args when not (TransparentState.is_transparent_constant ts c) -> Some (GRLabel ref, args) | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) | PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c]) diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 6af5012def07..cc31fb0599ae 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -18,7 +18,7 @@ open Pattern order in such a way patterns having the same prefix have this common prefix shared and the seek for the action associated to the patterns that a term matches are found in time proportional to the maximal -number of nodes of the patterns matching the term. The [TranspState.t] +number of nodes of the patterns matching the term. The [TransparentState.t] indicates which constants and variables can be considered as rigid. These dnets are able to cope with existential variables as well, which match [Everything]. *) @@ -30,10 +30,10 @@ sig val empty : t - val add : TranspState.t option -> t -> (constr_pattern * Z.t) -> t - val rmv : TranspState.t option -> t -> (constr_pattern * Z.t) -> t + val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t + val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t - val lookup : Evd.evar_map -> TranspState.t option -> t -> EConstr.constr -> Z.t list + val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list val app : (Z.t -> unit) -> t -> unit end diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index f27e5e281acd..1bb33f2a238e 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -585,9 +585,9 @@ module Search = struct (** Local hints *) let autogoal_cache = Summary.ref ~name:"autogoal_cache" (DirPath.empty, true, Context.Named.empty, - Hint_db.empty TranspState.full true) + Hint_db.empty TransparentState.full true) - let make_autogoal_hints only_classes ?(st=TranspState.full) g = + let make_autogoal_hints only_classes ?(st=TransparentState.full) g = let open Proofview in let open Tacmach.New in let sign = Goal.hyps g in @@ -605,7 +605,7 @@ module Search = struct in autogoal_cache := (cwd, only_classes, sign, hints); hints - let make_autogoal ?(st=TranspState.full) only_classes dep cut i g = + let make_autogoal ?(st=TransparentState.full) only_classes dep cut i g = let hints = make_autogoal_hints only_classes ~st g in { search_hints = hints; search_depth = [i]; last_tac = lazy (str"none"); @@ -843,7 +843,7 @@ module Search = struct let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in search_tac hints depth 1 info - let search_tac ?(st=TranspState.full) only_classes dep hints depth = + let search_tac ?(st=TransparentState.full) only_classes dep hints depth = let open Proofview in let tac sigma gls i = Goal.enter @@ -873,7 +873,7 @@ module Search = struct | (e,ie) -> Proofview.tclZERO ~info:ie e) in aux 1 - let eauto_tac ?(st=TranspState.full) ?(unique=false) + let eauto_tac ?(st=TransparentState.full) ?(unique=false) ~only_classes ?strategy ~depth ~dep hints = let open Proofview in let tac = @@ -985,7 +985,7 @@ end (** Binding to either V85 or Search implementations. *) -let typeclasses_eauto ?(only_classes=false) ?(st=TranspState.full) +let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full) ?strategy ~depth dbs = let dbs = List.map_filter (fun db -> try Some (searchtable_map db) diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 9e2b0d26b5a9..46dff34f8991 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -25,7 +25,7 @@ type search_strategy = Dfs | Bfs val set_typeclasses_strategy : search_strategy -> unit -val typeclasses_eauto : ?only_classes:bool -> ?st:TranspState.t -> ?strategy:search_strategy -> +val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.t -> ?strategy:search_strategy -> depth:(Int.t option) -> Hints.hint_db_name list -> unit Proofview.tactic @@ -39,7 +39,7 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic module Search : sig val eauto_tac : - ?st:TranspState.t -> + ?st:TransparentState.t -> (** The transparent_state used when working with local hypotheses *) ?unique:bool -> (** Should we force a unique solution *) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index c18b7bb21436..9a6bdab7b992 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -29,7 +29,7 @@ open Locusops open Hints open Proofview.Notations -let eauto_unif_flags = auto_flags_of_state TranspState.full +let eauto_unif_flags = auto_flags_of_state TransparentState.full let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter begin fun gl -> @@ -307,7 +307,7 @@ module SearchProblem = struct let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in let hyps' = pf_hyps gls in if hyps' == hyps then List.hd s.localdb - else make_local_hint_db (pf_env gls) (project gls) ~ts:TranspState.full true s.local_lemmas) + else make_local_hint_db (pf_env gls) (project gls) ~ts:TransparentState.full true s.local_lemmas) (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) in { depth = pred s.depth; priority = cost; tacres = lgls; @@ -388,7 +388,7 @@ let make_initial_state dbg n gl dblist localdb lems = } let e_search_auto debug (in_depth,p) lems db_list gl = - let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TranspState.full true lems in + let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TransparentState.full true lems in let d = mk_eauto_dbg debug in let tac = match in_depth,d with | (true,Debug) -> Search.debug_depth_first diff --git a/tactics/equality.ml b/tactics/equality.ml index 8377cd5c753e..969f539d1f1b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -101,8 +101,8 @@ let rewrite_core_unif_flags = { modulo_conv_on_closed_terms = None; use_metas_eagerly_in_conv_on_closed_terms = true; use_evars_eagerly_in_conv_on_closed_terms = false; - modulo_delta = TranspState.empty; - modulo_delta_types = TranspState.empty; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.empty; check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; @@ -169,7 +169,7 @@ let instantiate_lemma gl c ty l l2r concl = [eqclause] let rewrite_conv_closed_core_unif_flags = { - modulo_conv_on_closed_terms = Some TranspState.full; + modulo_conv_on_closed_terms = Some TransparentState.full; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -178,8 +178,8 @@ let rewrite_conv_closed_core_unif_flags = { (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) - modulo_delta = TranspState.empty; - modulo_delta_types = TranspState.full; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.full; check_applied_meta_types = true; use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) @@ -204,7 +204,7 @@ let rewrite_conv_closed_unif_flags = { } let rewrite_keyed_core_unif_flags = { - modulo_conv_on_closed_terms = Some TranspState.full; + modulo_conv_on_closed_terms = Some TransparentState.full; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -213,8 +213,8 @@ let rewrite_keyed_core_unif_flags = { (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) - modulo_delta = TranspState.full; - modulo_delta_types = TranspState.full; + modulo_delta = TransparentState.full; + modulo_delta_types = TransparentState.full; check_applied_meta_types = true; use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 287e289c2f99..6aa021543d33 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -291,8 +291,8 @@ let lookup_tacs sigma concl st se = module Constr_map = Map.Make(GlobRef.Ordered) let is_transparent_gr ts = function - | VarRef id -> TranspState.is_transparent_variable ts id - | ConstRef cst -> TranspState.is_transparent_constant ts cst + | VarRef id -> TransparentState.is_transparent_variable ts id + | ConstRef cst -> TransparentState.is_transparent_constant ts cst | IndRef _ | ConstructRef _ -> false let strip_params env sigma c = @@ -497,7 +497,7 @@ type hint_db_name = string module Hint_db : sig type t -val empty : ?name:hint_db_name -> TranspState.t -> bool -> t +val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list @@ -513,8 +513,8 @@ val remove_one : GlobRef.t -> t -> t val remove_list : GlobRef.t list -> t -> t val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool -val transparent_state : t -> TranspState.t -val set_transparent_state : t -> TranspState.t -> t +val transparent_state : t -> TransparentState.t +val set_transparent_state : t -> TransparentState.t -> t val add_cut : hints_path -> t -> t val add_mode : GlobRef.t -> hint_mode array -> t -> t val cut : t -> hints_path @@ -526,7 +526,7 @@ end = struct type t = { - hintdb_state : TranspState.t; + hintdb_state : TransparentState.t; hintdb_cut : hints_path; hintdb_unfolds : Id.Set.t * Cset.t; hintdb_max_id : int; @@ -664,7 +664,7 @@ struct match v.code.obj with | Unfold_nth egr -> let addunf ts (ids, csts) = - let open TranspState in + let open TransparentState in match egr with | EvalVarRef id -> { ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts) @@ -743,8 +743,8 @@ let typeclasses_db = "typeclass_instances" let rewrite_db = "rewrite" let auto_init_db = - Hintdbmap.add typeclasses_db (Hint_db.empty TranspState.full true) - (Hintdbmap.add rewrite_db (Hint_db.empty TranspState.cst_full true) + Hintdbmap.add typeclasses_db (Hint_db.empty TransparentState.full true) + (Hintdbmap.add rewrite_db (Hint_db.empty TransparentState.cst_full true) Hintdbmap.empty) let searchtable = Summary.ref ~name:"searchtable" auto_init_db @@ -980,7 +980,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let get_db dbname = try searchtable_map dbname - with Not_found -> Hint_db.empty ~name:dbname TranspState.empty false + with Not_found -> Hint_db.empty ~name:dbname TransparentState.empty false let add_hint dbname hintlist = let check (_, h) = @@ -998,7 +998,7 @@ let add_hint dbname hintlist = searchtable_add (dbname,db') let add_transparency dbname target b = - let open TranspState in + let open TransparentState in let db = get_db dbname in let st = Hint_db.transparent_state db in let st' = @@ -1019,7 +1019,7 @@ let remove_hint dbname grs = searchtable_add (dbname, db') type hint_action = - | CreateDB of bool * TranspState.t + | CreateDB of bool * TransparentState.t | AddTransparency of evaluable_global_reference hints_transparency_target * bool | AddHints of hint_entry list | RemoveHints of GlobRef.t list @@ -1547,7 +1547,7 @@ let pr_hint_db_env env sigma db = in Hint_db.fold fold db (mt ()) in - let { TranspState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in + let { TransparentState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in hov 0 ((if Hint_db.use_dn db then str"Discriminated database" else str"Non-discriminated database")) ++ fnl () ++ diff --git a/tactics/hints.mli b/tactics/hints.mli index 43cfb6a059b8..dd2c63d3511b 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -122,7 +122,7 @@ val glob_hints_path : module Hint_db : sig type t - val empty : ?name:hint_db_name -> TranspState.t -> bool -> t + val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t val find : GlobRef.t -> t -> search_entry (** All hints which have no pattern. @@ -155,8 +155,8 @@ module Hint_db : hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool - val transparent_state : t -> TranspState.t - val set_transparent_state : t -> TranspState.t -> t + val transparent_state : t -> TransparentState.t + val set_transparent_state : t -> TransparentState.t -> t val add_cut : hints_path -> t -> t val cut : t -> hints_path @@ -191,7 +191,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit [use_dn] switches the use of the discrimination net for all hints and patterns. *) -val create_hint_db : bool -> hint_db_name -> TranspState.t -> bool -> unit +val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit @@ -273,7 +273,7 @@ val repr_hint : hint -> (raw_hint * clausenv) hint_ast Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed *) -val make_local_hint_db : env -> evar_map -> ?ts:TranspState.t -> bool -> delayed_open_constr list -> hint_db +val make_local_hint_db : env -> evar_map -> ?ts:TransparentState.t -> bool -> delayed_open_constr list -> hint_db val make_db_list : hint_db_name list -> hint_db list diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2601b5fd8476..349cfce20589 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1660,7 +1660,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars let sigma = Tacmach.New.project gl in let ts = if respect_opaque then Conv_oracle.get_transp_state (oracle env) - else TranspState.full + else TransparentState.full in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in @@ -1826,7 +1826,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta let sigma = Tacmach.New.project gl in let ts = if respect_opaque then Conv_oracle.get_transp_state (oracle env) - else TranspState.full + else TransparentState.full in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in @@ -4909,7 +4909,7 @@ let constr_eq ~strict x y = | None -> fail end -let unify ?(state=TranspState.full) x y = +let unify ?(state=TransparentState.full) x y = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -4922,7 +4922,7 @@ let unify ?(state=TranspState.full) x y = let flags = { (default_unify_flags ()) with core_unify_flags = core_flags; merge_unify_flags = core_flags; - subterm_unify_flags = { core_flags with modulo_delta = TranspState.empty } } + subterm_unify_flags = { core_flags with modulo_delta = TransparentState.empty } } in let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in Proofview.Unsafe.tclEVARS sigma diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 1db65fc1aa67..4e91a9a7281e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -419,7 +419,7 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - are added to the evar map. *) val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic -val unify : ?state:TranspState.t -> constr -> constr -> unit Proofview.tactic +val unify : ?state:TransparentState.t -> constr -> constr -> unit Proofview.tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> unit Proofview.tactic diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index b51b6cedfb84..3ca2a4ad6bfa 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -315,7 +315,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let t = type_of_constant cb in let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Constant kn,l)) t accu - else if add_opaque && (Declareops.is_opaque cb || not (TranspState.is_transparent_constant st kn)) then + else if add_opaque && (Declareops.is_opaque cb || not (TransparentState.is_transparent_constant st kn)) then let t = type_of_constant cb in ContextObjectMap.add (Opaque kn) t accu else if add_transparent then diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 56d62021947f..536185f4aa6c 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -28,5 +28,5 @@ val traverse : on which a term relies (together with their type). The above warning of {!traverse} also applies. *) val assumptions : - ?add_opaque:bool -> ?add_transparent:bool -> TranspState.t -> + ?add_opaque:bool -> ?add_transparent:bool -> TransparentState.t -> GlobRef.t -> constr -> types ContextObjectMap.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 34ddf3377f35..7765f5b4174e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1096,7 +1096,7 @@ let vernac_restore_state file = (* Commands *) let vernac_create_hintdb ~module_local id b = - Hints.create_hint_db module_local id TranspState.full b + Hints.create_hint_db module_local id TransparentState.full b let vernac_remove_hints ~module_local dbs ids = Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids)