XXX experiment

pretyping/evarconv.ml

@@ -79,12 +79,7 @@ let unfold_projection env evd ts p r c =
 let eval_flexible_term ts env evd c =
   match EConstr.kind evd c with
   | Const (c, u) ->
-      let transparent =
-        match Structures.PrimitiveProjections.find_opt c with
-        | Some pr -> TransparentState.is_transparent_projection ts pr
-        | None -> TransparentState.is_transparent_constant ts c
-      in
-      if transparent
+      if Structures.PrimitiveProjections.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 ->
@@ -195,7 +190,7 @@ let occur_rigidly flags env evd (evk,_) t =
     | Lambda (na, t, b) -> aux b
     | LetIn (na, _, _, b) -> aux b
     | Const (c,_) ->
-      if TransparentState.is_transparent_constant flags.open_ts c then Reducible
+      if Structures.PrimitiveProjections.is_transparent_constant flags.open_ts c then Reducible
       else Rigid false
     | Prod (_, b, t) ->
       let b' = aux b and t' = aux t in

pretyping/structures.ml

@@ -443,4 +443,9 @@ let find_opt_with_relevance (c,u) =
       let u = EConstr.Unsafe.to_instance u in
       p, Relevanceops.relevance_of_projection_repr (Global.env()) (p,u))
 
+let is_transparent_constant ts c =
+  match find_opt c with
+  | None -> TransparentState.is_transparent_constant ts c
+  | Some p -> TransparentState.is_transparent_projection ts p
+
 end

pretyping/structures.mli

@@ -163,4 +163,5 @@ val find_opt : Names.Constant.t -> Names.Projection.Repr.t option
 val find_opt_with_relevance : Names.Constant.t * EConstr.EInstance.t
   -> (Names.Projection.Repr.t * Sorts.relevance) option
 
+val is_transparent_constant : TransparentState.t -> Names.Constant.t -> bool
 end

pretyping/tacred.ml

@@ -118,7 +118,7 @@ let isEvalRef env sigma c = match EConstr.kind sigma c with
   | _ -> false
 
 let isTransparentEvalRef env sigma ts c = match EConstr.kind sigma c with
-  | Const (cst,_) -> is_evaluable env (EvalConstRef cst) && TransparentState.is_transparent_constant ts cst
+  | Const (cst,_) -> is_evaluable env (EvalConstRef cst) && Structures.PrimitiveProjections.is_transparent_constant ts cst
   | Var id -> is_evaluable env (EvalVarRef id) && TransparentState.is_transparent_variable ts id
   | Rel _ -> true
   | Evar _ -> false (* undefined *)

pretyping/unification.ml

@@ -503,7 +503,7 @@ 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 (Evaluable.EvalConstRef cst) &&
-      (TransparentState.is_transparent_constant flags.modulo_delta cst
+      (Structures.PrimitiveProjections.is_transparent_constant flags.modulo_delta cst
        || PrimitiveProjections.mem cst) ->
       let u = EInstance.kind sigma u in
       Some (IsKey (ConstKey (cst, u)))
@@ -549,7 +549,7 @@ let oracle_order env cf1 cf2 =
 
 let is_rigid_head sigma flags t =
   match EConstr.kind sigma t with
-  | Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst)
+  | Const (cst,u) -> not (Structures.PrimitiveProjections.is_transparent_constant flags.modulo_delta cst)
   | Ind (i,u) -> true
   | Construct _ | Int _ | Float _ | Array _ -> true
   | Fix _ | CoFix _ -> true
@@ -640,7 +640,7 @@ let rec is_neutral env sigma ts t =
     | Const (c, u) ->
       not (Environ.evaluable_constant c env) ||
       not (is_transparent env (Evaluable.EvalConstRef c)) ||
-      not (TransparentState.is_transparent_constant ts c)
+      not (Structures.PrimitiveProjections.is_transparent_constant ts c)
     | Var id ->
       not (Environ.evaluable_named id env) ||
       not (is_transparent env (Evaluable.EvalVarRef id)) ||
@@ -1339,7 +1339,7 @@ let applyHead env evd c cl =
 
 let is_mimick_head sigma ts f =
   match EConstr.kind sigma f with
-  | Const (c,u) -> not (TransparentState.is_transparent_constant ts c)
+  | Const (c,u) -> not (Structures.PrimitiveProjections.is_transparent_constant ts c)
   | Var id -> not (TransparentState.is_transparent_variable ts id)
   | (Rel _|Construct _|Ind _) -> true
   | _ -> false

tactics/btermdn.ml

@@ -85,7 +85,7 @@ let evaluable_constant c env ts =
   (* This is a hack to work around a broken Print Module implementation, see
      bug #2668. *)
   (if Environ.mem_constant c env then Environ.evaluable_constant c env else true) &&
-  (match ts with None -> true | Some ts -> TransparentState.is_transparent_constant ts c)
+  (match ts with None -> true | Some ts -> Structures.PrimitiveProjections.is_transparent_constant ts c)
 
 let evaluable_named id env ts =
   (try Environ.evaluable_named id env with Not_found -> true) &&

vernac/assumptions.ml

@@ -370,7 +370,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 (TransparentState.is_transparent_constant st kn)) then
+    else if add_opaque && (Declareops.is_opaque cb || not (Structures.PrimitiveProjections.is_transparent_constant st kn)) then
       let t = type_of_constant cb in
       ContextObjectMap.add (Opaque kn) t accu
     else if add_transparent then