Rename TranspState into TransparentState.

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.
 

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

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;

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

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

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
 

kernel/kernel.mllib

@@ -1,5 +1,5 @@
 Names
-TranspState
+TransparentState
 Uint31
 Univ
 UGraph

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
 

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

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

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

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]
 				  )
 			   )
 			)

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]
 		      ]
 		    )
 		  )

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
   }

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;

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 =

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

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