Merge remote-tracking branch 'origin/master' into stm+doc_hook

14 files changed, 297 insertions, 313 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index c9f18d89be..5ea9b79336 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -145,7 +145,7 @@ let mkSTACK = function
 
 type cbv_infos = {
   env : Environ.env;
-  tab : cbv_value Declarations.constant_def KeyTable.t;
+  tab : (cbv_value, Empty.t) Declarations.constant_def KeyTable.t;
   reds : RedFlags.reds;
   sigma : Evd.evar_map
 }
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 062e3ca8b2..82726eccf0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -708,9 +708,6 @@ type binder_kind = BProd | BLambda | BLetIn
 (**********************************************************************)
 (* Main detyping function                                             *)
 
-let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable."))
-let set_detype_anonymous f = detype_anonymous := f
-
 let detype_level sigma l =
   let l = hack_qualid_of_univ_level sigma l in
   GType (UNamed l)
@@ -732,11 +729,13 @@ and detype_r d flags avoid env sigma t =
   match EConstr.kind sigma (collapse_appl sigma t) with
     | Rel n ->
       (try match lookup_name_of_rel n (fst env) with
-	 | Name id   -> GVar id
-	 | Anonymous -> GVar (!detype_anonymous n)
+         | Name id   -> GVar id
+         | Anonymous ->
+           let s = "_ANONYMOUS_REL_"^(string_of_int n) in
+           GVar (Id.of_string s)
        with Not_found ->
-	 let s = "_UNBOUND_REL_"^(string_of_int n)
-	 in GVar (Id.of_string s))
+         let s = "_UNBOUND_REL_"^(string_of_int n)
+         in GVar (Id.of_string s))
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
         if n = Constr_matching.special_meta then
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 1a8e97efb8..00b0578a52 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -68,9 +68,6 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> clo
 val lookup_name_as_displayed  : env -> evar_map -> constr -> Id.t -> int option
 val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
 
-(* XXX: This is a hack and should go away *)
-val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit
-
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0ccc4fd9f9..6b149a8b41 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -146,8 +146,8 @@ let flex_kind_of_term flags env evd c sk =
 let apprec_nohdbeta flags env evd c =
   let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
   if flags.modulo_betaiota && Stack.not_purely_applicative sk
-  then Stack.zip evd (fst (whd_betaiota_deltazeta_for_iota_state
-                   flags.open_ts env evd Cst_stack.empty appr))
+  then Stack.zip evd (whd_betaiota_deltazeta_for_iota_state
+                   flags.open_ts env evd appr)
   else c
 
 let position_problem l2r = function
@@ -496,8 +496,8 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
         let term2 = apprec_nohdbeta flags env evd term2 in
 	let default () = 
           evar_eqappr_x flags env evd pbty
-            (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
-            (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
+            (whd_nored_state evd (term1,Stack.empty))
+            (whd_nored_state evd (term2,Stack.empty))
 	in
           begin match EConstr.kind evd term1, EConstr.kind evd term2 with
           | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
@@ -525,7 +525,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
         end
 
 and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
-    ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
+    (term1, sk1 as appr1) (term2, sk2 as appr2) =
   let quick_fail i = (* not costly, loses info *)
     UnifFailure (i, NotSameHead)
   in
@@ -555,8 +555,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     let c = nf_evar evd c1 in
     let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
-      flags.open_ts env' evd Cst_stack.empty (c'1, Stack.empty) in
-    let out2 = whd_nored_state evd
+      flags.open_ts env' evd (c'1, Stack.empty) in
+    let out2, _ = whd_nored_state evd
       (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty),
       Cst_stack.empty in
     if onleft then evar_eqappr_x flags env' evd CONV out1 out2
@@ -636,11 +636,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 	    else quick_fail i)
             ev lF tM i
   in
-  let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
+  let flex_maybeflex on_left ev (termF,skF as apprF) (termM, skM as apprM) vM =
     let switch f a b = if on_left then f a b else f b a in
     let delta i =
-      switch (evar_eqappr_x flags env i pbty) (apprF,cstsF)
-        (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i cstsM (vM,skM))
+      switch (evar_eqappr_x flags env i pbty) apprF
+        (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (vM,skM))
     in    
     let default i = ise_try i [miller on_left ev apprF apprM;
                                consume on_left apprF apprM;
@@ -658,11 +658,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 	      let f =
 		try 
 		  let termM' = Retyping.expand_projection env evd p c [] in
-		  let apprM', cstsM' = 
-                    whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd cstsM (termM',skM)
+                  let apprM' =
+                    whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd (termM',skM)
 		  in
 		  let delta' i = 
-                    switch (evar_eqappr_x flags env i pbty) (apprF,cstsF) (apprM',cstsM')
+                    switch (evar_eqappr_x flags env i pbty) apprF apprM'
 		  in
                   fun i -> ise_try i [miller on_left ev apprF apprM';
                                    consume on_left apprF apprM'; delta']
@@ -718,7 +718,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                           (position_problem true pbty,destEvar i' ev1',term2)
        else
          evar_eqappr_x flags env evd pbty
-                       ((ev1', sk1), csts1) ((term2, sk2), csts2)
+                       (ev1', sk1) (term2, sk2)
     | Some (r,[]), Success i' ->
        (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
        (* we now unify r[?ev1] and ?ev2 *)
@@ -728,7 +728,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                           (position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r))
        else
          evar_eqappr_x flags env evd pbty
-                       ((ev2', sk1), csts1) ((term2, sk2), csts2)
+                       (ev2', sk1) (term2, sk2)
     | Some ([],r), Success i' ->
        (* Symmetrically *)
        (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
@@ -738,7 +738,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
          solve_simple_eqn (conv_fun evar_conv_x) flags env i'
                           (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r))
        else evar_eqappr_x flags env evd pbty
-                          ((ev1', sk1), csts1) ((term2, sk2), csts2)
+                          (ev1', sk1) (term2, sk2)
     | None, (UnifFailure _ as x) ->
        (* sk1 and sk2 have no common outer part *)
        if Stack.not_purely_applicative sk2 then
@@ -808,10 +808,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         ise_try evd [f1; f2; f3; f4; f5]
 
     | Flexible ev1, MaybeFlexible v2 ->
-      flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2
+      flex_maybeflex true ev1 appr1 appr2 v2
 
     | MaybeFlexible v1, Flexible ev2 -> 
-      flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1
+      flex_maybeflex false ev2 appr2 appr1 v1
 
     | MaybeFlexible v1, MaybeFlexible v2 -> begin
         match EConstr.kind evd term1, EConstr.kind evd term2 with
@@ -829,8 +829,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                evar_conv_x flags (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
              (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
         and f2 i =
-          let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1)
-          and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2)
+          let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v1,sk1)
+          and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v2,sk2)
           in evar_eqappr_x flags env i pbty out1 out2
 	in
 	ise_try evd [f1; f2]
@@ -841,8 +841,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
             [(fun i -> evar_conv_x flags env i CONV c c');
              (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
 	  and f2 i =
-            let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1)
-            and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2)
+            let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v1,sk1)
+            and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v2,sk2)
             in evar_eqappr_x flags env i pbty out1 out2
 	  in
 	    ise_try evd [f1; f2]
@@ -855,8 +855,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 	  in
 	    (match res with 
 	    | Some (f1,args1) -> 
-              evar_eqappr_x flags env evd pbty ((f1,Stack.append_app args1 sk1),csts1)
-		(appr2,csts2)
+              evar_eqappr_x flags env evd pbty (f1,Stack.append_app args1 sk1)
+                appr2
 	    | None -> UnifFailure (evd,NotSameHead))
 	      
 	| Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') ->
@@ -866,7 +866,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 	  in 
 	    (match res with
 	    | Some (f2,args2) ->
-              evar_eqappr_x flags env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2)
+              evar_eqappr_x flags env evd pbty appr1 (f2,Stack.append_app args2 sk2)
 	    | None -> UnifFailure (evd,NotSameHead))
 	      
 	| _, _ ->
@@ -906,16 +906,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 	    (* false (* immediate solution without Canon Struct *)*)
             | Lambda _ -> assert (match args with [] -> true | _ -> false); true
             | LetIn (_,b,_,c) -> is_unnamed
-	     (fst (whd_betaiota_deltazeta_for_iota_state
-                      flags.open_ts env i Cst_stack.empty (subst1 b c, args)))
+             (whd_betaiota_deltazeta_for_iota_state
+                      flags.open_ts env i (subst1 b c, args))
 	    | Fix _ -> true (* Partially applied fix can be the result of a whd call *)
 	    | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args
             | Case _ | App _| Cast _ -> assert false in
           let rhs_is_stuck_and_unnamed () =
 	    let applicative_stack = fst (Stack.strip_app sk2) in
 	    is_unnamed
-	      (fst (whd_betaiota_deltazeta_for_iota_state
-                      flags.open_ts env i Cst_stack.empty (v2, applicative_stack))) in
+              (whd_betaiota_deltazeta_for_iota_state
+                      flags.open_ts env i (v2, applicative_stack)) in
           let rhs_is_already_stuck =
             rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
 
@@ -923,12 +923,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 	    && (not (Stack.not_purely_applicative sk1)) then
             evar_eqappr_x ~rhs_is_already_stuck flags env i pbty
 	      (whd_betaiota_deltazeta_for_iota_state
-                 flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
-	      (appr2,csts2)
+                 flags.open_ts env i(v1,sk1))
+              appr2
 	  else
-            evar_eqappr_x flags env i pbty (appr1,csts1)
+            evar_eqappr_x flags env i pbty appr1
 	      (whd_betaiota_deltazeta_for_iota_state
-                 flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+                 flags.open_ts env i (v2,sk2))
 	in
 	ise_try evd [f1; f2; f3]
     end
@@ -957,8 +957,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 	and f4 i =
           evar_eqappr_x flags env i pbty
 	    (whd_betaiota_deltazeta_for_iota_state
-               flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
-	    (appr2,csts2)
+               flags.open_ts env i (v1,sk1))
+            appr2
 	in
 	  ise_try evd [f3; f4]
 
@@ -969,9 +969,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
              else conv_record flags env i (check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f4 i =
-          evar_eqappr_x flags env i pbty (appr1,csts1)
+          evar_eqappr_x flags env i pbty appr1
 	    (whd_betaiota_deltazeta_for_iota_state
-               flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+               flags.open_ts env i (v2,sk2))
 	in
 	  ise_try evd [f3; f4]
 
@@ -1769,28 +1769,3 @@ let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 =
      solve_unif_constraints_with_heuristics ~flags ~with_ho env evd
   | UnifFailure (evd, reason) ->
      raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason)))
-
-(* deprecated *)
-let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd =
-  let flags = default_flags_of ts in
-  match evar_conv_x flags env evd CONV  t1 t2 with
-  | Success evd' -> evd'
-  | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
-
-let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
-  let flags = default_flags_of ts in
-  match evar_conv_x flags env evd CUMUL t1 t2 with
-  | Success evd' -> evd'
-  | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
-
-let make_opt = function
-  | Success evd -> Some evd
-  | UnifFailure _ -> None
-
-let conv env ?(ts=default_transparent_state env) evd t1 t2 =
-  let flags = default_flags_of ts in
-  make_opt(evar_conv_x flags env evd CONV t1 t2)
-
-let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
-  let flags = default_flags_of ts in
-  make_opt(evar_conv_x flags env evd CUMUL t1 t2)
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 0fe47c2a48..eae961714d 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -46,19 +46,6 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error
 val unify_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
 val unify_leq_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
 
-(** returns exception UnableToUnify with best known evar_map if not unifiable *)
-val the_conv_x     : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
-[@@ocaml.deprecated "Use Evarconv.unify_delay instead"]
-val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
-[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"]
-(** The same function resolving evars by side-effect and
-   catching the exception *)
-
-val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
-[@@ocaml.deprecated "Use Evarconv.unify_delay instead"]
-val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
-[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"]
-
 (** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining
     constraints. In case of success the two terms are unified without condition.
 
@@ -144,7 +131,7 @@ val evar_unify : Evarsolve.unifier
 (* For debugging *)
 val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags ->
   env -> evar_map ->
-    conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
+    conv_pb -> state -> state ->
       Evarsolve.unification_result
 
 val occur_rigidly : Evarsolve.unify_flags ->
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index e694502231..0fcd6a9e9d 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -415,7 +415,7 @@ and  nf_predicate env sigma ind mip params v pT =
 and nf_evar env sigma evk args =
   let evi = try Evd.find sigma evk with Not_found -> assert false in
   let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
-  let ty = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in
+  let ty = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in
   if List.is_empty hyps then begin
     assert (Int.equal (Array.length args) 0);
     mkEvar (evk, [||]), ty
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 48d981082c..f2b8671a48 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -380,7 +380,7 @@ let orelse_name name name' = match name with
   | Anonymous -> name'
   | _ -> name
 
-let pretype_id pretype k0 loc env sigma id =
+let pretype_id pretype loc env sigma id =
   (* Look for the binder of [id] *)
   try
     let (n,_,typ) = lookup_rel_id id (rel_context !!env) in
@@ -475,10 +475,10 @@ let mark_obligation_evar sigma k evc =
 (* in environment [env], with existential variables [sigma] and *)
 (* the type constraint tycon *)
 
-let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
+let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
   let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in
-  let pretype_type = pretype_type ~program_mode ~poly k0 resolve_tc in
-  let pretype = pretype ~program_mode ~poly k0 resolve_tc in
+  let pretype_type = pretype_type ~program_mode ~poly resolve_tc in
+  let pretype = pretype ~program_mode ~poly resolve_tc in
   let open Context.Rel.Declaration in
   let loc = t.CAst.loc in
   match DAst.get t with
@@ -487,7 +487,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
     inh_conv_coerce_to_tycon ?loc env sigma t_ref tycon
 
   | GVar id ->
-    let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) k0 loc env sigma id in
+    let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in
     inh_conv_coerce_to_tycon ?loc env sigma t_id tycon
 
   | GEvar (id, inst) ->
@@ -498,7 +498,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
         try Evd.evar_key id sigma
         with Not_found -> error_evar_not_found ?loc !!env sigma id in
       let hyps = evar_filtered_context (Evd.find sigma evk) in
-      let sigma, args = pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk inst in
+      let sigma, args = pretype_instance ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = Retyping.get_judgment_of !!env sigma c in
       inh_conv_coerce_to_tycon ?loc env sigma j tycon
@@ -984,7 +984,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
         in
         inh_conv_coerce_to_tycon ?loc env sigma resj tycon
 
-and pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk update =
+and pretype_instance ~program_mode ~poly resolve_tc env sigma loc hyps evk update =
   let f decl (subst,update,sigma) =
     let id = NamedDecl.get_id decl in
     let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
@@ -1016,7 +1016,7 @@ and pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk up
     let sigma, c, update =
       try
         let c = List.assoc id update in
-        let sigma, c = pretype ~program_mode ~poly k0 resolve_tc (mk_tycon t) env sigma c in
+        let sigma, c = pretype ~program_mode ~poly resolve_tc (mk_tycon t) env sigma c in
         check_body sigma id (Some c.uj_val);
         sigma, c.uj_val, List.remove_assoc id update
       with Not_found ->
@@ -1041,7 +1041,7 @@ and pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk up
   sigma, Array.map_of_list snd subst
 
 (* [pretype_type valcon env sigma c] coerces [c] into a type *)
-and pretype_type ~program_mode ~poly k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
+and pretype_type ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
   | GHole (knd, naming, None) ->
       let loc = loc_of_glob_constr c in
       (match valcon with
@@ -1068,7 +1068,7 @@ and pretype_type ~program_mode ~poly k0 resolve_tc valcon (env : GlobEnv.t) sigm
          let sigma = if program_mode then mark_obligation_evar sigma knd utj_val else sigma in
          sigma, { utj_val; utj_type = s})
   | _ ->
-      let sigma, j = pretype ~program_mode ~poly k0 resolve_tc empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode ~poly resolve_tc empty_tycon env sigma c in
       let loc = loc_of_glob_constr c in
       let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in
 	match valcon with
@@ -1088,16 +1088,15 @@ let ise_pretype_gen flags env sigma lvar kind c =
     if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
   in
   let env = GlobEnv.make ~hypnaming env sigma lvar in
-  let k0 = Context.Rel.length (rel_context !!env) in
   let sigma', c', c'_ty = match kind with
     | WithoutTypeConstraint ->
-      let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in
       sigma, j.uj_val, j.uj_type
     | OfType exptyp ->
-      let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+      let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses (mk_tycon exptyp) env sigma c in
       sigma, j.uj_val, j.uj_type
     | IsType ->
-      let sigma, tj = pretype_type ~program_mode ~poly k0 flags.use_typeclasses empty_valcon env sigma c in
+      let sigma, tj = pretype_type ~program_mode ~poly flags.use_typeclasses empty_valcon env sigma c in
       sigma, tj.utj_val, mkSort tj.utj_type
   in
   process_inference_flags flags !!env sigma (sigma',c',c'_ty)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 1feb8acd5f..a23c58c062 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -27,16 +27,27 @@ open Reductionops
 (*s A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
-(* Table des structures: le nom de la structure (un [inductive]) donne
-   le nom du constructeur, le nombre de paramètres et pour chaque
-   argument réel du constructeur, le nom de la projection
-   correspondante, si valide, et un booléen disant si c'est une vraie
-   projection ou bien une fonction constante (associée à un LetIn) *)
+(* Table of structures.
+   It maps to each structure name (of type [inductive]):
+     - the name of its constructor;
+     - the number of parameters;
+     - for each true argument, some data about the corresponding projection:
+         * its name (may be anonymous);
+         * whether it is a true projection (as opposed to a constant function, LetIn);
+         * whether it should be used as a canonical hint;
+         * the constant realizing this projection (if any).
+*)
+
+type proj_kind = {
+  pk_name: Name.t;
+  pk_true_proj: bool;
+  pk_canonical: bool;
+}
 
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (Name.t * bool) list;
+  s_PROJKIND : proj_kind list;
   s_PROJ : Constant.t option list }
 
 let structure_table =
@@ -47,7 +58,7 @@ let projection_table =
 (* TODO: could be unify struc_typ and struc_tuple ? *)
 
 type struc_tuple =
-    constructor * (Name.t * bool) list * Constant.t option list
+    constructor * proj_kind list * Constant.t option list
 
 let register_structure env (id,kl,projs) =
   let open Declarations in
@@ -161,7 +172,7 @@ let canonical_projections () =
     !object_table []
 
 let keep_true_projections projs kinds =
-  let filter (p, (_, b)) = if b then Some p else None in
+  let filter (p, { pk_true_proj ; pk_canonical }) = if pk_true_proj then Some (p, pk_canonical) else None in
   List.map_filter filter (List.combine projs kinds)
 
 let rec cs_pattern_of_constr env t =
@@ -191,41 +202,36 @@ let warn_projection_no_head_constant =
 
 (* Intended to always succeed *)
 let compute_canonical_projections env ~warn (con,ind) =
-  let ctx = Environ.constant_context env con in
-  let u = Univ.make_abstract_instance ctx in
-  let v = (mkConstU (con,u)) in
+  let o_CTX = Environ.constant_context env con in
+  let u = Univ.make_abstract_instance o_CTX in
+  let o_DEF = mkConstU (con, u) in
   let c = Environ.constant_value_in env (con,u) in
   let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in
   let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
-  let lt = List.rev_map snd sign in
+  let o_TABS = List.rev_map snd sign in
   let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
     lookup_structure ind in
-  let params, projs = List.chop p args in
+  let o_TPARAMS, projs = List.chop p args in
+  let o_NPARAMS = List.length o_TPARAMS in
   let lpj = keep_true_projections lpj kl in
-  let lps = List.combine lpj projs in
   let nenv = Termops.push_rels_assum sign env in
-  let comp =
-    List.fold_left
-      (fun l (spopt,t) -> (* comp=components *)
-	 match spopt with
-           | Some proji_sp ->
-	       begin
-		 try
-		   let patt, n , args = cs_pattern_of_constr nenv t in
-		     ((ConstRef proji_sp, patt, t, n, args) :: l)
-		 with Not_found ->
-                   if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp);
-                   l
-	       end
-	   | _ -> l)
-      [] lps in
-  List.map (fun (refi,c,t,inj,argj) ->
-    (refi,(c,t)),
-    {o_DEF=v; o_CTX=ctx; o_INJ=inj; o_TABS=lt;
-     o_TPARAMS=params; o_NPARAMS=List.length params; o_TCOMPS=argj})
-    comp
+  List.fold_left2 (fun acc (spopt, canonical) t ->
+      if canonical
+      then
+        Option.cata (fun proji_sp ->
+            match cs_pattern_of_constr nenv t with
+            | patt, o_INJ, o_TCOMPS ->
+              ((ConstRef proji_sp, (patt, t)),
+               { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
+              :: acc
+            | exception Not_found ->
+              if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
+              acc
+          ) acc spopt
+      else acc
+    ) [] lpj projs
 
 let pr_cs_pattern = function
     Const_cs c -> Nametab.pr_global_env Id.Set.empty c
@@ -296,7 +302,7 @@ let check_and_decompose_canonical_structure env sigma ref =
     with Not_found ->
       error_not_structure ref
         (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in
-  let ntrue_projs = List.count snd s.s_PROJKIND in
+  let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (sp,indsp)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index f0594d513a..25b6cd0751 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -17,14 +17,20 @@ open Constr
 (** A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
+type proj_kind = {
+  pk_name: Name.t;
+  pk_true_proj: bool;
+  pk_canonical: bool;
+}
+
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (Name.t * bool) list;
+  s_PROJKIND : proj_kind list;
   s_PROJ : Constant.t option list }
 
 type struc_tuple =
-    constructor * (Name.t * bool) list * Constant.t option list
+    constructor * proj_kind list * Constant.t option list
 
 val register_structure : Environ.env -> struc_tuple -> unit
 val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1871609e18..85e6f51387 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -90,48 +90,43 @@ module ReductionBehaviour = struct
   open Names
   open Libobject
 
-  type t = {
-    b_nargs: int;
-    b_recargs: int list;
-    b_dont_expose_case: bool;
-  }
+  type t = NeverUnfold | UnfoldWhen of when_flags | UnfoldWhenNoMatch of when_flags
+  and when_flags = { recargs : int list ; nargs : int option }
+
+  let more_args_when k { recargs; nargs } =
+    { nargs = Option.map ((+) k) nargs;
+      recargs = List.map ((+) k) recargs;
+    }
+
+  let more_args k = function
+    | NeverUnfold -> NeverUnfold
+    | UnfoldWhen x -> UnfoldWhen (more_args_when k x)
+    | UnfoldWhenNoMatch x -> UnfoldWhenNoMatch (more_args_when k x)
 
   let table =
     Summary.ref (GlobRef.Map.empty : t GlobRef.Map.t) ~name:"reductionbehaviour"
 
-  type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
-  type req =
-    | ReqLocal
-    | ReqGlobal of GlobRef.t * (int list * int * flag list)
-
   let load _ (_,(_,(r, b))) =
     table := GlobRef.Map.add r b !table
 
   let cache o = load 1 o
 
-  let classify = function
-    | ReqLocal, _ -> Dispose
-    | ReqGlobal _, _ as o -> Substitute o
+  let classify (local,_ as o) = if local then Dispose else Substitute o
 
-  let subst (subst, (_, (r,o as orig))) =
-    ReqLocal,
-    let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
+  let subst (subst, (local, (r,o) as orig)) =
+    let r' = subst_global_reference subst r in if r==r' then orig
+    else (local,(r',o))
 
   let discharge = function
-    | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) ->
+    | _,(false, (gr, b)) ->
       let b =
         if Lib.is_in_section gr then
           let vars = Lib.variable_section_segment_of_reference gr in
           let extra = List.length vars in
-          let nargs' =
-             if b.b_nargs = max_int then max_int
-             else if b.b_nargs < 0 then b.b_nargs
-             else b.b_nargs + extra in
-          let recargs' = List.map ((+) extra) b.b_recargs in
-          { b with b_nargs = nargs'; b_recargs = recargs' }
+          more_args extra b
         else b
       in
-      Some (ReqGlobal (gr, req), (ConstRef c, b))
+      Some (false, (gr, b))
     | _ -> None
 
   let rebuild = function
@@ -148,55 +143,45 @@ module ReductionBehaviour = struct
 			rebuild_function = rebuild;
 		      }
 
-  let set local r (recargs, nargs, flags as req) =
-    let nargs = if List.mem `ReductionNeverUnfold flags then max_int else nargs in
-    let behaviour = {
-      b_nargs = nargs; b_recargs = recargs;
-      b_dont_expose_case = List.mem `ReductionDontExposeCase flags } in
-    let req = if local then ReqLocal else ReqGlobal (r, req) in
-    Lib.add_anonymous_leaf (inRedBehaviour (req, (r, behaviour)))
-  ;;
+  let set ~local r b =
+    Lib.add_anonymous_leaf (inRedBehaviour (local, (r, b)))
 
-  let get r =
-    try
-      let b = GlobRef.Map.find r !table in
-      let flags =
-	if Int.equal b.b_nargs max_int then [`ReductionNeverUnfold]
-	else if b.b_dont_expose_case then [`ReductionDontExposeCase] else [] in
-      Some (b.b_recargs, (if Int.equal b.b_nargs max_int then -1 else b.b_nargs), flags)
-    with Not_found -> None
+  let get r = GlobRef.Map.find_opt r !table
 
   let print ref =
     let open Pp in
     let pr_global = Nametab.pr_global_env Id.Set.empty in
     match get ref with
     | None -> mt ()
-    | Some (recargs, nargs, flags) ->
-       let never = List.mem `ReductionNeverUnfold flags in
-       let nomatch = List.mem `ReductionDontExposeCase flags in
-       let pp_nomatch = spc() ++ if nomatch then
-				   str "but avoid exposing match constructs" else str"" in
-       let pp_recargs = spc() ++ str "when the " ++
+    | Some b ->
+       let pp_nomatch = spc () ++ str "but avoid exposing match constructs" in
+       let pp_recargs recargs = spc() ++ str "when the " ++
 			  pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (String.plural (List.length recargs) " argument") ++
 			  str (String.plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
 			  str " to a constructor" in
-       let pp_nargs =
-	 spc() ++ str "when applied to " ++ int nargs ++
-	   str (String.plural nargs " argument") in
-       hov 2 (str "The reduction tactics " ++
-		 match recargs, nargs, never with
-		 | _,_, true -> str "never unfold " ++ pr_global ref
-		 | [], 0, _ -> str "always unfold " ++ pr_global ref
-		 | _::_, n, _ when n < 0 ->
-		    str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
-		 | _::_, n, _ when n > List.fold_left max 0 recargs ->
-		    str "unfold " ++ pr_global ref ++ pp_recargs ++
-		      str " and" ++ pp_nargs ++ pp_nomatch
-		 | _::_, _, _ ->
-		    str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
-		 | [], n, _ when n > 0 ->
-		    str "unfold " ++ pr_global ref ++ pp_nargs ++ pp_nomatch
-		 | _ -> str "unfold " ++ pr_global ref ++ pp_nomatch )
+       let pp_nargs nargs =
+         spc() ++ str "when applied to " ++ int nargs ++
+         str (String.plural nargs " argument") in
+       let pp_when = function
+         | { recargs = []; nargs = Some 0 } ->
+           str "always unfold " ++ pr_global ref
+         | { recargs = []; nargs = Some n } ->
+           str "unfold " ++ pr_global ref ++ pp_nargs n
+         | { recargs = []; nargs = None } ->
+           str "unfold " ++ pr_global ref
+         | { recargs; nargs = Some n } when n > List.fold_left max 0 recargs ->
+           str "unfold " ++ pr_global ref ++ pp_recargs recargs ++
+           str " and" ++ pp_nargs n
+         | { recargs; nargs = _ } ->
+           str "unfold " ++ pr_global ref ++ pp_recargs recargs
+       in
+       let pp_behavior = function
+         | NeverUnfold -> str "never unfold " ++ pr_global ref
+         | UnfoldWhen x -> pp_when x
+         | UnfoldWhenNoMatch x -> pp_when x ++ pp_nomatch
+       in
+       hov 2 (str "The reduction tactics " ++ pp_behavior b)
+
 end
 
 (** Machinery about stack of unfolded constants *)
@@ -928,6 +913,7 @@ let equal_stacks sigma (x, l) (y, l') =
 
 let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let open Context.Named.Declaration in
+  let open ReductionBehaviour in
   let rec whrec cst_l (x, stack) =
     let () = if !debug_RAKAM then
 	let open Pp in
@@ -974,37 +960,42 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
           else (* Looks for ReductionBehaviour *)
             match ReductionBehaviour.get (Globnames.ConstRef c) with
             | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
-            | Some (recargs, nargs, flags) ->
-              if (List.mem `ReductionNeverUnfold flags
-                  || (nargs > 0 && Stack.args_size stack < nargs))
-              then fold ()
-              else (* maybe unfolds *)
-              if List.mem `ReductionDontExposeCase flags then
-                let app_sk,sk = Stack.strip_app stack in
-                let (tm',sk'),cst_l' =
-                  whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
-                in
-                let rec is_case x = match EConstr.kind sigma x with
-                  | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
-                  | App (hd, _) -> is_case hd
-                  | Case _ -> true
-                  | _ -> false in
-                if equal_stacks sigma (x, app_sk) (tm', sk')
-                || Stack.will_expose_iota sk'
-                || is_case tm'
-                then fold ()
-                else whrec cst_l' (tm', sk' @ sk)
-              else match recargs with
-                |[] -> (* if nargs has been specified *)
-                  (* CAUTION : the constant is NEVER refold
-                                          (even when it hides a (co)fix) *)
-                  whrec cst_l (body, stack)
-                |curr::remains -> match Stack.strip_n_app curr stack with
-                              | None -> fold ()
-                              | Some (bef,arg,s') ->
-                                whrec Cst_stack.empty
-                                        (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
-         end
+            | Some behavior ->
+              begin match behavior with
+              | NeverUnfold -> fold ()
+              | (UnfoldWhen { nargs = Some n } |
+                 UnfoldWhenNoMatch { nargs = Some n } )
+                when Stack.args_size stack < n ->
+                fold ()
+              | UnfoldWhenNoMatch { recargs } -> (* maybe unfolds *)
+                  let app_sk,sk = Stack.strip_app stack in
+                  let (tm',sk'),cst_l' =
+                    whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
+                  in
+                  let rec is_case x = match EConstr.kind sigma x with
+                    | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+                    | App (hd, _) -> is_case hd
+                    | Case _ -> true
+                    | _ -> false in
+                  if equal_stacks sigma (x, app_sk) (tm', sk')
+                  || Stack.will_expose_iota sk'
+                  || is_case tm'
+                  then fold ()
+                  else whrec cst_l' (tm', sk' @ sk)
+              | UnfoldWhen { recargs } -> (* maybe unfolds *)
+                begin match recargs with
+                  |[] -> (* if nargs has been specified *)
+                    (* CAUTION : the constant is NEVER refold
+                                            (even when it hides a (co)fix) *)
+                    whrec cst_l (body, stack)
+                  |curr::remains -> match Stack.strip_n_app curr stack with
+                    | None -> fold ()
+                    | Some (bef,arg,s') ->
+                      whrec Cst_stack.empty
+                        (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
+                end
+              end
+        end
        | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack ->
           let kargs = CPrimitives.kind p in
           let (kargs,o) = Stack.get_next_primitive_args kargs stack in
@@ -1015,41 +1006,45 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       else fold ()
     | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
       (let npars = Projection.npars p in
-         if not tactic_mode then
-           let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
-	     whrec Cst_stack.empty stack'
-         else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with
-	 | None ->
+       if not tactic_mode then
+         let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
+         whrec Cst_stack.empty stack'
+       else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with
+         | None ->
            let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
-	   let stack'', csts = whrec Cst_stack.empty stack' in
-	     if equal_stacks sigma stack' stack'' then fold ()
-	     else stack'', csts
-	 | Some (recargs, nargs, flags) ->
-	   if (List.mem `ReductionNeverUnfold flags
-	       || (nargs > 0 && Stack.args_size stack < (nargs - (npars + 1))))
-	   then fold ()
-	   else
-	     let recargs = List.map_filter (fun x -> 
-	       let idx = x - npars in 
-		 if idx < 0 then None else Some idx) recargs
-	     in
-	       match recargs with
-	       |[] -> (* if nargs has been specified *)
-		(* CAUTION : the constant is NEVER refold
-                   (even when it hides a (co)fix) *)
+           let stack'', csts = whrec Cst_stack.empty stack' in
+           if equal_stacks sigma stack' stack'' then fold ()
+           else stack'', csts
+         | Some behavior ->
+           begin match behavior with
+             | NeverUnfold -> fold ()
+             | (UnfoldWhen { nargs = Some n }
+               | UnfoldWhenNoMatch { nargs = Some n })
+               when Stack.args_size stack < n - (npars + 1) -> fold ()
+             | UnfoldWhen { recargs }
+             | UnfoldWhenNoMatch { recargs }-> (* maybe unfolds *)
+               let recargs = List.map_filter (fun x ->
+                   let idx = x - npars in
+                   if idx < 0 then None else Some idx) recargs
+               in
+               match recargs with
+               |[] -> (* if nargs has been specified *)
+                 (* CAUTION : the constant is NEVER refold
+                                  (even when it hides a (co)fix) *)
                  let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
-		   whrec Cst_stack.empty(* cst_l *) stack'
-	       | curr::remains -> 
-		 if curr == 0 then (* Try to reduce the record argument *)
-		   whrec Cst_stack.empty 
-		     (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack)
-		 else
-		   match Stack.strip_n_app curr stack with
-		   | None -> fold ()
-		   | Some (bef,arg,s') ->
-		     whrec Cst_stack.empty 
-		       (arg,Stack.Cst(Stack.Cst_proj p,curr,remains,
-				      Stack.append_app [|c|] bef,cst_l)::s'))
+                 whrec Cst_stack.empty(* cst_l *) stack'
+               | curr::remains ->
+                 if curr == 0 then (* Try to reduce the record argument *)
+                   whrec Cst_stack.empty
+                     (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack)
+                 else
+                   match Stack.strip_n_app curr stack with
+                   | None -> fold ()
+                   | Some (bef,arg,s') ->
+                     whrec Cst_stack.empty
+                       (arg,Stack.Cst(Stack.Cst_proj p,curr,remains,
+                                      Stack.append_app [|c|] bef,cst_l)::s')
+           end)
 
     | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
       apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack
@@ -1675,7 +1670,7 @@ let is_sort env sigma t =
 (* reduction to head-normal-form allowing delta/zeta only in argument
    of case/fix (heuristic used by evar_conv) *)
 
-let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
+let whd_betaiota_deltazeta_for_iota_state ts env sigma s =
   let refold = false in
   let tactic_mode = false in
   let rec whrec csts s =
@@ -1696,7 +1691,8 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
           whrec Cst_stack.empty (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'')
 	else s,csts'
       |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s,csts'
-  in whrec csts s
+  in
+  fst (whrec Cst_stack.empty s)
 
 let find_conclusion env sigma =
   let rec decrec env c =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 5938d9b367..aa39921ea2 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -21,13 +21,12 @@ exception Elimconst
 
 (** Machinery to customize the behavior of the reduction *)
 module ReductionBehaviour : sig
-  type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
 
-(** [set is_local ref (recargs, nargs, flags)] *)
-  val set :
-    bool -> GlobRef.t -> (int list * int * flag list) -> unit
-  val get :
-    GlobRef.t -> (int list * int * flag list) option
+  type t = NeverUnfold | UnfoldWhen of when_flags | UnfoldWhenNoMatch of when_flags
+  and when_flags = { recargs : int list ; nargs : int option }
+
+  val set : local:bool -> GlobRef.t -> t -> unit
+  val get : GlobRef.t -> t option
   val print : GlobRef.t -> Pp.t
 end
 
@@ -312,8 +311,7 @@ val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 (** {6 Heuristic for Conversion with Evar } *)
 
 val whd_betaiota_deltazeta_for_iota_state :
-  TransparentState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
-  state * Cst_stack.t
+  TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
 
 (** {6 Meta-related reduction functions } *)
 val meta_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index bcc20a41b4..231219c9de 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -664,18 +664,38 @@ let whd_nothing_for_iota env sigma s =
    it fails if no redex is around *)
 
 let rec red_elim_const env sigma ref u largs =
+  let open ReductionBehaviour in
   let nargs = List.length largs in
   let largs, unfold_anyway, unfold_nonelim, nocase =
     match recargs ref with
     | None -> largs, false, false, false
-    | Some (_,n,f) when nargs < n || List.mem `ReductionNeverUnfold f -> raise Redelimination
-    | Some (x::l,_,_) when nargs <= List.fold_left max x l -> raise Redelimination
-    | Some (l,n,f) ->
-        let is_empty = match l with [] -> true | _ -> false in
-	  reduce_params env sigma largs l, 
-	  n >= 0 && is_empty && nargs >= n,
-          n >= 0 && not is_empty && nargs >= n,
-	  List.mem `ReductionDontExposeCase f
+    | Some NeverUnfold -> raise Redelimination
+    | Some (UnfoldWhen { nargs = Some n } | UnfoldWhenNoMatch { nargs = Some n })
+      when nargs < n -> raise Redelimination
+    | Some (UnfoldWhen { recargs = x::l } | UnfoldWhenNoMatch { recargs = x::l })
+      when nargs <= List.fold_left max x l -> raise Redelimination
+    | Some (UnfoldWhen { recargs; nargs = None }) ->
+      reduce_params env sigma largs recargs,
+      false,
+      false,
+      false
+    | Some (UnfoldWhenNoMatch { recargs; nargs = None }) ->
+      reduce_params env sigma largs recargs,
+      false,
+      false,
+      true
+    | Some (UnfoldWhen { recargs; nargs = Some n }) ->
+      let is_empty = List.is_empty recargs in
+      reduce_params env sigma largs recargs,
+      is_empty && nargs >= n,
+      not is_empty && nargs >= n,
+      false
+    | Some (UnfoldWhenNoMatch { recargs; nargs = Some n }) ->
+      let is_empty = List.is_empty recargs in
+      reduce_params env sigma largs recargs,
+      is_empty && nargs >= n,
+      not is_empty && nargs >= n,
+      true
   in
   try match reference_eval env sigma ref with
     | EliminationCases n when nargs >= n ->
@@ -737,6 +757,7 @@ and reduce_params env sigma stack l =
    a reducible iota/fix/cofix redex (the "simpl" tactic) *)
 
 and whd_simpl_stack env sigma =
+  let open ReductionBehaviour in
   let rec redrec s =
     let (x, stack) = decompose_app_vect sigma s in
     let stack = Array.to_list stack in
@@ -761,30 +782,30 @@ and whd_simpl_stack env sigma =
 	  with Redelimination -> s')
 
       | Proj (p, c) ->
-        (try 
-	   let unf = Projection.unfolded p in
-	     if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
-               let npars = Projection.npars p in
- 		 (match unf, ReductionBehaviour.get (ConstRef (Projection.constant p)) with
- 		 | false, Some (l, n, f) when List.mem `ReductionNeverUnfold f -> 
-                   (* simpl never *) s'
-		 | false, Some (l, n, f) when not (List.is_empty l) ->
-		   let l' = List.map_filter (fun i -> 
-                     let idx = (i - (npars + 1)) in
-		       if idx < 0 then None else Some idx) l in
-		   let stack = reduce_params env sigma stack l' in
-                     (match reduce_projection env sigma p ~npars
-		       (whd_construct_stack env sigma c) stack 
-		      with
-		      | Reduced s' -> redrec (applist s')
-		      | NotReducible -> s')
- 		 | _ ->
-                   match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with
-		   | Reduced s' -> redrec (applist s')
-		   | NotReducible -> s')
-	   else s'
-	 with Redelimination -> s')
-	  
+        (try
+           let unf = Projection.unfolded p in
+           if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
+             let npars = Projection.npars p in
+             (match unf, get (ConstRef (Projection.constant p)) with
+              | false, Some NeverUnfold -> s'
+              | false, Some (UnfoldWhen { recargs } | UnfoldWhenNoMatch { recargs })
+                when not (List.is_empty recargs) ->
+                let l' = List.map_filter (fun i ->
+                    let idx = (i - (npars + 1)) in
+                    if idx < 0 then None else Some idx) recargs in
+                let stack = reduce_params env sigma stack l' in
+                (match reduce_projection env sigma p ~npars
+                         (whd_construct_stack env sigma c) stack
+                 with
+                 | Reduced s' -> redrec (applist s')
+                 | NotReducible -> s')
+              | _ ->
+                match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with
+                | Reduced s' -> redrec (applist s')
+                            | NotReducible -> s')
+                 else s'
+               with Redelimination -> s')
+
       | _ -> 
         match match_eval_ref env sigma x stack with
 	| Some (ref, u) ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9ba51dcfa9..d134c7319f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -489,8 +489,8 @@ let unfold_projection env p stk =
 let expand_key ts env sigma = function
   | Some (IsKey k) -> Option.map EConstr.of_constr (expand_table_key env k)
   | Some (IsProj (p, c)) -> 
-    let red = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
-                               Cst_stack.empty (c, unfold_projection env p [])))
+    let red = Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state ts env sigma
+                               (c, unfold_projection env p []))
     in if EConstr.eq_constr sigma (EConstr.mkProj (p, c)) red then None else Some red
   | None -> None
 
@@ -597,8 +597,8 @@ let constr_cmp pb env sigma flags t u =
     None
     
 let do_reduce ts (env, nb) sigma c =
-  Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
-		  ts env sigma Cst_stack.empty (c, Stack.empty)))
+  Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state
+                  ts env sigma (c, Stack.empty))
 
 let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
   | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 62e9e477f7..1fe6545ce4 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -202,7 +202,7 @@ and nf_univ_args ~nb_univs mk env sigma stk =
 and nf_evar env sigma evk stk =
   let evi = try Evd.find sigma evk with Not_found -> assert false in
   let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
-  let concl = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in
+  let concl = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in
   if List.is_empty hyps then
     nf_stk env sigma (mkEvar (evk, [||])) concl stk
   else match stk with