Addapt unification algorithms and tactics.

plugins/ltac/tacintern.ml

@@ -303,7 +303,12 @@ let short_name strict qid =
   else None
 
 let evalref_of_globref ?loc ?short = function
-  | GlobRef.ConstRef cst -> ArgArg (Evaluable.EvalConstRef cst, short)
+  | GlobRef.ConstRef cst ->
+      begin
+        match Structures.PrimitiveProjections.find_opt cst with
+        | None -> ArgArg (Evaluable.EvalConstRef cst, short)
+        | Some p -> ArgArg (Evaluable.EvalProjectionRef p, short)
+      end
   | GlobRef.VarRef id -> ArgArg (Evaluable.EvalVarRef id, short)
   | r ->
     let tpe = match r with

plugins/ltac/tacinterp.ml

@@ -432,6 +432,7 @@ let interp_evaluable ist env sigma = function
       with Not_found as exn ->
         match r with
         | Evaluable.EvalConstRef _ -> r
+        | Evaluable.EvalProjectionRef _ -> r
         | _ ->
           let _, info = Exninfo.capture exn in
           Nametab.error_global_not_found ~info (qualid_of_ident ?loc id)

pretyping/cbv.ml

@@ -473,7 +473,7 @@ let rec norm_head info env t stack =
 
   | Proj (p, r, c) ->
     let p' =
-      if red_set info.reds (fCONST (Projection.constant p))
+      if red_set info.reds (fPROJ (Projection.repr p))
         && red_set info.reds fBETA
       then Projection.unfold p
       else p

pretyping/evarconv.ml

@@ -72,15 +72,14 @@ let coq_unit_judge env sigma =
   | None -> sigma, unit_judge_fallback
 
 let unfold_projection env evd ts p r c =
-  let cst = Projection.constant p in
-    if TransparentState.is_transparent_constant ts cst then
-      Some (mkProj (Projection.unfold p, r, c))
-    else None
+  if TransparentState.is_transparent_projection ts (Projection.repr p) then
+    Some (mkProj (Projection.unfold p, r, c))
+  else None
 
 let eval_flexible_term ts env evd c =
   match EConstr.kind evd c with
   | Const (c, u) ->
-      if TransparentState.is_transparent_constant ts c
+      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 ->
@@ -170,9 +169,11 @@ let occur_rigidly flags env evd (evk,_) t =
     | Construct _ -> Normal false
     | Ind _ | Sort _ -> Rigid false
     | Proj (p, _, c) ->
-      let cst = Projection.constant p in
-      let rigid = not (TransparentState.is_transparent_constant flags.open_ts cst) in
-        if rigid then aux c
+       let rigid =
+         let p = Projection.repr p in
+         not (TransparentState.is_transparent_projection flags.open_ts p)
+       in
+       if rigid then aux c
         else (* if the evar appears rigidly in c then this elimination
                 cannot reduce and we have a rigid occurrence, otherwise
                 we don't know. *)
@@ -189,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/reductionops.ml

@@ -258,7 +258,7 @@ struct
          prvect_with_sep (pr_bar) (fun (_, c) -> pr_c c) br
        ++ str ")"
     | Proj (p,_)  ->
-      str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
+      str "ZProj(" ++ Projection.debug_print p ++ str ")"
     | Fix (f,args) ->
        str "ZFix(" ++ Constr.debug_print_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"

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 *)
@@ -531,7 +531,7 @@ let match_eval_ref_value env sigma constr stack =
     else
       None
   | Proj (p, r, c) when not (Projection.unfolded p) ->
-     if is_evaluable env (EvalConstRef (Projection.constant p)) then
+     if is_evaluable env (EvalProjectionRef (Projection.repr p)) then
        Some (mkProj (Projection.unfold p, r, c))
      else None
   | Var id when is_evaluable env (EvalVarRef id) ->
@@ -743,7 +743,7 @@ and whd_simpl_stack allowed_reds env sigma =
       | Proj (p, _, c) ->
         let ans =
            let unf = Projection.unfolded p in
-           if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
+           if unf || is_evaluable env (EvalProjectionRef (Projection.repr p)) then
              let npars = Projection.npars p in
              match unf, ReductionBehaviour.get (Projection.constant p) with
               | false, Some NeverUnfold -> NotReducible

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)) ||
@@ -1335,7 +1335,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) &&

tactics/cbn.ml

@@ -193,7 +193,7 @@ struct
          prvect_with_sep (pr_bar) (fun (_, b) -> pr_c b) br
        ++ str ")"
     | Proj (p,_,cst) ->
-      str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
+      str "ZProj(" ++ Projection.debug_print p ++ str ")"
     | Fix (f,args,cst) ->
        str "ZFix(" ++ Constr.debug_print_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
@@ -217,7 +217,7 @@ struct
         else str"(" ++ Constant.debug_print c ++ str ", " ++
           UVars.Instance.pr Sorts.QVar.raw_pr Univ.Level.raw_pr u ++ str")"
       | Cst_proj (p,r) ->
-        str".(" ++ Constant.debug_print (Projection.constant p) ++ str")"
+        str".(" ++ Projection.debug_print p ++ str")"
 
   let empty = []
 

tactics/redexpr.ml

@@ -129,9 +129,14 @@ type red_expr_val =
   (constr, Evaluable.t, constr_pattern, strength * RedFlags.reds) red_expr_gen0
 
 let make_flag_constant = function
-  | Evaluable.EvalVarRef id -> fVAR id
-  | Evaluable.EvalConstRef sp -> fCONST sp
-  | Evaluable.EvalProjectionRef p -> fPROJ p
+  | Evaluable.EvalVarRef id -> [fVAR id]
+  | Evaluable.EvalConstRef sp ->
+      begin
+        match Structures.PrimitiveProjections.find_opt sp with
+        | None -> [fCONST sp]
+        | Some p -> [fCONST sp; fPROJ p]
+      end
+  | Evaluable.EvalProjectionRef p -> [fPROJ p; fCONST (Projection.Repr.constant p)]
 
 let make_flag env f =
   let red = no_red in
@@ -146,12 +151,12 @@ let make_flag env f =
         let red = red_add_transparent red
                     (Conv_oracle.get_transp_state (Environ.oracle env)) in
         List.fold_right
-          (fun v red -> red_sub red (make_flag_constant v))
+          (fun v red -> red_sub_list red (make_flag_constant v))
           f.rConst red
     else (* Only rConst *)
         let red = red_add red fDELTA in
         List.fold_right
-          (fun v red -> red_add red (make_flag_constant v))
+          (fun v red -> red_add_list red (make_flag_constant v))
           f.rConst red
   in
   f.rStrength, red

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