25 files changed, 396 insertions, 336 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a793e217d4..d2859b1b4e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -46,8 +46,10 @@ module NamedDecl = Context.Named.Declaration
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor * int
-  | WrongNumargInductive of inductive * int
+  | WrongNumargConstructor of
+      {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
+  | WrongNumargInductive of
+      {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
   | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
@@ -65,11 +67,13 @@ let error_bad_constructor ?loc env cstr ind =
   raise_pattern_matching_error ?loc
     (env, Evd.empty, BadConstructor (cstr,ind))
 
-let error_wrong_numarg_constructor ?loc env c n =
-  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,n))
+let error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls =
+  raise_pattern_matching_error ?loc (env, Evd.empty,
+    WrongNumargConstructor {cstr; expanded; nargs; expected_nassums; expected_ndecls})
 
-let error_wrong_numarg_inductive ?loc env c n =
-  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n))
+let error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls =
+  raise_pattern_matching_error ?loc (env, Evd.empty,
+    WrongNumargInductive {ind; expanded; nargs; expected_nassums; expected_ndecls})
 
 let list_try_compile f l =
   let rec aux errors = function
@@ -519,13 +523,18 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with
         (* Check the constructor has the right number of args *)
         let ci = cstrs.(i-1) in
         let nb_args_constr = ci.cs_nargs in
-        if Int.equal (List.length args) nb_args_constr then pat
+        let nargs = List.length args in
+        if Int.equal nargs nb_args_constr then pat
         else
           try
             let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args)
             in DAst.make ?loc @@ PatCstr (cstr, args', alias)
           with NotAdjustable ->
-            error_wrong_numarg_constructor ?loc env cstr nb_args_constr
+            let nlet = List.count (function LocalDef _ -> true | _ -> false) ci.cs_args in
+            (* In practice, this is already checked at interning *)
+            error_wrong_numarg_constructor ?loc env ~cstr
+              (* as if not expanded: *) ~expanded:false ~nargs ~expected_nassums:nb_args_constr
+              ~expected_ndecls:(nb_args_constr + nlet)
       else
         (* Try to insert a coercion *)
         try
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9a986bc14c..ade1fbf3d3 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -23,17 +23,21 @@ open Evardefine
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor * int
-  | WrongNumargInductive of inductive * int
+  | WrongNumargConstructor of
+      {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
+  | WrongNumargInductive of
+      {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
   | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
 
 exception PatternMatchingError of env * evar_map * pattern_matching_error
 
-val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a
+val error_wrong_numarg_constructor :
+  ?loc:Loc.t -> env -> cstr:constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
 
-val error_wrong_numarg_inductive   : ?loc:Loc.t -> env -> inductive -> int -> 'a
+val error_wrong_numarg_inductive :
+  ?loc:Loc.t -> env -> ind:inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
 
 val irrefutable : env -> cases_pattern -> bool
 
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2661000a39..bada2c3a60 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -111,15 +111,20 @@ let shift_value n v =
  * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
  *    -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
  *)
+
+let rec mk_fix_subs make_body n env i =
+  if Int.equal i n then env
+  else mk_fix_subs make_body n (subs_cons (make_body i) env) (i + 1)
+
 let contract_fixp env ((reci,i),(_,_,bds as bodies)) =
   let make_body j = FIXP(((reci,j),bodies), env, [||]) in
   let n = Array.length bds in
-  subs_cons(Array.init n make_body, env), bds.(i)
+  mk_fix_subs make_body n env 0, bds.(i)
 
 let contract_cofixp env (i,(_,_,bds as bodies)) =
   let make_body j = COFIXP((j,bodies), env, [||]) in
   let n = Array.length bds in
-  subs_cons(Array.init n make_body, env), bds.(i)
+  mk_fix_subs make_body n env 0, bds.(i)
 
 let make_constr_ref n k t =
   match k with
@@ -401,6 +406,10 @@ let rec strip_app = function
   | APP (args,st) -> APP (args,strip_app st)
   | s -> TOP
 
+let rec subs_consn v i n s =
+  if Int.equal i n then s
+  else subs_consn v (i + 1) n (subs_cons v.(i) s)
+
 (* The main recursive functions
  *
  * Go under applications and cases/projections (pushed in the stack),
@@ -456,7 +465,7 @@ let rec norm_head info env t stack =
         (* New rule: for Cbv, Delta does not apply to locally bound variables
            or red_set info.reds fDELTA
          *)
-        let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in
+        let env' = subs_cons (cbv_stack_term info TOP env b) env in
         norm_head info env' c stack
       else
         (CBN(t,env), stack) (* Should we consider a commutative cut ? *)
@@ -526,14 +535,14 @@ and cbv_stack_value info env = function
       when red_set info.reds fBETA ->
     let nargs = Array.length args in
       if nargs == nlams then
-          cbv_stack_term info stk (subs_cons(args,env)) b
+          cbv_stack_term info stk (subs_consn args 0 nargs env) b
         else if nlams < nargs then
-          let env' = subs_cons(Array.sub args 0 nlams, env) in
+          let env' = subs_consn args 0 nlams env in
           let eargs = Array.sub args nlams (nargs-nlams) in
           cbv_stack_term info (APP(eargs,stk)) env' b
         else
           let ctxt' = List.skipn nargs ctxt in
-          LAM(nlams-nargs,ctxt', b, subs_cons(args,env))
+          LAM(nlams-nargs,ctxt', b, subs_consn args 0 nargs env)
 
     (* a Fix applied enough -> IOTA *)
     | (FIXP(fix,env,[||]), stk)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index a3f1c0b004..0e69b814c7 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -528,10 +528,9 @@ let sub_match ?(closed=true) env sigma pat c =
     let sub = subargs env types @ subargs env' bodies in
     try_aux sub next_mk_ctx next
   | Proj (p,c') ->
-    begin try
-      let term = Retyping.expand_projection env sigma p c' [] in
-      aux env term mk_ctx next
-    with Retyping.RetypeError _ -> next ()
+    begin match Retyping.expand_projection env sigma p c' [] with
+    | term -> aux env term mk_ctx next
+    | exception Retyping.RetypeError _ -> next ()
     end
   | Array(u, t, def, ty) ->
     let next_mk_ctx = function
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a12a832f76..402a6f6ed3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -648,26 +648,16 @@ let detype_cofix detype flags avoid env sigma n (names,tys,bodies) =
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-(* TODO use some algebraic type with a case for unnamed univs so we
-   can cleanly detype them. NB: this corresponds to a hack in
-   Pretyping.interp_universe_level_name to convert Foo.xx strings into
-   universes. *)
-let hack_qualid_of_univ_level sigma l =
-  match Termops.reference_of_level sigma l with
-  | Some qid -> qid
-  | None ->
-    let path = String.split_on_char '.' (Univ.Level.to_string l) in
-    let path = List.rev_map Id.of_string_soft path in
-    Libnames.qualid_of_dirpath (DirPath.make path)
+let detype_level_name sigma l =
+  if Univ.Level.is_sprop l then GSProp else
+  if Univ.Level.is_prop l then GProp else
+  if Univ.Level.is_set l then GSet else
+    match UState.id_of_level (Evd.evar_universe_context sigma) l with
+    | Some id -> GLocalUniv (CAst.make id)
+    | None -> GUniv l
 
 let detype_universe sigma u =
-  let fn (l, n) =
-    let s =
-      if Univ.Level.is_prop l then GProp else
-      if Univ.Level.is_set l then GSet else
-      GType (hack_qualid_of_univ_level sigma l) in
-    (s, n) in
-  List.map fn (Univ.Universe.repr u)
+  List.map (on_fst (detype_level_name sigma)) (Univ.Universe.repr u)
 
 let detype_sort sigma = function
   | SProp -> UNamed [GSProp,0]
@@ -684,8 +674,7 @@ type binder_kind = BProd | BLambda | BLetIn
 (* Main detyping function                                             *)
 
 let detype_level sigma l =
-  let l = hack_qualid_of_univ_level sigma l in
-  UNamed (GType l)
+  UNamed (detype_level_name sigma l)
 
 let detype_instance sigma l =
   let l = EInstance.kind sigma l in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b770ae53bd..4b0974ae03 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -455,6 +455,58 @@ let compare_cumulative_instances evd variances u u' =
     Success evd
   | Inr p -> UnifFailure (evd, UnifUnivInconsistency p)
 
+let compare_heads env evd ~nargs term term' =
+    let check_strict evd u u' =
+      let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in
+      try Success (Evd.add_constraints evd cstrs)
+      with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+    in
+      match EConstr.kind evd term, EConstr.kind evd term' with
+      | Const (c, u), Const (c', u') when QConstant.equal env c c' ->
+        if Int.equal nargs 1 && Environ.is_array_type env c
+        then
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u'
+        else
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          check_strict evd u u'
+      | Const _, Const _ -> UnifFailure (evd, NotSameHead)
+      | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' ->
+        if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+        else
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          let mind = Environ.lookup_mind mi env in
+          let open Declarations in
+          begin match mind.mind_variance with
+            | None -> check_strict evd u u'
+            | Some variances ->
+              let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
+              if not (Int.equal nargs needed)
+              then check_strict evd u u'
+              else
+                compare_cumulative_instances evd variances u u'
+          end
+      | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
+      | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
+        when Names.Construct.CanOrd.equal cons cons' ->
+        if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+        else
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          let mind = Environ.lookup_mind mi env in
+          let open Declarations in
+          begin match mind.mind_variance with
+            | None -> check_strict evd u u'
+            | Some variances ->
+              let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
+              if not (Int.equal nargs needed)
+              then check_strict evd u u'
+              else
+                Success (compare_constructor_instances evd u u')
+          end
+      | Construct _, Construct _ -> UnifFailure (evd, NotSameHead)
+      | _, _ -> anomaly (Pp.str "")
+
+
 let conv_fun f flags on_types =
   let typefn env evd pbty term1 term2 =
     let flags = { (default_flags env) with
@@ -567,65 +619,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     else evar_eqappr_x flags env' evd CONV out2 out1
   in
   let rigids env evd sk term sk' term' =
-    let check_strict evd u u' =
-      let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in
-      try Success (Evd.add_constraints evd cstrs)
-      with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
-    in
-    let compare_heads evd =
-      match EConstr.kind evd term, EConstr.kind evd term' with
-      | Const (c, u), Const (c', u') when QConstant.equal env c c' ->
-        if Int.equal (Stack.args_size sk) 1 && Environ.is_array_type env c
-        then
-          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
-          compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u'
-        else
-          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
-          check_strict evd u u'
-      | Const _, Const _ -> UnifFailure (evd, NotSameHead)
-      | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' ->
-        if EInstance.is_empty u && EInstance.is_empty u' then Success evd
-        else
-          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
-          let mind = Environ.lookup_mind mi env in
-          let open Declarations in
-          begin match mind.mind_variance with
-            | None -> check_strict evd u u'
-            | Some variances ->
-              let nparamsaplied = Stack.args_size sk in
-              let nparamsaplied' = Stack.args_size sk' in
-              let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
-              if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
-              then check_strict evd u u'
-              else
-                compare_cumulative_instances evd variances u u'
-          end
-      | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
-      | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
-        when Names.Construct.CanOrd.equal cons cons' ->
-        if EInstance.is_empty u && EInstance.is_empty u' then Success evd
-        else
-          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
-          let mind = Environ.lookup_mind mi env in
-          let open Declarations in
-          begin match mind.mind_variance with
-            | None -> check_strict evd u u'
-            | Some variances ->
-              let nparamsaplied = Stack.args_size sk in
-              let nparamsaplied' = Stack.args_size sk' in
-              let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
-              if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
-              then check_strict evd u u'
-              else
-                Success (compare_constructor_instances evd u u')
-          end
-      | Construct _, Construct _ -> UnifFailure (evd, NotSameHead)
-      | _, _ -> anomaly (Pp.str "")
-    in
-    ise_and evd [(fun i ->
-                try compare_heads i
-                with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
-                 (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')]
+    let nargs = Stack.args_size sk in
+    let nargs' = Stack.args_size sk' in
+    if not (Int.equal nargs nargs') then UnifFailure (evd, NotSameArgSize)
+    else
+      ise_and evd [(fun i ->
+          try compare_heads env i ~nargs term term'
+          with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
+         (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')]
   in
   let consume l2r (_, skF as apprF) (_,skM as apprM) i =
     if not (Stack.is_empty skF && Stack.is_empty skM) then
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index a5a8d1f916..be03ced7eb 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -84,6 +84,12 @@ val check_conv_record : env -> evar_map ->
     (constr Stack.t * constr Stack.t) * constr *
     (int option * constr)
 
+(** Compares two constants/inductives/constructors unifying their universes.
+   It required the number of arguments applied to the c/i/c in order to decided
+   the kind of check it must perform. *)
+val compare_heads : env -> evar_map ->
+  nargs:int -> EConstr.t -> EConstr.t -> Evarsolve.unification_result
+
 (** Try to solve problems of the form ?x[args] = c by second-order
     matching, using typing to select occurrences *)
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index bd717e2d1f..52e3364109 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -21,42 +21,15 @@ module NamedDecl = Context.Named.Declaration
 
 (** Processing occurrences *)
 
-type occurrence_error =
-  | InvalidOccurrence of int list
-  | IncorrectInValueOccurrence of Id.t
-
-let explain_invalid_occurrence l =
-  let l = List.sort_uniquize Int.compare l in
-  str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ")
-  ++ prlist_with_sep spc int l ++ str "."
-
 let explain_incorrect_in_value_occurrence id =
   Id.print id ++ str " has no value."
 
-let explain_occurrence_error = function
-  | InvalidOccurrence l -> explain_invalid_occurrence l
-  | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
-
-let error_occurrences_error e =
-  user_err  (explain_occurrence_error e)
-
-let error_invalid_occurrence occ =
-  error_occurrences_error (InvalidOccurrence occ)
-
-let check_used_occurrences nbocc (nowhere_except_in,locs) =
-  let rest = List.filter (fun o -> o >= nbocc) locs in
-  match rest with
-  | [] -> ()
-  | _ -> error_occurrences_error (InvalidOccurrence rest)
-
 let proceed_with_occurrences f occs x =
   match occs with
   | NoOccurrences -> x
   | occs ->
-    let plocs = Locusops.convert_occs occs in
-    assert (List.for_all (fun x -> x >= 0) (snd plocs));
-    let (nbocc,x) = f 1 x in
-    check_used_occurrences nbocc plocs;
+    let (occs,x) = f (Locusops.initialize_occurrence_counter occs) x in
+    Locusops.check_used_occurrences occs;
     x
 
 (** Applying a function over a named_declaration with an hypothesis
@@ -70,7 +43,7 @@ let map_named_declaration_with_hyploc f hyploc acc decl =
   in
   match decl,hyploc with
   | LocalAssum (id,_), InHypValueOnly ->
-      error_occurrences_error (IncorrectInValueOccurrence id.Context.binder_name)
+      user_err (explain_incorrect_in_value_occurrence id.Context.binder_name)
   | LocalAssum (id,typ), _ ->
       let acc,typ = f acc typ in acc, LocalAssum (id,typ)
   | LocalDef (id,body,typ), InHypTypeOnly ->
@@ -101,43 +74,43 @@ type 'a testing_function = {
    means all occurrences except the ones in l *)
 
 let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
-  let (nowhere_except_in,locs) = Locusops.convert_occs occs in
-  let maxocc = List.fold_right max locs 0 in
-  let pos = ref occ in
+  let count = ref (Locusops.initialize_occurrence_counter occs) in
   let nested = ref false in
-  let add_subst t subst =
+  let add_subst pos t subst =
     try
       test.testing_state <- test.merge_fun subst test.testing_state;
-      test.last_found <- Some ((cl,!pos),t)
+      test.last_found <- Some ((cl,pos),t)
     with NotUnifiable e when not like_first ->
       let lastpos = Option.get test.last_found in
-     raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in
+     raise (SubtermUnificationError (!nested,((cl,pos),t),lastpos,e)) in
   let rec substrec k t =
-    if nowhere_except_in && !pos > maxocc then t else
+    if Locusops.occurrences_done !count then t else
     try
       let subst = test.match_fun test.testing_state t in
-      if Locusops.is_selected !pos occs then
+      let selected, count' = Locusops.update_occurrence_counter !count in count := count';
+      if selected then
+        let pos = Locusops.current_occurrence !count in
         (if !nested then begin
           (* in case it is nested but not later detected as unconvertible,
              as when matching "id _" in "id (id 0)" *)
           let lastpos = Option.get test.last_found in
-          raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,None))
+          raise (SubtermUnificationError (!nested,((cl,pos),t),lastpos,None))
          end;
-         add_subst t subst; incr pos;
+         add_subst pos t subst;
          (* Check nested matching subterms *)
-         if not (Locusops.is_all_occurrences occs) && occs != Locus.NoOccurrences then
+         if Locusops.more_specific_occurrences !count then
            begin nested := true; ignore (subst_below k t); nested := false end;
          (* Do the effective substitution *)
          Vars.lift k (bywhat ()))
       else
-        (incr pos; subst_below k t)
+        subst_below k t
     with NotUnifiable _ ->
       subst_below k t
   and subst_below k t =
     map_constr_with_binders_left_to_right sigma (fun d k -> k+1) substrec k t
   in
   let t' = substrec 0 t in
-  (!pos, t')
+  (!count, t')
 
 let replace_term_occ_modulo evd occs test bywhat t =
   let occs',like_first =
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 436b730a88..1ddae01e2b 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -65,6 +65,3 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
 val subst_closed_term_occ_decl : env -> evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
   constr -> named_declaration -> named_declaration * evar_map
-
-(** Miscellaneous *)
-val error_invalid_occurrence : int list -> 'a
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index f42c754ef5..86d2cc78e0 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -48,8 +48,10 @@ let glob_sort_name_eq g1 g2 = match g1, g2 with
   | GSProp, GSProp
   | GProp, GProp
   | GSet, GSet -> true
-  | GType u1, GType u2 -> Libnames.qualid_eq u1 u2
-  | (GSProp|GProp|GSet|GType _), _ -> false
+  | GUniv u1, GUniv u2 -> Univ.Level.equal u1 u2
+  | GLocalUniv u1, GLocalUniv u2 -> lident_eq u1 u2
+  | GRawUniv u1, GRawUniv u2 -> Univ.Level.equal u1 u2
+  | (GSProp|GProp|GSet|GUniv _|GLocalUniv _|GRawUniv _), _ -> false
 
 exception ComplexSort
 
@@ -60,19 +62,23 @@ let glob_sort_family = let open Sorts in function
   | UNamed [GSet,0] -> InSet
   | _ -> raise ComplexSort
 
-let glob_sort_expr_eq f u1 u2 =
+let map_glob_sort_gen f = function
+  | UNamed l -> UNamed (f l)
+  | UAnonymous _ as x -> x
+
+let glob_sort_gen_eq f u1 u2 =
  match u1, u2 with
   | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2
   | UNamed l1, UNamed l2 -> f l1 l2
   | (UNamed _ | UAnonymous _), _ -> false
 
 let glob_sort_eq u1 u2 =
-  glob_sort_expr_eq
+  glob_sort_gen_eq
     (List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n))
     u1 u2
 
 let glob_level_eq u1 u2 =
-  glob_sort_expr_eq glob_sort_name_eq u1 u2
+  glob_sort_gen_eq glob_sort_name_eq u1 u2
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Explicit, Explicit -> true
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 6da8173dce..5ad1a207f3 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -11,8 +11,12 @@
 open Names
 open Glob_term
 
+val map_glob_sort_gen : ('a -> 'b) -> 'a glob_sort_gen -> 'b glob_sort_gen
+
 (** Equalities *)
 
+val glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a glob_sort_gen -> 'a glob_sort_gen -> bool
+
 val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
 
 val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index a49c8abe26..9f93e5e6c1 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -26,17 +26,23 @@ type glob_sort_name =
   | GSProp (** representation of [SProp] literal *)
   | GProp (** representation of [Prop] level *)
   | GSet  (** representation of [Set] level *)
-  | GType of Libnames.qualid (** representation of a [Type] level *)
+  | GUniv of Univ.Level.t
+  | GLocalUniv of lident (** Locally bound universes (may also be nonstrict declaration) *)
+  | GRawUniv of Univ.Level.t
+  (** Hack for funind, DO NOT USE
 
-type 'a glob_sort_expr =
+      Note that producing the similar Constrexpr.CRawType for printing
+      is OK, just don't try to reinterp it. *)
+
+type 'a glob_sort_gen =
   | UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *)
   | UNamed of 'a
 
 (** levels, occurring in universe instances *)
-type glob_level = glob_sort_name glob_sort_expr
+type glob_level = glob_sort_name glob_sort_gen
 
 (** sort expressions *)
-type glob_sort = (glob_sort_name * int) list glob_sort_expr
+type glob_sort = (glob_sort_name * int) list glob_sort_gen
 
 type glob_constraint = glob_sort_name * Univ.constraint_type * glob_sort_name
 
@@ -131,7 +137,7 @@ type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g
 
 type 'a extended_glob_local_binder_r =
   | GLocalAssum   of Name.t * binding_kind * 'a glob_constr_g
-  | GLocalDef     of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option
+  | GLocalDef     of Name.t * 'a glob_constr_g * 'a glob_constr_g option
   | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g
 and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 23145b1629..bd875cf68b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -245,6 +245,14 @@ let inductive_alldecls env (ind,u) =
 let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u)
 [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"]
 
+let inductive_alltags env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  Context.Rel.to_tags mip.mind_arity_ctxt
+
+let constructor_alltags env (ind,j) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1))
+
 let constructor_has_local_defs env (indsp,j) =
   let (mib,mip) = Inductive.lookup_mind_specif env indsp in
   let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 1e2bba9f73..3705d39280 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -138,6 +138,10 @@ val constructor_nrealdecls : env -> constructor -> int
 val constructor_nrealdecls_env : env -> constructor -> int
 [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"]
 
+(** @return tags of all decls: true = assumption, false = letin *)
+val inductive_alltags : env -> inductive -> bool list
+val constructor_alltags : env -> constructor -> bool list
+
 (** Is there local defs in params or args ? *)
 val constructor_has_local_defs : env -> constructor -> bool
 val inductive_has_local_defs : env -> inductive -> bool
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 86352eb79a..256d61a32b 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Util
 open Locus
 
 (** Utilities on or_var *)
@@ -27,12 +28,43 @@ let occurrences_map f = function
     if l' = [] then AllOccurrences else AllOccurrencesBut l'
   | (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o
 
-let convert_occs = function
-  | AtLeastOneOccurrence -> (false,[])
-  | AllOccurrences -> (false,[])
-  | AllOccurrencesBut l -> (false,l)
-  | NoOccurrences -> (true,[])
-  | OnlyOccurrences l -> (true,l)
+type occurrences_count = {current: int; remaining: int list; where: (bool * int)}
+
+let error_invalid_occurrence l =
+  CErrors.user_err Pp.(str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ")
+  ++ prlist_with_sep spc int l ++ str ".")
+
+let initialize_occurrence_counter occs =
+  let (nowhere_except_in,occs) =
+    match occs with
+    | AtLeastOneOccurrence -> (false,[])
+    | AllOccurrences -> (false,[])
+    | AllOccurrencesBut l -> (false,List.sort_uniquize Int.compare l)
+    | NoOccurrences -> (true,[])
+    | OnlyOccurrences l -> (true,List.sort_uniquize Int.compare l) in
+  let max =
+    match occs with
+    | n::_ when n <= 0 -> error_invalid_occurrence [n]
+    | [] -> 0
+    | _ -> Util.List.last occs in
+  {current = 0; remaining = occs; where = (nowhere_except_in,max)}
+
+let update_occurrence_counter {current; remaining; where = (nowhere_except_in,_ as where)} =
+  let current = succ current in
+  match remaining with
+  | occ::remaining when Int.equal current occ -> (nowhere_except_in,{current;remaining;where})
+  | _ -> (not nowhere_except_in,{current;remaining;where})
+
+let check_used_occurrences {remaining} =
+  if not (Util.List.is_empty remaining) then error_invalid_occurrence remaining
+
+let occurrences_done {current; where = (nowhere_except_in,max)} =
+  nowhere_except_in && current > max
+
+let current_occurrence {current} = current
+
+let more_specific_occurrences {current; where = (_,max)} =
+  current <= max
 
 let is_selected occ = function
   | AtLeastOneOccurrence -> true
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index 911ccc1a38..748bfbc252 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -20,13 +20,44 @@ val or_var_map : ('a -> 'b) -> 'a or_var -> 'b or_var
 val occurrences_map :
   ('a list -> 'b list) -> 'a occurrences_gen -> 'b occurrences_gen
 
-(** From occurrences to a list of positions (or complement of positions) *)
-val convert_occs : occurrences -> bool * int list
+(** {6 Counting occurrences} *)
+
+type occurrences_count
+  (** A counter of occurrences associated to a list of occurrences *)
+
+(** Three basic functions to initialize, count, and conclude a loop
+    browsing over subterms *)
+
+val initialize_occurrence_counter : occurrences -> occurrences_count
+  (** Initialize an occurrence_counter *)
+
+val update_occurrence_counter : occurrences_count -> bool * occurrences_count
+  (** Increase the occurrence counter by one and tell if the current occurrence is selected *)
+
+val check_used_occurrences : occurrences_count -> unit
+  (** Increase the occurrence counter and tell if the current occurrence is selected *)
+
+(** Auxiliary functions about occurrence counters *)
+
+val current_occurrence : occurrences_count -> int
+  (** Tell the value of the current occurrence *)
+
+val occurrences_done : occurrences_count -> bool
+  (** Tell if there are no more occurrences to select and if the loop
+      can be shortcut *)
+
+val more_specific_occurrences : occurrences_count -> bool
+  (** Tell if there are no more occurrences to select (or unselect)
+      and if an inner loop can be shortcut *)
+
+(** {6 Miscellaneous} *)
 
 val is_selected : int -> occurrences -> bool
 
 val is_all_occurrences : 'a occurrences_gen -> bool
 
+val error_invalid_occurrence : int list -> 'a
+
 (** Usual clauses *)
 
 val allHypsAndConcl : 'a clause_expr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b70ff20e32..9dbded75ba 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -130,53 +130,32 @@ let is_strict_universe_declarations =
 
 (** Miscellaneous interpretation functions *)
 
-let interp_known_universe_level_name evd qid =
-  try
-    let open Libnames in
-    if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
-    else raise Not_found
-  with Not_found ->
-    let qid = Nametab.locate_universe qid in
-    Univ.Level.make qid
-
-let interp_universe_level_name evd qid =
-  try evd, interp_known_universe_level_name evd qid
+let universe_level_name evd ({CAst.v=id} as lid) =
+  try evd, Evd.universe_of_name evd id
   with Not_found ->
-    if Libnames.qualid_is_ident qid then (* Undeclared *)
-      let id = Libnames.qualid_basename qid in
-      if not (is_strict_universe_declarations ()) then
-        new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd
-      else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
-          (Pp.(str "Undeclared universe: " ++ Id.print id))
-    else
-      let dp, i = Libnames.repr_qualid qid in
-      let num =
-        try int_of_string (Id.to_string i)
-        with Failure _ ->
-          user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
-            (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
-      in
-      let level = Univ.Level.(make (UGlobal.make dp num)) in
-      let evd =
-        try Evd.add_global_univ evd level
-        with UGraph.AlreadyDeclared -> evd
-      in evd, level
+    if not (is_strict_universe_declarations ()) then
+      new_univ_level_variable ?loc:lid.CAst.loc ~name:id univ_rigid evd
+    else user_err ?loc:lid.CAst.loc ~hdr:"universe_level_name"
+        (Pp.(str "Undeclared universe: " ++ Id.print id))
 
-let interp_sort_name sigma = function
+let sort_name sigma = function
   | GSProp -> sigma, Univ.Level.sprop
   | GProp -> sigma, Univ.Level.prop
   | GSet -> sigma, Univ.Level.set
-  | GType l -> interp_universe_level_name sigma l
+  | GUniv u -> sigma, u
+  | GRawUniv u ->
+    (try Evd.add_global_univ sigma u with UGraph.AlreadyDeclared -> sigma), u
+  | GLocalUniv l -> universe_level_name sigma l
 
-let interp_sort_info ?loc evd l =
+let sort_info ?loc evd l =
     List.fold_left (fun (evd, u) (l,n) ->
-      let evd', u' = interp_sort_name evd l in
+      let evd', u' = sort_name evd l in
       let u' = Univ.Universe.make u' in
       let u' = match n with
       | 0 -> u'
       | 1 -> Univ.Universe.super u'
       | n ->
-        user_err ?loc ~hdr:"interp_universe"
+        user_err ?loc ~hdr:"sort_info"
           (Pp.(str "Cannot interpret universe increment +" ++ int n))
       in (evd', Univ.sup u u'))
     (evd, Univ.Universe.type0m) l
@@ -393,24 +372,33 @@ let pretype_id pretype loc env sigma id =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let interp_known_glob_level ?loc evd = function
+let known_universe_level_name evd lid =
+  try Evd.universe_of_name evd lid.CAst.v
+  with Not_found ->
+    let u = Nametab.locate_universe (Libnames.qualid_of_lident lid) in
+    Univ.Level.make u
+
+let known_glob_level evd = function
   | GSProp -> Univ.Level.sprop
   | GProp -> Univ.Level.prop
   | GSet -> Univ.Level.set
-  | GType qid ->
-    try interp_known_universe_level_name evd qid
+  | GUniv u -> u
+  | GRawUniv u -> anomaly Pp.(str "Raw universe in known_glob_level.")
+  | GLocalUniv lid ->
+    try known_universe_level_name evd lid
     with Not_found ->
-      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
+      user_err ?loc:lid.CAst.loc ~hdr:"known_level_info"
+        (str "Undeclared universe " ++ Id.print lid.CAst.v)
 
-let interp_glob_level ?loc evd : glob_level -> _ = function
+let glob_level ?loc evd : glob_level -> _ = function
   | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd
-  | UNamed s -> interp_sort_name evd s
+  | UNamed s -> sort_name evd s
 
-let interp_instance ?loc evd l =
+let instance ?loc evd l =
   let evd, l' =
     List.fold_left
       (fun (evd, univs) l ->
-         let evd, l = interp_glob_level ?loc evd l in
+         let evd, l = glob_level ?loc evd l in
          (evd, l :: univs)) (evd, [])
       l
   in
@@ -424,7 +412,7 @@ let pretype_global ?loc rigid env evd gr us =
   let evd, instance =
     match us with
     | None -> evd, None
-    | Some l -> interp_instance ?loc evd l
+    | Some l -> instance ?loc evd l
   in
   Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr
 
@@ -451,11 +439,11 @@ let pretype_ref ?loc sigma env ref us =
     let sigma, ty = type_of !!env sigma c in
     sigma, make_judge c ty
 
-let interp_sort ?loc evd : glob_sort -> _ = function
+let sort ?loc evd : glob_sort -> _ = function
   | UAnonymous {rigid} ->
     let evd, l = new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd in
     evd, Univ.Universe.make l
-  | UNamed l -> interp_sort_info ?loc evd l
+  | UNamed l -> sort_info ?loc evd l
 
 let judge_of_sort ?loc evd s =
   let judge =
@@ -469,11 +457,22 @@ let pretype_sort ?loc sigma s =
   | UNamed [GProp,0] -> sigma, judge_of_prop
   | UNamed [GSet,0] -> sigma, judge_of_set
   | _ ->
-  let sigma, s = interp_sort ?loc sigma s in
+  let sigma, s = sort ?loc sigma s in
   judge_of_sort ?loc sigma s
 
-let new_type_evar env sigma loc =
-  new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
+let new_typed_evar env sigma ?naming ~src tycon =
+  match tycon with
+  | Some ty ->
+    let sigma, c = new_evar env sigma ~src ?naming ty in
+    sigma, c, ty
+  | None ->
+    let sigma, ty = new_type_evar env sigma ~src in
+    let sigma, c = new_evar env sigma ~src ?naming ty in
+    let evk = fst (destEvar sigma c) in
+    let ido = Evd.evar_ident evk sigma in
+    let src = (fst src,Evar_kinds.EvarType (ido,evk)) in
+    let sigma = update_source sigma (fst (destEvar sigma ty)) src in
+    sigma, c, ty
 
 let mark_obligation_evar sigma k evc =
   match k with
@@ -636,13 +635,9 @@ struct
       discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
 
   let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma =
-    let sigma, ty =
-      match tycon with
-      | Some ty -> sigma, ty
-      | None -> new_type_evar env sigma loc in
     let k = Evar_kinds.MatchingVar kind in
-    let sigma, uj_val = new_evar env sigma ~src:(loc,k) ty in
-    sigma, { uj_val; uj_type = ty }
+    let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) tycon in
+    sigma, { uj_val; uj_type }
 
   let pretype_hole self (k, naming, ext) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -653,19 +648,15 @@ struct
         | IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id)
         | IntroAnonymous -> IntroAnonymous
         | IntroFresh id -> IntroFresh (interp_ltac_id env id) in
-      let sigma, ty =
-        match tycon with
-        | Some ty -> sigma, ty
-        | None -> new_type_evar env sigma loc in
-      let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
+      let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) ~naming tycon in
       let sigma = if program_mode then mark_obligation_evar sigma k uj_val else sigma in
-      sigma, { uj_val; uj_type = ty }
+      sigma, { uj_val; uj_type }
 
     | Some arg ->
       let sigma, ty =
         match tycon with
         | Some ty -> sigma, ty
-        | None -> new_type_evar env sigma loc in
+        | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) in
       let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in
       sigma, { uj_val = c; uj_type = ty }
 
@@ -1144,7 +1135,7 @@ struct
         | None ->
           let sigma, p = match tycon with
             | Some ty -> sigma, ty
-            | None -> new_type_evar env sigma loc
+            | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.CasesType false)
           in
           sigma, it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
       let pred = nf_evar sigma pred in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7bb4a6e273..5668098fe6 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -30,8 +30,7 @@ val get_bidirectionality_hint : GlobRef.t -> int option
 
 val clear_bidirectionality_hint : GlobRef.t -> unit
 
-val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
-  glob_sort_name -> Univ.Level.t
+val known_glob_level : Evd.evar_map -> glob_sort_name -> Univ.Level.t
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b6e44265ae..aa862a912e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -323,23 +323,32 @@ let check_and_decompose_canonical_structure env sigma ref =
 let lookup_canonical_conversion env (proj,pat) =
   assoc_pat env pat (GlobRef.Map.find proj !object_table)
 
-let decompose_projection sigma c args =
+let rec get_nth n = function
+| [] -> raise Not_found
+| arg :: args ->
+  let len = Array.length arg in
+  if n < len then arg.(n)
+  else get_nth (n - len) args
+
+let rec decompose_projection sigma c args =
   match EConstr.kind sigma c with
+  | Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) args
+  | Cast (c, _, _) -> decompose_projection sigma c args
+  | App (c, arg) -> decompose_projection sigma c (arg :: args)
   | Const (c, u) ->
      let n = find_projection_nparams (GlobRef.ConstRef c) in
      (* Check if there is some canonical projection attached to this structure *)
      let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in
-     let arg = Stack.nth args n in
-     arg
+     get_nth n args
   | Proj (p, c) ->
      let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in
      c
   | _ -> raise Not_found
 
-let is_open_canonical_projection env sigma (c,args) =
+let is_open_canonical_projection env sigma c =
   let open EConstr in
   try
-    let arg = decompose_projection sigma c args in
+    let arg = decompose_projection sigma c [] in
     try
       let arg = whd_all env sigma arg in
       let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5b8dc8184a..83927085e9 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -94,7 +94,7 @@ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
   cs -> unit
 val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
 val is_open_canonical_projection :
-  Environ.env -> Evd.evar_map -> Reductionops.state -> bool
+  Environ.env -> Evd.evar_map -> EConstr.t -> bool
 val canonical_projections : unit ->
   ((GlobRef.t * cs_pattern) * obj_typ) list
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index cf5d4de40c..52f60fbc5e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -934,14 +934,6 @@ let stack_red_of_state_red f =
   let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in
   f
 
-(* Drops the Cst_stack *)
-let iterate_whd_gen flags env sigma s =
-  let rec aux t =
-  let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in
-  let whd_sk = Stack.map aux sk in
-  Stack.zip sigma (hd,whd_sk)
-  in aux s
-
 let red_of_state_red f env sigma x =
   Stack.zip sigma (f env sigma (x,Stack.empty))
 
@@ -1196,11 +1188,15 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
 
 let default_plain_instance_ident = Id.of_string "H"
 
+type subst_fun = { sfun : metavariable -> EConstr.t }
+
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
-let plain_instance sigma s c =
+let plain_instance sigma s c = match s with
+| None -> c
+| Some s ->
   let rec irec n u = match EConstr.kind sigma u with
-    | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
+    | Meta p -> (try lift n (s.sfun p) with Not_found -> u)
     | App (f,l) when isCast sigma f ->
         let (f,_,t) = destCast sigma f in
         let l' = Array.Fun1.Smart.map irec n l in
@@ -1209,7 +1205,7 @@ let plain_instance sigma s c =
             (* Don't flatten application nodes: this is used to extract a
                proof-term from a proof-tree and we want to keep the structure
                of the proof-tree *)
-            (try let g = Metamap.find p s in
+            (try let g = s.sfun p in
             match EConstr.kind sigma g with
             | App _ ->
                 let l' = Array.Fun1.Smart.map lift 1 l' in
@@ -1220,12 +1216,11 @@ let plain_instance sigma s c =
             with Not_found -> mkApp (f,l'))
         | _ -> mkApp (irec n f,l'))
     | Cast (m,_,_) when isMeta sigma m ->
-        (try lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u)
+        (try lift n (s.sfun (destMeta sigma m)) with Not_found -> u)
     | _ ->
         map_with_binders sigma succ irec n u
   in
-  if Metamap.is_empty s then c
-  else irec 0 c
+  irec 0 c
 
 (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
    has (unfortunately) different subtle side effects:
@@ -1427,23 +1422,41 @@ let is_arity env sigma c =
 (*************************************)
 (* Metas *)
 
-let meta_value env evd mv =
-  let rec valrec mv =
-    match meta_opt_fvalue evd mv with
-    | Some (b,_) ->
-      let metas = Metamap.bind valrec b.freemetas in
-      instance env evd metas b.rebus
-    | None -> mkMeta mv
+type meta_instance_subst = {
+  sigma : Evd.evar_map;
+  mutable cache : EConstr.t Metamap.t;
+}
+
+let create_meta_instance_subst sigma = {
+  sigma;
+  cache = Metamap.empty;
+}
+
+let eval_subst env subst =
+  let rec ans mv =
+    try Metamap.find mv subst.cache
+    with Not_found ->
+      match meta_opt_fvalue subst.sigma mv with
+      | None -> mkMeta mv
+      | Some (b, _) ->
+        let metas =
+          if Metaset.is_empty b.freemetas then None
+          else Some { sfun = ans }
+        in
+        let res = instance env subst.sigma metas b.rebus in
+        let () = subst.cache <- Metamap.add mv res subst.cache in
+        res
   in
-  valrec mv
+  { sfun = ans }
 
-let meta_instance env sigma b =
+let meta_instance env subst b =
   let fm = b.freemetas in
   if Metaset.is_empty fm then b.rebus
   else
-    let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in
-    instance env sigma c_sigma b.rebus
+    let sfun = eval_subst env subst in
+    instance env subst.sigma (Some sfun) b.rebus
 
 let nf_meta env sigma c =
+  let sigma = create_meta_instance_subst sigma in
   let cl = mk_freelisted c in
   meta_instance env sigma { cl with rebus = cl.rebus }
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 29b698f9d6..ae93eb48b4 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -133,8 +133,6 @@ end
 
 (************************************************************************)
 
-type state = constr * constr Stack.t
-
 type reduction_function = env -> evar_map -> constr -> constr
 
 type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
@@ -142,11 +140,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 type stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
 
-type state_reduction_function =
-    env -> evar_map -> state -> state
-
-val pr_state : env -> evar_map -> state -> Pp.t
-
 (** {6 Reduction Function Operators } *)
 
 val strong_with_flags :
@@ -154,12 +147,6 @@ val strong_with_flags :
   (CClosure.RedFlags.reds -> reduction_function)
 val strong : reduction_function -> reduction_function
 
-val whd_state_gen :
-  CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state
-
-val iterate_whd_gen : CClosure.RedFlags.reds ->
-  Environ.env -> Evd.evar_map -> constr -> constr
-
 (** {6 Generic Optimized Reduction Function using Closures } *)
 
 val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
@@ -193,24 +180,13 @@ val whd_all_stack : stack_reduction_function
 val whd_allnolet_stack : stack_reduction_function
 val whd_betalet_stack : stack_reduction_function
 
-val whd_nored_state : state_reduction_function
-val whd_beta_state : state_reduction_function
-val whd_betaiota_state : state_reduction_function
-val whd_betaiotazeta_state : state_reduction_function
-val whd_all_state : state_reduction_function
-val whd_allnolet_state : state_reduction_function
-val whd_betalet_state : state_reduction_function
-
 (** {6 Head normal forms } *)
 
 val whd_delta_stack :  stack_reduction_function
-val whd_delta_state :  state_reduction_function
 val whd_delta :  reduction_function
 val whd_betadeltazeta_stack :  stack_reduction_function
-val whd_betadeltazeta_state :  state_reduction_function
 val whd_betadeltazeta :  reduction_function
 val whd_zeta_stack : stack_reduction_function
-val whd_zeta_state : state_reduction_function
 val whd_zeta : reduction_function
 
 val shrink_eta : Environ.env -> constr -> constr
@@ -296,11 +272,24 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t ->
 
 (** {6 Heuristic for Conversion with Evar } *)
 
+type state = constr * constr Stack.t
+
+type state_reduction_function =
+    env -> evar_map -> state -> state
+
+val pr_state : env -> evar_map -> state -> Pp.t
+
+val whd_nored_state : state_reduction_function
+
 val whd_betaiota_deltazeta_for_iota_state :
-  TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
+  TransparentState.t -> state_reduction_function
 
 (** {6 Meta-related reduction functions } *)
-val meta_instance : env -> evar_map -> constr freelisted -> constr
+type meta_instance_subst
+
+val create_meta_instance_subst : Evd.evar_map -> meta_instance_subst
+
+val meta_instance : env -> meta_instance_subst -> constr freelisted -> constr
 val nf_meta       : env -> evar_map -> constr -> constr
 
 exception AnomalyInConversion of exn
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9cf7119709..c705ac16e7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1046,28 +1046,23 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
   | _ -> map_constr_with_binders_left_to_right sigma g f acc c
 
 let e_contextually byhead (occs,c) f = begin fun env sigma t ->
-  let (nowhere_except_in,locs) = Locusops.convert_occs occs in
-  let maxocc = List.fold_right max locs 0 in
-  let pos = ref 1 in
+  let count = ref (Locusops.initialize_occurrence_counter occs) in
   (* FIXME: we do suspicious things with this evarmap *)
   let evd = ref sigma in
   let rec traverse nested (env,c as envc) t =
-    if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t
+    if Locusops.occurrences_done !count then (* Shortcut *) t
     else
     try
       let subst =
         if byhead then matches_head env sigma c t
         else Constr_matching.matches env sigma c t in
-      let ok =
-        if nowhere_except_in then Int.List.mem !pos locs
-        else not (Int.List.mem !pos locs) in
-      incr pos;
+      let ok, count' = Locusops.update_occurrence_counter !count in count := count';
       if ok then begin
         if Option.has_some nested then
-          user_err  (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
+          user_err  (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (Locusops.current_occurrence !count) ++ str ".");
         (* Skip inner occurrences for stable counting of occurrences *)
-        if locs != [] then
-          ignore (traverse_below (Some (!pos-1)) envc t);
+        if Locusops.more_specific_occurrences !count then
+          ignore (traverse_below (Some (Locusops.current_occurrence !count)) envc t);
         let (evm, t) = (f subst) env !evd t in
         (evd := evm; t)
       end
@@ -1087,7 +1082,7 @@ let e_contextually byhead (occs,c) f = begin fun env sigma t ->
           (traverse nested) envc sigma t
   in
   let t' = traverse None (env,c) t in
-  if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
+  Locusops.check_used_occurrences !count;
   (!evd, t')
   end
 
@@ -1105,28 +1100,25 @@ let match_constr_evaluable_ref sigma c evref =
   | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
   | _, _ -> None
 
-let substlin env sigma evalref n (nowhere_except_in,locs) c =
-  let maxocc = List.fold_right max locs 0 in
-  let pos = ref n in
-  assert (List.for_all (fun x -> x >= 0) locs);
+let substlin env sigma evalref occs c =
+  let count = ref (Locusops.initialize_occurrence_counter occs) in
   let value u = value_of_evaluable_ref env evalref u in
   let rec substrec () c =
-    if nowhere_except_in && !pos > maxocc then c
+    if Locusops.occurrences_done !count then c
     else
       match match_constr_evaluable_ref sigma c evalref with
       | Some u ->
-        let ok =
-          if nowhere_except_in then Int.List.mem !pos locs
-          else not (Int.List.mem !pos locs) in
-          incr pos;
-          if ok then value u else c
+        let ok, count' = Locusops.update_occurrence_counter !count in
+        count := count';
+        if ok then value u else c
       | None ->
         map_constr_with_binders_left_to_right sigma
           (fun _ () -> ())
           substrec () c
   in
   let t' = substrec () c in
-  (!pos, t')
+  Locusops.check_used_occurrences !count;
+  (Locusops.current_occurrence !count, t')
 
 let string_of_evaluable_ref env = function
   | EvalVarRef id -> Id.to_string id
@@ -1154,23 +1146,14 @@ let unfold env sigma name c =
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env sigma (occs,name) c =
-  let unfo nowhere_except_in locs =
-    let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in
-    if Int.equal nbocc 1 then
+  match occs with
+  | NoOccurrences -> c
+  | AllOccurrences -> unfold env sigma name c
+  | OnlyOccurrences _ | AllOccurrencesBut _ | AtLeastOneOccurrence ->
+    let (occ,uc) = substlin env sigma name occs c in
+    if Int.equal occ 0 then
       user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur."));
-    let rest = List.filter (fun o -> o >= nbocc) locs in
-    let () = match rest with
-    | [] -> ()
-    | _ -> error_invalid_occurrence rest
-    in
     nf_betaiotazeta env sigma uc
-  in
-  match occs with
-    | NoOccurrences -> c
-    | AllOccurrences -> unfold env sigma name c
-    | OnlyOccurrences l -> unfo true l
-    | AllOccurrencesBut l -> unfo false l
-    | AtLeastOneOccurrence -> unfo false []
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c =
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index aeb3873de7..e3e5244a8c 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -33,7 +33,7 @@ let meta_type env evd mv =
   let ty =
     try Evd.meta_ftype evd mv
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
-  meta_instance env evd ty
+  meta_instance env (create_meta_instance_subst evd) ty
 
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let u = Unsafe.to_instance u in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c352a6ac1f..3d3010d1a4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1070,10 +1070,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp_or_Proj sigma cM then
-        let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in
-          if is_open_canonical_projection curenv sigma f1l1 then
-            let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in
-              solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
+          if is_open_canonical_projection curenv sigma cM then
+            solve_canonical_projection curenvnb pb opt cM cN substn
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
@@ -1086,14 +1084,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       else
         try f1 () with e when precatchable_exception e ->
           if isApp_or_Proj sigma cN then
-            let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in
-              if is_open_canonical_projection curenv sigma f2l2 then
-                let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in
-                  solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
+              if is_open_canonical_projection curenv sigma cN then
+                solve_canonical_projection curenvnb pb opt cN cM substn
               else error_cannot_unify (fst curenvnb) sigma (cM,cN)
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 
-  and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
+  and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) =
+    let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in
+    let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in
     let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
       try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1944,7 +1942,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
               try (* First try finding a subterm w/o conversion on open terms *)
                 let flags = set_no_delta_open_flags flags in
                 w_unify_to_subterm env evd ~flags t'
-              with e ->
+              with e when CErrors.noncritical e ->
                 (* If this fails, try with full conversion *)
                 w_unify_to_subterm env evd ~flags t'
             else w_unify_to_subterm env evd ~flags t'