Merge branch 'v8.6'

34 files changed, 420 insertions, 78 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index c9ee326cb..6c38f38e2 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -530,7 +530,7 @@ let check_positivity env_ar mind params nrecp inds =
 let check_inductive env kn mib =
   Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
   (* check mind_constraints: should be consistent with env *)
-  let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
+  let env = Environ.push_context (Univ.instantiate_univ_context mib.mind_universes) env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index a0cb008a3..2095245eb 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
 
 git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
 
-( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers && make -j ${NJOBS} fiat-core )
+( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers parsers-examples && make -j ${NJOBS} fiat-core )
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 19ca8d50b..d254520e0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -288,17 +288,8 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
 
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
-  (* pboutill: There are letins in pat which is incompatible with notations and
-     not explicit application. *)
-  match pat with
-    | { loc; v = PatCstr(cstrsp,args,na) }
-	when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
-      let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in
-      let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-      CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
-    | _ ->
   try
-    if !Flags.raw_print || !print_no_symbol then raise No_match;
+    if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
     match availability_of_prim_token p sc scopes with
       | None -> raise No_match
@@ -307,7 +298,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na
   with No_match ->
     try
-      if !Flags.raw_print || !print_no_symbol then raise No_match;
+      if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
       extern_notation_pattern scopes vars pat
 	(uninterp_cases_pattern_notations pat)
     with No_match ->
@@ -321,21 +312,19 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
               if !Flags.raw_print then raise Exit;
 	      let projs = Recordops.lookup_projections (fst cstrsp) in
 	      let rec ip projs args acc =
-		match projs with
-		  | [] -> acc
-		  | None :: q -> ip q args acc
-		  | Some c :: q ->
-		    match args with
-		      | [] -> raise No_match
-
-
-
-
-
-	| { CAst.v = CPatAtom None } :: tail -> ip q tail acc
-		    (* we don't want to have 'x = _' in our patterns *)
-		      | head :: tail -> ip q tail
-		        ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc)
+		match projs, args with
+		  | [], [] -> acc
+		  | proj :: q, pat :: tail ->
+                     let acc =
+                       match proj, pat with
+		       | _, { CAst.v = CPatAtom None } ->
+		          (* we don't want to have 'x := _' in our patterns *)
+                          acc
+		       | Some c, _ ->
+		          ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc)
+                       | _ -> raise No_match in
+                     ip q tail acc
+	          | _ -> assert false
 	      in
 	      CPatRecord(List.rev (ip projs args []))
 	    with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6f17324a1..3d484a02d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -963,6 +963,45 @@ let check_constructor_length env loc cstr len_pl pl0 =
       (error_wrong_numarg_constructor ?loc env cstr
          (Inductiveops.constructor_nrealargs cstr)))
 
+open Term
+open Declarations
+
+(* Similar to Cases.adjust_local_defs but on RCPat *)
+let insert_local_defs_in_pattern (ind,j) l =
+  let (mib,mip) = Global.lookup_inductive ind in
+  if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
+    (* Optimisation *) l
+  else
+    let typi = mip.mind_nf_lc.(j-1) in
+    let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in
+    let (decls,_) = decompose_prod_assum typi in
+    let rec aux decls args =
+      match decls, args with
+      | Context.Rel.Declaration.LocalDef _ :: decls, args -> (CAst.make @@ RCPatAtom None) :: aux decls args
+      | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *)
+      | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
+      | _ -> assert false in
+    aux (List.rev decls) l
+
+let add_local_defs_and_check_length loc env g pl args = match g with
+  | ConstructRef cstr ->
+     (* We consider that no variables corresponding to local binders
+        have been given in the "explicit" arguments, which come from a
+        "@C args" notation or from a custom user notation *)
+     let pl' = insert_local_defs_in_pattern cstr pl in
+     let maxargs = Inductiveops.constructor_nalldecls cstr in
+     if List.length pl' + List.length args > maxargs then
+       error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr);
+     (* Two possibilities: either the args are given with explict
+     variables for local definitions, then we give the explicit args
+     extended with local defs, so that there is nothing more to be
+     added later on; or the args are not enough to have all arguments,
+     which a priori means local defs to add in the [args] part, so we
+     postpone the insertion of local defs in the explicit args *)
+     (* Note: further checks done later by check_constructor_length *)
+     if List.length pl' + List.length args = maxargs then pl' else pl
+  | _ -> pl
+
 let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
   let impl_list = if Int.equal len_pl1 0
     then select_impargs_size (List.length pl2) impls_st
@@ -1200,7 +1239,7 @@ let rec subst_pat_iterator y t = CAst.(map (function
   | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
   | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
 
-let drop_notations_pattern looked_for =
+let drop_notations_pattern looked_for genv =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
      only constructor are allowed *)
   let ensure_kind top loc g =
@@ -1355,9 +1394,9 @@ let drop_notations_pattern looked_for =
     | NApp (NRef g,pl) ->
       ensure_kind top loc g;
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
-      CAst.make ?loc @@ RCPatCstr (g,
-		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
-		 List.map (in_pat false scopes) args, [])
+      let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in
+      let pl = add_local_defs_and_check_length loc genv g pl args in
+      CAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, [])
     | NList (x,y,iter,terminator,lassoc) ->
       if not (List.is_empty args) then user_err ?loc 
         (strbrk "Application of arguments to a recursive notation not supported in patterns.");
@@ -1418,7 +1457,7 @@ let rec intern_pat genv aliases pat =
 
 let intern_cases_pattern genv scopes aliases pat =
   intern_pat genv aliases
-    (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
+    (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat)
 
 let _ =
   intern_cases_pattern_fwd :=
@@ -1427,7 +1466,7 @@ let _ =
 let intern_ind_pattern genv scopes pat =
   let no_not =
     try
-      drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
+      drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
     with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
   in
   let loc = no_not.CAst.loc in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 08b9fbe8e..33b93606e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1154,10 +1154,6 @@ let match_notation_constr u c (metas,pat) =
     metas ([],[],[])
 
 (* Matching cases pattern *)
-let add_patterns_for_params ind l =
-  let mib,_ = Global.lookup_inductive ind in
-  let nparams = mib.Declarations.mind_nparams in
-    Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l
 
 let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
   try
@@ -1187,10 +1183,11 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
   | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
-      sigma,(0,add_patterns_for_params (fst r1) largs)
+      let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
+      sigma,(0,l)
   | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
-      let l1 = add_patterns_for_params (fst r1) args1 in
+      let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
       if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
       then
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 5f5f548f8..6c0e2d776 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -174,12 +174,18 @@ Ltac zify_nat_op :=
      match isnat with
       | true => simpl (Z.of_nat (S a)) in H
       | _ => rewrite (Nat2Z.inj_succ a) in H
+      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+                hide [Z.of_nat (S a)] in this one hypothesis *)
+        change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H
      end
   | |- context [ Z.of_nat (S ?a) ] =>
      let isnat := isnatcst a in
      match isnat with
       | true => simpl (Z.of_nat (S a))
       | _ => rewrite (Nat2Z.inj_succ a)
+      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+                hide [Z.of_nat (S a)] in the goal *)
+        change (Z.of_nat (S a)) with (Z_of_nat' (S a))
      end
 
   (* atoms of type nat : we add a positivity condition (if not already there) *)
@@ -401,4 +407,3 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
 (** The complete Z-ification tactic *)
 
 Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op.
-
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 94e3f508f..9cb94b68d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -708,6 +708,39 @@ let clever_rewrite p vpath t =
   refine_app gl t'
   end
 
+(** simpl_coeffs :
+    The subterm at location [path_init] in the current goal should
+    look like [(v1*c1 + (v2*c2 + ... (vn*cn + k)))], and we reduce
+    via "simpl" each [ci] and the final constant [k].
+    The path [path_k] gives the location of constant [k].
+    Earlier, the whole was a mere call to [focused_simpl],
+    leading to reduction inside the atoms [vi], which is bad,
+    for instance when the atom is an evaluable definition
+    (see #4132). *)
+
+let simpl_coeffs path_init path_k =
+  Proofview.Goal.enter begin fun gl ->
+  let sigma = project gl in
+  let rec loop n t =
+    if Int.equal n 0 then pf_nf gl t
+    else
+      (* t should be of the form ((v * c) + ...) *)
+      match EConstr.kind sigma t with
+      | App(f,[|t1;t2|]) ->
+         (match EConstr.kind sigma t1 with
+          | App (g,[|v;c|]) ->
+             let c' = pf_nf gl c in
+             let t2' = loop (pred n) t2 in
+             mkApp (f,[|mkApp (g,[|v;c'|]);t2'|])
+          | _ -> assert false)
+      | _ -> assert false
+  in
+  let n = Pervasives.(-) (List.length path_k) (List.length path_init) in
+  let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl)
+  in
+  convert_concl_no_check newc DEFAULTcast
+  end
+
 let rec shuffle p (t1,t2) =
   match t1,t2 with
     | Oplus(l1,r1), Oplus(l2,r2) ->
@@ -770,7 +803,7 @@ let shuffle_mult p_init k1 e1 k2 e2 =
             let tac' =
 	      clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
                 (Lazy.force coq_fast_Zred_factor5) in
-	    tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' ::
+	    tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' ::
 	    loop p (l1,l2)
           else tac :: loop (P_APP 2 :: p) (l1,l2)
 	else if v1 > v2 then
@@ -805,7 +838,7 @@ let shuffle_mult p_init k1 e1 k2 e2 =
                            [P_APP 2; P_APP 2]]
           (Lazy.force coq_fast_OMEGA12) ::
         loop (P_APP 2 :: p) ([],l2)
-    | [],[] -> [focused_simpl p_init]
+    | [],[] -> [simpl_coeffs p_init p]
   in
   loop p_init (e1,e2)
 
@@ -828,7 +861,7 @@ let shuffle_mult_right p_init e1 k2 e2 =
               clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
                 (Lazy.force coq_fast_Zred_factor5)
 	    in
-            tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' ::
+            tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' ::
             loop p (l1,l2)
           else tac :: loop (P_APP 2 :: p) (l1,l2)
 	else if v1 > v2 then
@@ -855,7 +888,7 @@ let shuffle_mult_right p_init e1 k2 e2 =
                           [P_APP 2; P_APP 2]]
           (Lazy.force coq_fast_OMEGA12) ::
         loop (P_APP 2 :: p) ([],l2)
-    | [],[] -> [focused_simpl p_init]
+    | [],[] -> [simpl_coeffs p_init p]
   in
   loop p_init (e1,e2)
 
@@ -896,7 +929,7 @@ let rec scalar p n = function
 
 let scalar_norm p_init =
   let rec loop p = function
-    | [] -> [focused_simpl p_init]
+    | [] -> [simpl_coeffs p_init p]
     | (_::l) ->
 	clever_rewrite p
           [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2];
@@ -907,7 +940,7 @@ let scalar_norm p_init =
 
 let norm_add p_init =
   let rec loop p = function
-    | [] -> [focused_simpl p_init]
+    | [] -> [simpl_coeffs p_init p]
     | _:: l ->
 	clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
           (Lazy.force coq_fast_Zplus_assoc_reverse) ::
@@ -917,7 +950,7 @@ let norm_add p_init =
 
 let scalar_norm_add p_init =
   let rec loop p = function
-    | [] -> [focused_simpl p_init]
+    | [] -> [simpl_coeffs p_init p]
     | _ :: l ->
 	clever_rewrite p
           [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e53d19b59..62ff9ac70 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -457,11 +457,44 @@ let rec cases_pattern_of_glob_constr na = CAst.map (function
   | _ -> raise Not_found
   )
 
+open Declarations
+open Term
+open Context
+
+(* Keep only patterns which are not bound to a local definitions *)
+let drop_local_defs typi args =
+    let (decls,_) = decompose_prod_assum typi in
+    let rec aux decls args =
+      match decls, args with
+      | [], [] -> []
+      | Rel.Declaration.LocalDef _ :: decls, pat :: args ->
+         begin
+           match pat.CAst.v with
+           | PatVar Anonymous -> aux decls args
+           | _ -> raise Not_found (* The pattern is used, one cannot drop it *)
+         end
+      | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
+      | _ -> assert false in
+    aux (List.rev decls) args
+
+let add_patterns_for_params_remove_local_defs (ind,j) l =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let nparams = mib.Declarations.mind_nparams in
+  let l =
+    if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
+      (* Optimisation *) l
+    else
+      let typi = mip.mind_nf_lc.(j-1) in
+      let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in
+      drop_local_defs typi l in
+  Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l
+
 (* Turn a closed cases pattern into a glob_constr *)
 let rec glob_constr_of_closed_cases_pattern_aux x = CAst.map_with_loc (fun ?loc -> function
   | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
   | PatCstr (cstr,l,Anonymous)  ->
       let ref = CAst.make ?loc @@ GRef (ConstructRef cstr,None) in
+      let l = add_patterns_for_params_remove_local_defs cstr l in
       GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
   | _ -> raise Not_found
   ) x
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index f7cc08ca2..75db04f77 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -81,3 +81,5 @@ val map_pattern : (glob_constr -> glob_constr) ->
 val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
 
 val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr
+
+val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index db2e5da95..c36542aeb 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -364,9 +364,9 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
-      let mkGLambda c na = CAst.make ?loc @@
+      let mkGLambda na c = CAst.make ?loc @@
 	GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
-      let c = List.fold_left mkGLambda c nal in
+      let c = List.fold_right mkGLambda nal c in
       let cip =
 	{ cip_style = LetStyle;
 	  cip_ind = None;
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b4654bfb5..52d1ffe06 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -777,7 +777,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
     context" in contract_fix *)
 let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
   let raw_answer =
-    let env = if refold then None else Some env in
+    let env = if refold then Some env else None in
     contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
   apply_subst
     (fun sigma x (t,sk') ->
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 79d2e4694..34875cbcd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -662,7 +662,8 @@ let evar_of_binder holes = function
 | NamedHyp s -> evar_with_name holes s
 | AnonHyp n ->
   try
-    let h = List.nth holes (pred n) in
+    let nondeps = List.filter (fun hole -> not hole.hole_deps) holes in
+    let h = List.nth nondeps (pred n) in
     h.hole_evar
   with e when CErrors.noncritical e ->
     user_err  (str "No such binder.")
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index de49a521f..4bde427b1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -603,6 +603,7 @@ let make_hints g st only_classes sign =
     List.fold_left
       (fun hints hyp ->
         let consider =
+          not only_classes ||
           try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in
               (* Section variable, reindex only if the type changed *)
               not (EConstr.eq_constr (project g) (EConstr.of_constr t) (NamedDecl.get_type hyp))
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index aa574e41c..4101dc23e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -468,6 +468,7 @@ module New = struct
 
   let check_evars env sigma extsigma origsigma =
     let rec is_undefined_up_to_restriction sigma evk =
+      if Evd.mem origsigma evk then None else
       let evi = Evd.find sigma evk in
       match Evd.evar_body evi with
       | Evd.Evar_empty -> Some (evk,evi)
@@ -481,7 +482,7 @@ module New = struct
     let rest =
       Evd.fold_undefined (fun evk evi acc ->
         match is_undefined_up_to_restriction sigma evk with
-        | Some (evk',evi) when not (Evd.mem origsigma evk) -> (evk',evi)::acc
+        | Some (evk',evi) -> (evk',evi)::acc
         | _ -> acc)
         extsigma []
     in
diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v
new file mode 100644
index 000000000..806ffb771
--- /dev/null
+++ b/test-suite/bugs/closed/4132.v
@@ -0,0 +1,31 @@
+
+Require Import ZArith Omega.
+Open Scope Z_scope.
+
+(** bug 4132: omega was using "simpl" either on whole equations, or on
+   delimited but wrong spots. This was leading to unexpected reductions
+   when one atom (here [b]) is an evaluable reference instead of a variable. *)
+
+Lemma foo
+  (x y x' zxy zxy' z : Z)
+  (b := 5)
+  (Ry : - b <= y < b)
+  (Bx : x' <= b)
+  (H : - zxy' <= zxy)
+  (H' : zxy' <= x') : - b <= zxy.
+Proof.
+omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
+Qed.
+
+Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
+omega. (* Pierre L: according to a comment of bug report #4132,
+          this might have triggered "index out of bounds" in the past,
+          but I never managed to reproduce that in any version,
+          even before my fix. *)
+Qed.
+
+Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
+omega. (* Pierre L: according to a comment of bug report #4132,
+          this might have triggered "Failure(occurence 2)" in the past,
+          but I never managed to reproduce that. *)
+Qed.
diff --git a/test-suite/bugs/closed/5019.v b/test-suite/bugs/closed/5019.v
new file mode 100644
index 000000000..7c973f88b
--- /dev/null
+++ b/test-suite/bugs/closed/5019.v
@@ -0,0 +1,5 @@
+Require Import Coq.ZArith.ZArith.
+Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d.
+  clear; intros.
+  Timeout 1 zify. (* used to loop forever; should take < 0.01 s *)
+Admitted.
diff --git a/test-suite/bugs/closed/5255.v b/test-suite/bugs/closed/5255.v
new file mode 100644
index 000000000..5daaf9edb
--- /dev/null
+++ b/test-suite/bugs/closed/5255.v
@@ -0,0 +1,24 @@
+Section foo.
+  Context (x := 1).
+  Definition foo : x = 1 := eq_refl.
+End foo.
+
+Module Type Foo.
+  Context (x := 1).
+  Definition foo : x = 1 := eq_refl.
+End Foo.
+
+Set Universe Polymorphism.
+
+Inductive unit := tt.
+Inductive eq {A} (x y : A) : Type := eq_refl : eq x y.
+
+Section bar.
+  Context (x := tt).
+  Definition bar : eq x tt := eq_refl _ _.
+End bar.
+
+Module Type Bar.
+  Context (x := tt).
+  Definition bar : eq x tt := eq_refl _ _.
+End Bar.
diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v
new file mode 100644
index 000000000..390133162
--- /dev/null
+++ b/test-suite/bugs/closed/5486.v
@@ -0,0 +1,15 @@
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k :
+									 forall _ : T, Fm),
+    @eq Fm
+	(k
+	   match p return T with
+	   | pair p0 swap => fst p0
+	   end) f.
+  intros.
+  (* next statement failed in Bug 5486 *)
+  match goal with
+  | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ]
+    => pose (let (a, b) := d in e a b) as t0
+  end.
diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v
new file mode 100644
index 000000000..88f219be3
--- /dev/null
+++ b/test-suite/bugs/closed/5526.v
@@ -0,0 +1,3 @@
+Fail Notation "x === x" := (eq_refl x) (at level 10).
+Reserved Notation "x === x" (only printing, at level 10).
+Notation "x === x" := (eq_refl x) (only printing).
diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v
new file mode 100644
index 000000000..bb1222489
--- /dev/null
+++ b/test-suite/bugs/closed/5550.v
@@ -0,0 +1,10 @@
+Section foo.
+
+  Variable bar : Prop.
+  Variable H : bar.
+
+  Goal bar.
+    typeclasses eauto with foobar.
+  Qed.
+
+End foo.
diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v
index 84a4009d7..19eea94b1 100644
--- a/test-suite/coqchk/univ.v
+++ b/test-suite/coqchk/univ.v
@@ -33,3 +33,16 @@ Inductive finite_of_order T (D : T -> Type) (n : natural) :=
     (rank_injective : injective_in T natural D rank)
     (rank_onto :
        forall i, equivalent (less_than i n) (in_image T natural D rank i)).
+
+(* Constraints *)
+Universes i j.
+Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})).
+Constraint i < j.
+Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}).
+Universes i' j'.
+Constraint i' = j'.
+Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})).
+Inductive constraint4 : (Type -> Type) -> Type
+  := mk_constraint4 : let U1 := Type in
+                      let U2 := Type in
+                      constraint4 (fun x : U1 => (x : U2)).
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 8ce6f9795..f064dfe76 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -2,18 +2,18 @@ t_rect =
 fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
-  | @k _ x0 => f x0 (F x0)
+  | k _ x0 => f x0 (F x0)
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
 Argument scopes are [function_scope function_scope _]
      = fun d : TT => match d with
-                     | @CTT _ _ b => b
+                     | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
      = fun d : TT => match d with
-                     | @CTT _ _ b => b
+                     | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
 proj = 
@@ -72,3 +72,11 @@ e1 : texp t1
 e2 : texp t2
 The term "0" has type "nat" while it is expected to have type
  "typeDenote t0".
+fun '{{n, m, _}} => n + m
+     : J -> nat
+fun '{{n, m, p}} => n + m + p
+     : J -> nat
+fun '(D n m p q) => n + m + p + q
+     : J -> nat
+The command has indeed failed with message:
+The constructor D (in type J) expects 3 arguments.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 407489642..6a4fd007d 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -106,3 +106,18 @@ Fail Fixpoint texpDenote t (e:texp t):typeDenote t:=
   | TBinop t1 t2 _ b e1 e2 => O
   end.
 
+(* Test notations with local definitions in constructors *)
+
+Inductive J := D : forall n m, let p := n+m in nat -> J.
+Notation "{{ n , m , q }}" := (D n m q).
+
+Check fun x : J => let '{{n, m, _}} := x in n + m.
+Check fun x : J => let '{{n, m, p}} := x in n + m + p.
+
+(* Cannot use the notation because of the dependency in p *)
+
+Check fun x => let '(D n m p q) := x in n+m+p+q.
+
+(* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
+
+Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index f4ecfd736..ffea0819a 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -105,3 +105,7 @@ tele (t : Type) '(y, z) (x : t0) := tt
          ((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat))))))
 foo5 x nat x
      : nat -> nat
+fun x : ?A => x === x
+     : forall x : ?A, x = x
+where
+?A : [x : ?A |- Type] (x cannot be used)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 71536c68f..250aecafd 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -148,5 +148,15 @@ Check [ fun x => x+0 ;; fun x => x+1 ;; fun x => x+2 ].
 
 (* Cyprien's part of bug #4765 *)
 
+Section Bug4765.
+
 Notation foo5 x T y := (fun x : T => y).
 Check foo5 x nat x.
+
+End Bug4765.
+
+(**********************************************************************)
+(* Test printing of #5526                                             *)
+
+Notation "x === x" := (eq_refl x) (only printing, at level 10).
+Check (fun x => eq_refl x).
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index 36d643a44..d45343fe6 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -14,3 +14,19 @@ build 5
      : test_r
 build_c 5
      : test_c
+fun '(C _ p) => p
+     : N -> True
+fun '{| T := T |} => T
+     : N -> Type
+fun '(C T p) => (T, p)
+     : N -> Type * True
+fun '{| q := p |} => p
+     : M -> True
+fun '{| U := T |} => T
+     : M -> Type
+fun '{| U := T; q := p |} => (T, p)
+     : M -> Type * True
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+     : M -> Type * True * nat
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+     : M -> Type * True * nat
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 6aa3df983..d9a649fad 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -19,3 +19,15 @@ Check build 5.
 Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
+
+Record N := C { T : Type; _ : True }.
+Check fun x:N => let 'C _ p := x in p.
+Check fun x:N => let 'C T _ := x in T.
+Check fun x:N => let 'C T p := x in (T,p).
+
+Record M := D { U : Type; a := 0; q : True }.
+Check fun x:M => let 'D T _ p := x in p.
+Check fun x:M => let 'D T _ p := x in T.
+Check fun x:M => let 'D T p := x in (T,p).
+Check fun x:M => let 'D T a p := x in (T,p,a).
+Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a).
diff --git a/test-suite/output/ShowMatch.out b/test-suite/output/ShowMatch.out
new file mode 100644
index 000000000..e5520b8df
--- /dev/null
+++ b/test-suite/output/ShowMatch.out
@@ -0,0 +1,8 @@
+match # with
+ | f =>
+ end
+ 
+match # with
+ | A.f =>
+ end
+ 
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v
new file mode 100644
index 000000000..02b7eada8
--- /dev/null
+++ b/test-suite/output/ShowMatch.v
@@ -0,0 +1,13 @@
+(* Bug 5546 complained about unqualified constructors in Show Match output, 
+   when qualification is needed to disambiguate them
+*)
+
+Module A.
+  Inductive foo := f.
+  Show Match foo. (* no need to disambiguate *)
+End A. 
+
+Module B.
+  Inductive foo := f.
+  (* local foo shadows A.foo, so constructor "f" needs disambiguation *)
+  Show Match A.foo. 
diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v
new file mode 100644
index 000000000..6aeb05f54
--- /dev/null
+++ b/test-suite/success/cbn.v
@@ -0,0 +1,18 @@
+(* cbn is able to refold mutual recursive calls *)
+
+Fixpoint foo (n : nat) :=
+  match n with
+  | 0 => true
+  | S n => g n
+  end
+with g (n : nat) : bool :=
+  match n with
+  | 0 => true
+  | S n => foo n
+  end.
+Goal forall n, foo (S n) = g n.
+  intros. cbn.
+  match goal with
+    |- g _ = g _ => reflexivity
+  end.
+Qed.
\ No newline at end of file
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 82f726fa7..c36313ec1 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -414,4 +414,10 @@ Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2.
 Import EqNotations.
 Definition test2 {A B:Type} {H:A=B} (a:A) : B := rew H in a.
 
+(* Check that pre-existing evars are not counted as newly undefined in "set" *)
+(* Reported by Théo *)
 
+Goal exists n : nat, n = n -> True.
+eexists.
+set (H := _ = _).
+Abort.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index dc5ce1a53..8e6a0f6a7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -386,7 +386,13 @@ let context poly l =
       let ctx = Univ.ContextSet.to_context !uctx in
       (* Declare the universe context once *)
       let () = uctx := Univ.ContextSet.empty in
-      let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in
+      let decl = match b with
+      | None ->
+        (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical)
+      | Some b ->
+        let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+        (DefinitionEntry entry, IsAssumption Logical)
+      in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
 	match class_of_constr !evars (EConstr.of_constr t) with
 	| Some (rels, ((tc,_), args) as _cl) ->
@@ -402,9 +408,17 @@ let context poly l =
       in
       let impl = List.exists test impls in
       let decl = (Discharge, poly, Definitional) in
-      let nstatus =
+      let nstatus = match b with
+      | None ->
         pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
           Vernacexpr.NoInline (Loc.tag id))
+      | Some b ->
+        let ctx = Univ.ContextSet.to_context !uctx in
+        let decl = (Discharge, poly, Definition) in
+        let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+        let hook = Lemmas.mk_hook (fun _ gr -> gr) in
+        let _ = Command.declare_definition id decl entry [] [] hook in
+        Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
       let () = uctx := Univ.ContextSet.empty in
 	status && nstatus
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 34b9b97d8..a114553cd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -301,22 +301,22 @@ let is_numeral symbs =
   | _ ->
       false
 
-let rec get_notation_vars = function
+let rec get_notation_vars onlyprint = function
   | [] -> []
   | NonTerminal id :: sl ->
-      let vars = get_notation_vars sl in
+      let vars = get_notation_vars onlyprint sl in
       if Id.equal id ldots_var then vars else
-	if Id.List.mem id vars then
+	(* don't check for nonlinearity if printing only, see Bug 5526 *)
+	if not onlyprint && Id.List.mem id vars then 
 	  user_err ~hdr:"Metasyntax.get_notation_vars"
             (str "Variable " ++ pr_id id ++ str " occurs more than once.")
-	else
-          id::vars
-  | (Terminal _ | Break _) :: sl -> get_notation_vars sl
+	else id::vars
+  | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
   | SProdList _ :: _ -> assert false
 
-let analyze_notation_tokens l =
+let analyze_notation_tokens ~onlyprint l =
   let l = raw_analyze_notation_tokens l in
-  let vars = get_notation_vars l in
+  let vars = get_notation_vars onlyprint l in
   let recvars,l = interp_list_parser [] l in
   recvars, List.subtract Id.equal vars (List.map snd recvars), l
 
@@ -1084,12 +1084,12 @@ let compute_syntax_data df modifiers =
   if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
   let assoc = Option.append mods.assoc (Some NonA) in
   let toks = split_notation_string df in
-  let recvars,mainvars,symbols = analyze_notation_tokens toks in
+  let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint toks in
   let _ = check_useless_entry_types recvars mainvars mods.etyps in
   let _ = check_binder_type recvars mods.etyps in
 
   (* Notations for interp and grammar  *)
-let ntn_for_interp = make_notation_key symbols in
+  let ntn_for_interp = make_notation_key symbols in
   let symbols' = remove_curly_brackets symbols in
   let ntn_for_grammar = make_notation_key symbols' in
   if not onlyprint then check_rule_productivity symbols';
@@ -1333,7 +1333,7 @@ let add_notation_in_scope local df c mods scope =
 
 let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
   let dfs = split_notation_string df in
-  let recvars,mainvars,symbs = analyze_notation_tokens dfs in
+  let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
   let i_typs, onlyprint = if not (is_numeral symbs) then begin
     let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in
@@ -1410,7 +1410,7 @@ let add_notation local c ((loc,df),modifiers) sc =
 let add_notation_extra_printing_rule df k v =
   let notk = 
     let dfs = split_notation_string df in
-    let _,_, symbs = analyze_notation_tokens dfs in
+    let _,_, symbs = analyze_notation_tokens ~onlyprint:true dfs in
     make_notation_key symbs in
   Notation.add_notation_extra_printing_rule notk k v
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 69492759b..ef16df5b7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -108,14 +108,29 @@ let show_intro all =
     [Not_found] is raised if the given string isn't the qualid of
     a known inductive type. *)
 
+(*
+
+  HH notes in PR #679:
+
+  The Show Match could also be made more robust, for instance in the
+  presence of let in the branch of a constructor. A
+  decompose_prod_assum would probably suffice for that, but then, it
+  is a Context.Rel.Declaration.t which needs to be matched and not
+  just a pair (name,type).
+
+  Otherwise, this is OK. After all, the API on inductive types is not
+  so canonical in general, and in this simple case, working at the
+  low-level of mind_nf_lc seems reasonable (compared to working at the
+  higher-level of Inductiveops).
+
+*)
+    
 let make_cases_aux glob_ref =
   match glob_ref with
-    | Globnames.IndRef i ->
-	let {Declarations.mind_nparams = np}
-	    , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr }
-	      = Global.lookup_inductive i in
-	Util.Array.fold_right2
-	  (fun consname typ l ->
+    | Globnames.IndRef ind ->
+	let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in
+	Util.Array.fold_right_i
+	  (fun i typ l ->
 	     let al = List.rev (fst (decompose_prod typ)) in
 	     let al = Util.List.skipn np al in
 	     let rec rename avoid = function
@@ -124,8 +139,9 @@ let make_cases_aux glob_ref =
 		   let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
 		   Id.to_string n' :: rename (n'::avoid) l in
 	     let al' = rename [] al in
-	     (Id.to_string consname :: al') :: l)
-	  carr tarr []
+	     let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
+	     (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
+	  tarr []
     | _ -> raise Not_found
 
 let make_cases s =