Merge PR#707: add support for "-bypass-API" argument to "coq_makefile"

69 files changed, 543 insertions, 223 deletions

diff --git a/.gitignore b/.gitignore
index 84fe89d1eb..fa83045e75 100644
--- a/.gitignore
+++ b/.gitignore
@@ -72,6 +72,8 @@ test-suite/coq-makefile/*/mlihtml
 test-suite/coq-makefile/*/subdir/done
 test-suite/coq-makefile/latex1/all.pdf
 test-suite/coq-makefile/merlin1/.merlin
+test-suite/coq-makefile/plugin-reach-outside-API-and-fail/_CoqProject
+test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/_CoqProject
 
 # documentation
 
diff --git a/Makefile.common b/Makefile.common
index e7887f216a..62bbbc4fd7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -145,8 +145,6 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
 # vo files
 ###########################################################################
 
-## we now retrieve the names of .vo file to compile in */vo.itarget files
-
 GENVOFILES := $(GENVFILES:.v=.vo)
 
 THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) \
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index c9ee326cb9..6c38f38e29 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/config/coq_config.mli b/config/coq_config.mli
index 2b3bc2c25b..3f7b65c395 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -53,7 +53,10 @@ val compile_date : string (* compile date *)
 val vo_magic_number : int
 val state_magic_number : int
 
+val core_src_dirs : string list
+val api_dirs : string list
 val plugins_dirs : string list
+val all_src_dirs : string list
 
 val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
 val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *)
diff --git a/configure.ml b/configure.ml
index a5204d5b57..316cea5c93 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1088,7 +1088,19 @@ let write_configml f =
   pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/");
   pr_s "localwwwrefman"  ("file:/" ^ docdir ^ "/html/refman");
   pr_b "no_native_compiler" (not !Prefs.nativecompiler);
+
+  let core_src_dirs = [ "config"; "dev"; "kernel"; "library";
+                        "engine"; "pretyping"; "interp"; "parsing"; "proofs";
+                        "tactics"; "toplevel"; "printing"; "intf";
+                        "grammar"; "ide"; "stm"; "vernac" ] in
+  let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ "  \"" ^ core_src_subdir ^ "\";\n")
+                                    ""
+                                    core_src_dirs in
+
+  pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs;
+  pr "\nlet api_dirs = [\"API\"; \"lib\"]\n";
   pr "\nlet plugins_dirs = [\n";
+
   let plugins = Sys.readdir "plugins" in
   Array.sort compare plugins;
   Array.iter
@@ -1097,6 +1109,9 @@ let write_configml f =
       if Sys.is_directory f' && f.[0] <> '.' then pr "  %S;\n" f')
     plugins;
   pr "]\n";
+
+  pr "\nlet all_src_dirs = core_src_dirs @ api_dirs @ plugins_dirs\n";
+
   close_out o;
   Unix.chmod f 0o444
 
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index a0cb008a32..2095245eb8 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/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 195ede6d00..0edaf07efc 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -30,3 +30,13 @@ if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
 
+echo "DEBUG: ci-user-overlay.sh 0"
+if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
+    echo "DEBUG: ci-user-overlay.sh 1"
+    bedrock_src_CI_BRANCH=trunk__API
+    bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
+    bedrock_facade_CI_BRANCH=trunk__API
+    bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
+    fiat_parsers_CI_BRANCH=trunk__API
+    fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
+fi
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 19ca8d50b5..d254520e0e 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 6f17324a19..3d484a02da 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 08b9fbe8ec..33b93606ec 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/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 7a16605695..97aa90e07d 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -11,6 +11,7 @@ type project = {
   makefile : string option;
   install_kind  : install option;
   use_ocamlopt : bool;
+  bypass_API : bool;
 
   v_files : string list;
   mli_files : string list;
@@ -42,11 +43,12 @@ and install =
   | UserInstall
 
 (* TODO generate with PPX *)
-let mk_project project_file makefile install_kind use_ocamlopt = {
+let mk_project project_file makefile install_kind use_ocamlopt bypass_API = {
   project_file;
   makefile;
   install_kind;
   use_ocamlopt;
+  bypass_API;
 
   v_files = [];
   mli_files = [];
@@ -166,6 +168,8 @@ let process_cmd_line orig_dir proj args =
     aux { proj with defs = proj.defs @ [v,def] } r
   | "-arg" :: a :: r ->
     aux { proj with extra_args = proj.extra_args @ [a] } r
+  | "-bypass-API" :: r ->
+    aux { proj with bypass_API = true } r
   | f :: r ->
       let f = CUnix.correct_path f orig_dir in
       let proj =
@@ -185,11 +189,11 @@ let process_cmd_line orig_dir proj args =
  (******************************* API ************************************)
 
 let cmdline_args_to_project ~curdir args =
-  process_cmd_line curdir (mk_project None None None true) args
+  process_cmd_line curdir (mk_project None None None true false) args
 
 let read_project_file f =
   process_cmd_line (Filename.dirname f)
-    (mk_project (Some f) None (Some NoInstall) true) (parse f)
+    (mk_project (Some f) None (Some NoInstall) true false) (parse f)
 
 let rec find_project_file ~from ~projfile_name =
   let fname = Filename.concat from projfile_name in
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 8c8fc068a3..19fc9227ae 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -13,6 +13,7 @@ type project = {
   makefile : string option;
   install_kind  : install option;
   use_ocamlopt : bool;
+  bypass_API : bool;
 
   v_files : string list;
   mli_files : string list;
diff --git a/lib/envars.ml b/lib/envars.ml
index 2f76183eb3..47baf66a69 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -202,14 +202,7 @@ let xdg_dirs ~warn =
 
 (* Print the configuration information *)
 
-let coq_src_subdirs = [ 
-   "config" ; "dev" ; "lib" ; "kernel" ; "library" ;
-   "engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ;
-   "tactics" ; "toplevel" ; "printing" ; "intf" ;
-   "grammar" ; "ide" ; "stm"; "vernac" ; "API" ] @
-   Coq_config.plugins_dirs
-  
-let print_config ?(prefix_var_name="") f =
+let print_config ?(prefix_var_name="") f coq_src_subdirs =
   let open Printf in 
   fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0");
   fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
diff --git a/lib/envars.mli b/lib/envars.mli
index c8bbf17d96..edd13447fc 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -76,7 +76,4 @@ val xdg_data_dirs   : (string -> unit) -> string list
 val xdg_dirs : warn : (string -> unit) -> string list
 
 (** {6 Prints the configuration information } *)
-val print_config : ?prefix_var_name:string -> out_channel -> unit
-
-(** Directories in which coq sources are found *)
-val coq_src_subdirs : string list
+val print_config : ?prefix_var_name:string -> out_channel -> string list -> unit
diff --git a/plugins/btauto/vo.itarget b/plugins/btauto/vo.itarget
deleted file mode 100644
index 1f72d3ef22..0000000000
--- a/plugins/btauto/vo.itarget
+++ /dev/null
@@ -1,3 +0,0 @@
-Algebra.vo
-Reflect.vo
-Btauto.vo
diff --git a/plugins/derive/vo.itarget b/plugins/derive/vo.itarget
deleted file mode 100644
index b480982193..0000000000
--- a/plugins/derive/vo.itarget
+++ /dev/null
@@ -1 +0,0 @@
-Derive.vo
\ No newline at end of file
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
deleted file mode 100644
index 9c30c5eb3e..0000000000
--- a/plugins/extraction/vo.itarget
+++ /dev/null
@@ -1,16 +0,0 @@
-ExtrHaskellBasic.vo
-ExtrHaskellNatNum.vo
-ExtrHaskellNatInt.vo
-ExtrHaskellNatInteger.vo
-ExtrHaskellZNum.vo
-ExtrHaskellZInt.vo
-ExtrHaskellZInteger.vo
-ExtrHaskellString.vo
-ExtrOcamlBasic.vo
-ExtrOcamlIntConv.vo
-ExtrOcamlBigIntConv.vo
-ExtrOcamlNatInt.vo
-ExtrOcamlNatBigInt.vo
-ExtrOcamlZInt.vo
-ExtrOcamlZBigInt.vo
-ExtrOcamlString.vo
diff --git a/plugins/fourier/vo.itarget b/plugins/fourier/vo.itarget
deleted file mode 100644
index 87d82dacc5..0000000000
--- a/plugins/fourier/vo.itarget
+++ /dev/null
@@ -1,2 +0,0 @@
-Fourier_util.vo
-Fourier.vo
diff --git a/plugins/funind/vo.itarget b/plugins/funind/vo.itarget
deleted file mode 100644
index 33c9683028..0000000000
--- a/plugins/funind/vo.itarget
+++ /dev/null
@@ -1 +0,0 @@
-Recdef.vo
diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget
deleted file mode 100644
index a28fb770be..0000000000
--- a/plugins/ltac/vo.itarget
+++ /dev/null
@@ -1 +0,0 @@
-Ltac.vo
diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget
deleted file mode 100644
index a555d5ba17..0000000000
--- a/plugins/micromega/vo.itarget
+++ /dev/null
@@ -1,16 +0,0 @@
-MExtraction.vo
-EnvRing.vo
-Env.vo
-OrderedRing.vo
-Psatz.vo
-QMicromega.vo
-Refl.vo
-RingMicromega.vo
-RMicromega.vo
-Tauto.vo
-VarMap.vo
-ZCoeff.vo
-ZMicromega.vo
-Lia.vo
-Lqa.vo
-Lra.vo
diff --git a/plugins/nsatz/vo.itarget b/plugins/nsatz/vo.itarget
deleted file mode 100644
index 06fc883431..0000000000
--- a/plugins/nsatz/vo.itarget
+++ /dev/null
@@ -1 +0,0 @@
-Nsatz.vo
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 5f5f548f84..6c0e2d776d 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 94e3f508ff..9cb94b68df 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/plugins/omega/vo.itarget b/plugins/omega/vo.itarget
deleted file mode 100644
index 842210e216..0000000000
--- a/plugins/omega/vo.itarget
+++ /dev/null
@@ -1,5 +0,0 @@
-OmegaLemmas.vo
-OmegaPlugin.vo
-OmegaTactic.vo
-Omega.vo
-PreOmega.vo
diff --git a/plugins/quote/vo.itarget b/plugins/quote/vo.itarget
deleted file mode 100644
index 7a44fc5aa6..0000000000
--- a/plugins/quote/vo.itarget
+++ /dev/null
@@ -1 +0,0 @@
-Quote.vo
\ No newline at end of file
diff --git a/plugins/romega/vo.itarget b/plugins/romega/vo.itarget
deleted file mode 100644
index f7a3c41c78..0000000000
--- a/plugins/romega/vo.itarget
+++ /dev/null
@@ -1,2 +0,0 @@
-ReflOmegaCore.vo
-ROmega.vo
diff --git a/plugins/rtauto/vo.itarget b/plugins/rtauto/vo.itarget
deleted file mode 100644
index 4c9364ad72..0000000000
--- a/plugins/rtauto/vo.itarget
+++ /dev/null
@@ -1,2 +0,0 @@
-Bintree.vo
-Rtauto.vo
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
deleted file mode 100644
index 595ba55ec6..0000000000
--- a/plugins/setoid_ring/vo.itarget
+++ /dev/null
@@ -1,24 +0,0 @@
-ArithRing.vo
-BinList.vo
-Field_tac.vo
-Field_theory.vo
-Field.vo
-InitialRing.vo
-NArithRing.vo
-RealField.vo
-Ring_base.vo
-Ring_polynom.vo
-Ring_tac.vo
-Ring_theory.vo
-Ring.vo
-ZArithRing.vo
-Algebra_syntax.vo
-Cring.vo
-Ncring.vo
-Ncring_polynom.vo
-Ncring_initial.vo
-Ncring_tac.vo
-Rings_Z.vo
-Rings_R.vo
-Rings_Q.vo
-Integral_domain.vo
\ No newline at end of file
diff --git a/plugins/ssr/vo.itarget b/plugins/ssr/vo.itarget
deleted file mode 100644
index 99f9f160bb..0000000000
--- a/plugins/ssr/vo.itarget
+++ /dev/null
@@ -1,3 +0,0 @@
-ssreflect.vo
-ssrfun.vo
-ssrbool.vo
diff --git a/plugins/ssrmatching/vo.itarget b/plugins/ssrmatching/vo.itarget
deleted file mode 100644
index b0eb388349..0000000000
--- a/plugins/ssrmatching/vo.itarget
+++ /dev/null
@@ -1 +0,0 @@
-ssrmatching.vo
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e53d19b595..62ff9ac708 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 f7cc08ca21..75db04f77f 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 db2e5da957..c36542aebc 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 b4654bfb56..52d1ffe06d 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 79d2e46942..34875cbcdd 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 de49a521fd..4bde427b15 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 aa574e41c5..4101dc23e4 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 0000000000..806ffb771f
--- /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 0000000000..7c973f88b5
--- /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 0000000000..5daaf9edbf
--- /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 0000000000..390133162f
--- /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 0000000000..88f219be30
--- /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 0000000000..bb1222489a
--- /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/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
new file mode 100755
index 0000000000..6301aa03c0
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+if make VERBOSE=1; then
+  # make command should have failed (but didn't)
+  exit 1
+else
+  # make command should have failed (and it indeed did)
+  exit 0
+fi
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
new file mode 100755
index 0000000000..991fb4a61d
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-bypass-API
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+make VERBOSE=1
diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4
index 72765abe04..e7d0bfe1f8 100644
--- a/test-suite/coq-makefile/template/src/test.ml4
+++ b/test-suite/coq-makefile/template/src/test.ml4
@@ -1,3 +1,4 @@
+open API
 open Ltac_plugin
 DECLARE PLUGIN "test_plugin"
 let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml
index a01d0865a8..e134abd840 100644
--- a/test-suite/coq-makefile/template/src/test_aux.ml
+++ b/test-suite/coq-makefile/template/src/test_aux.ml
@@ -1 +1 @@
-let tac = Proofview.tclUNIT ()
+let tac = API.Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli
index 10020f27de..2e7ad1529f 100644
--- a/test-suite/coq-makefile/template/src/test_aux.mli
+++ b/test-suite/coq-makefile/template/src/test_aux.mli
@@ -1 +1 @@
-val tac : unit Proofview.tactic
+val tac : unit API.Proofview.tactic
diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v
index 84a4009d7e..19eea94b19 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 8ce6f9795c..f064dfe763 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 4074896420..6a4fd007df 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 f4ecfd7362..ffea0819a5 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 71536c68fb..250aecafd4 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 36d643a447..d45343fe60 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 6aa3df9830..d9a649fadc 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 0000000000..e5520b8dfa
--- /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 0000000000..02b7eada83
--- /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/save-logs.sh b/test-suite/save-logs.sh
index fb8a1c1b0a..b613621085 100755
--- a/test-suite/save-logs.sh
+++ b/test-suite/save-logs.sh
@@ -9,7 +9,7 @@ mkdir "$SAVEDIR"
 # keep this synced with test-suite/Makefile
 FAILMARK="==========> FAILURE <=========="
 
-FAILED=$(mktemp)
+FAILED=$(mktemp /tmp/coq-check-XXXXX)
 find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED"
 
 rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR"
diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v
new file mode 100644
index 0000000000..6aeb05f54e
--- /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 82f726fa7c..c36313ec16 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/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
deleted file mode 100644
index 5eba0b6235..0000000000
--- a/theories/Logic/vo.itarget
+++ /dev/null
@@ -1,35 +0,0 @@
-Berardi.vo
-PropExtensionalityFacts.vo
-ChoiceFacts.vo
-ClassicalChoice.vo
-ClassicalDescription.vo
-ClassicalEpsilon.vo
-ClassicalFacts.vo
-Classical_Pred_Type.vo
-Classical_Prop.vo
-ClassicalUniqueChoice.vo
-Classical.vo
-ConstructiveEpsilon.vo
-Decidable.vo
-Description.vo
-Diaconescu.vo
-Epsilon.vo
-Eqdep_dec.vo
-EqdepFacts.vo
-Eqdep.vo
-WeakFan.vo
-WKL.vo
-FunctionalExtensionality.vo
-ExtensionalityFacts.vo
-ExtensionalFunctionRepresentative.vo
-Hurkens.vo
-IndefiniteDescription.vo
-JMeq.vo
-ProofIrrelevanceFacts.vo
-ProofIrrelevance.vo
-PropFacts.vo
-PropExtensionality.vo
-RelationalChoice.vo
-SetIsType.vo
-SetoidChoice.vo
-FinFun.vo
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 8e2f75fc9c..e4f1359774 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -27,11 +27,6 @@ let rec print_prefix_list sep = function
   | x :: l -> print sep; print x; print_prefix_list sep l
   | [] -> ()
 
-(* These are the Coq library directories that are used for
- * plugin development
- *)
-let lib_dirs = Envars.coq_src_subdirs
-
 let usage () =
   output_string stderr "Usage summary:\
 \n\
@@ -73,6 +68,7 @@ let usage () =
 \n[-f file]: take the contents of file as arguments\
 \n[-o file]: output should go in file file\
 \n	Output file outside the current directory is forbidden.\
+\n[-bypass-API]: when compiling plugins, bypass Coq API\
 \n[-h]: print this usage summary\
 \n[--help]: equivalent to [-h]\n";
   exit 1
@@ -197,9 +193,12 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
     (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes))
 ;;
 
-let generate_conf_coq_config oc args =
+let generate_conf_coq_config oc args bypass_API =
   section oc "Coq configuration.";
-  Envars.print_config ~prefix_var_name:"COQMF_" oc;
+  let src_dirs = if bypass_API
+                 then Coq_config.all_src_dirs
+                 else Coq_config.api_dirs @ Coq_config.plugins_dirs in
+  Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
   fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); 
 ;;
 
@@ -258,7 +257,7 @@ let generate_conf oc project args  =
   fprintf oc "# %s\n\n" (String.concat " " (List.map quote args));
   generate_conf_files oc project;
   generate_conf_includes oc project;
-  generate_conf_coq_config oc args;
+  generate_conf_coq_config oc args project.bypass_API;
   generate_conf_defs oc project;
   generate_conf_doc oc project;
   generate_conf_extra_target oc project.extra_targets;
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 240531f123..c1f0182d9c 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -83,7 +83,7 @@ let parse_args () =
 
     | ("-config" | "--config") :: _ ->
         Envars.set_coqlib ~fail:(fun x -> x);
-        Envars.print_config stdout;
+        Envars.print_config stdout Coq_config.all_src_dirs;
         exit 0
       
     |"--print-version" :: _ ->
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8fca302687..16fe405551 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -124,7 +124,7 @@ let init_ocaml_path () =
     Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl])
   in
     Mltop.add_ml_dir (Envars.coqlib ());
-    List.iter add_subdir Envars.coq_src_subdirs
+    List.iter add_subdir Coq_config.all_src_dirs
 
 let get_compat_version = function
   | "8.7" -> Flags.Current
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 26ee413fb0..31450ebd51 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -621,7 +621,7 @@ let init_toplevel arglist =
       Spawned.init_channels ();
       Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
       if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
-      if !print_config then (Envars.print_config stdout; exit (exitcode ()));
+      if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
       if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
       init_load_path ();
diff --git a/vernac/classes.ml b/vernac/classes.ml
index dc5ce1a537..8e6a0f6a72 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 34b9b97d8c..a114553cdb 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 69492759be..ef16df5b75 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 =