Merge branch 'v8.6'

45 files changed, 462 insertions, 213 deletions

diff --git a/Makefile.dev b/Makefile.dev
index d9db7055f..8c1812da1 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -164,7 +164,7 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \
 .PHONY: init theories-light noreal
 .PHONY: logic arith bool narith zarith qarith lists strings sets
 .PHONY: fsets relations wellfounded reals setoids sorting numbers
-.PHONY: msets mmaps compat
+.PHONY: msets mmaps compat parith classes program unicode structures vectors
 
 ################
 ### 4) plugins
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 1efed6ef7..4daf98f87 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -4,16 +4,19 @@
 
  
 \asection{Short description of the tactics}
-\tacindex{psatz}  \tacindex{lra} 
+\tacindex{psatz}  \tacindex{lra} \tacindex{lia}  \tacindex{nia} \tacindex{nra} 
 \label{sec:psatz-hurry}
 The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to
 several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and
 {\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by
-  pre-processing the goal with the {\tt zify} tactic.}
+  pre-processing the goal with the {\tt zify} tactic.}.
+It also possible to get the tactics for integers by a {\tt Require Import Lia}, rationals {\tt Require Import Lqa} 
+and reals {\tt Require Import Lra}.
 \begin{itemize}
 \item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia});
 \item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia});
-\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra});
+\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic  (see Section~\ref{sec:lra});
+\item {\tt nra} is an incomplete proof procedure for non-linear (real or rational) arithmetic  (see Section~\ref{sec:nra});
 \item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and
   {\tt n} is an optional integer limiting the proof search depth is is an
   incomplete proof procedure for non-linear arithmetic. It is based on
@@ -114,36 +117,6 @@ The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_s
 %
 There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}.
 
-\asection{{\tt psatz}: a proof procedure for non-linear arithmetic}
-\label{sec:psatz}
-The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$.
-In theory, such a proof search is complete -- if the goal is provable the search eventually stops.
-Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a
-refutation. 
-
-To illustrate the working of the tactic, consider we wish to prove the following Coq goal.
-\begin{coq_eval}
-Require Import ZArith Psatz.
-Open Scope Z_scope.
-\end{coq_eval}
-\begin{coq_example*}
-Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
-\end{coq_example*}
-\begin{coq_eval}
-intro x; psatz Z 2.
-\end{coq_eval}
-Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the
-cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times
-(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in
-bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2,
-x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By
-Theorem~\ref{thm:psatz}, the goal is valid.
-%
-
-%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a
-%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$.
-%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$.
-%
 
 \asection{{\tt lia}: a tactic for linear integer arithmetic}
 \tacindex{lia}
@@ -219,22 +192,61 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2]
 We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and
 recursively search for a proof.
 
-\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic}
-\tacindex{nia}
-\label{sec:nia}
-The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear  integer arithmetic.
+
+\asection{{\tt nra}: a proof procedure for non-linear arithmetic}
+\tacindex{nra}
+\label{sec:nra}
+The {\tt nra} tactic is an {\emph experimental} proof procedure for non-linear arithmetic.
 %
 The tactic performs a limited amount of non-linear reasoning before running the
-linear prover of {\tt lia}.
+linear prover of {\tt lra}.
 This pre-processing does the following:
 \begin{itemize}
 \item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a
   monomial, the context is enriched with $x^2\ge 0$;
 \item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$.
 \end{itemize}
-After pre-processing, the linear prover of {\tt lia} searches for a proof
+After this pre-processing, the linear prover of {\tt lra} searches for a proof
 by abstracting monomials by variables.
 
+\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic}
+\tacindex{nia}
+\label{sec:nia}
+The {\tt nia} tactic is a proof procedure for non-linear  integer arithmetic.
+%
+It performs a pre-processing similar to {\tt nra}. The obtained goal is solved using the linear integer prover {\tt lia}.
+
+\asection{{\tt psatz}: a proof procedure for non-linear arithmetic}
+\label{sec:psatz}
+The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$.
+In theory, such a proof search is complete -- if the goal is provable the search eventually stops.
+Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a
+refutation. 
+
+To illustrate the working of the tactic, consider we wish to prove the following Coq goal.
+\begin{coq_eval}
+Require Import ZArith Psatz.
+Open Scope Z_scope.
+\end{coq_eval}
+\begin{coq_example*}
+Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+\end{coq_example*}
+\begin{coq_eval}
+intro x; psatz Z 2.
+\end{coq_eval}
+Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the
+cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times
+(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in
+bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2,
+x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By
+Theorem~\ref{thm:psatz}, the goal is valid.
+%
+
+%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a
+%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$.
+%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$.
+%
+
 
 
 %%% Local Variables: 
diff --git a/engine/evd.mli b/engine/evd.mli
index 942414511..b47b389d1 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -98,11 +98,12 @@ type evar_info = {
   (** Optional content of the evar. *)
   evar_filter : Filter.t;
   (** Boolean mask over {!evar_hyps}. Should have the same length.
-      TODO: document me more. *)
+      When filtered out, the corresponding variable is not allowed to occur
+      in the solution *)
   evar_source : Evar_kinds.t located;
   (** Information about the evar. *)
   evar_candidates : constr list option;
-  (** TODO: document this *)
+  (** List of possible solutions when known that it is a finite list *)
   evar_extra : Store.t
   (** Extra store, used for clever hacks. *)
 }
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 50b3f2c0a..5b6bad349 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -785,7 +785,6 @@ object(self)
   method private handle_failure_aux
     ?(move_insert=false) (safe_id, (loc : (int * int) option), msg)
   =
-    messages#clear;
     messages#push Feedback.Error msg;
     ignore(self#process_feedback ());
     if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index fe69be9e4..06a132732 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -46,23 +46,37 @@ let xml_to_string xml =
   let () = iter (Richpp.repr xml) in
   Buffer.contents buf
 
-let translate s = s
-
-let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg =
+let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
+  (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that
+      it has to reimplement its own helper function. Unluckily, it relies on
+      a slow algorithm, so that we have to have our own quicker version here.
+      Alas, it is still much slower than the native version... *)
+  if CList.is_empty tags then buf#insert ~iter:(buf#get_iter_at_mark mark) text
+  else
+    let it = buf#get_iter_at_mark mark in
+    let () = buf#move_mark rmark ~where:it in
+    let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in
+    let start = buf#get_iter_at_mark mark in
+    let stop = buf#get_iter_at_mark rmark in
+    let iter tag = buf#apply_tag tag start stop in
+    List.iter iter tags
+
+let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
   let open Xml_datatype in
   let tag name =
-    let name = translate name in
     match GtkText.TagTable.lookup buf#tag_table name with
     | None -> raise Not_found
     | Some tag -> new GText.tag tag
   in
+  let rmark = `MARK (buf#create_mark buf#start_iter) in
   let rec insert tags = function
-  | PCData s -> buf#insert ~tags:(List.rev tags) s
+  | PCData s -> insert_with_tags buf mark rmark tags s
   | Element (t, _, children) ->
     let tags = try tag t :: tags with Not_found -> tags in
     List.iter (fun xml -> insert tags xml) children
   in
-  insert tags (Richpp.repr msg)
+  let () = try insert tags (Richpp.repr msg) with _ -> () in
+  buf#delete_mark rmark
 
 let set_location = ref  (function s -> failwith "not ready")
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 491e8e823..e32a4d9e3 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -54,7 +54,7 @@ val flash_info : ?delay:int -> string -> unit
 
 val xml_to_string : Richpp.richpp -> string
 
-val insert_xml : ?tags:GText.tag list ->
+val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list ->
   #GText.buffer_skel -> Richpp.richpp -> unit
 
 val set_location : (string -> unit) ref
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 3241a962d..64327d74f 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -33,6 +33,7 @@ type obj = {
 }
 
 let preferences : obj Util.String.Map.t ref = ref Util.String.Map.empty
+let unknown_preferences : string list Util.String.Map.t ref = ref Util.String.Map.empty
 
 class type ['a] repr =
 object
@@ -617,19 +618,19 @@ let save_pref () =
   then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
   let () = try GtkData.AccelMap.save accel_file with _ -> () in
   let add = Util.String.Map.add in
-  let (++) x f = f x in
   let fold key obj accu = add key (obj.get ()) accu in
- 
-    (Util.String.Map.fold fold !preferences Util.String.Map.empty) ++
-    Config_lexer.print_file pref_file
+  let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in
+  let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in
+  Config_lexer.print_file pref_file prefs
 
 let load_pref () =
   let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
 
     let m = Config_lexer.load_file loaded_pref_file in
     let iter name v =
-      try (Util.String.Map.find name !preferences).set v
-      with _ -> ()
+      if Util.String.Map.mem name !preferences then
+        try (Util.String.Map.find name !preferences).set v with _ -> ()
+      else unknown_preferences := Util.String.Map.add name v !unknown_preferences
     in
     Util.String.Map.iter iter m
 
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 758f383d6..0330b8eff 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -43,6 +43,7 @@ let message_view () : message_view =
     ~tag_table:Tags.Message.table ()
   in
   let text_buffer = new GText.buffer buffer#as_buffer in
+  let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in
   let box = GPack.vbox () in
   let scroll = GBin.scrolled_window
     ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(box#pack ~expand:true) () in
@@ -69,7 +70,8 @@ let message_view () : message_view =
       new message_view_signals_impl box#as_widget push
 
     method clear =
-      buffer#set_text ""
+      buffer#set_text "";
+      buffer#move_mark (`MARK mark) ~where:buffer#start_iter
 
     method push level msg =
       let tags = match level with
@@ -83,8 +85,9 @@ let message_view () : message_view =
       | Xml_datatype.Element (_, _, children) -> List.exists non_empty children
       in
       if non_empty (Richpp.repr msg) then begin
-        Ideutils.insert_xml buffer ~tags msg;
-        buffer#insert (*~tags*) "\n";
+        let mark = `MARK mark in
+        Ideutils.insert_xml ~mark buffer ~tags msg;
+        buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n";
         push#call (level, msg)
       end
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f3e0682bd..fcb4a345e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -124,6 +124,14 @@ let rec cases_pattern_fold_map loc g e = function
       let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in
       e', PatCstr (loc,cstr,patl',na')
 
+let subst_binder_type_vars l = function
+  | Evar_kinds.BinderType (Name id) as e ->
+     let id =
+       try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
+       with Not_found -> id in
+     Evar_kinds.BinderType (Name id)
+  | e -> e
+
 let rec subst_glob_vars l = function
   | GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r)
   | GProd (loc,Name id,bk,t,c) ->
@@ -136,6 +144,7 @@ let rec subst_glob_vars l = function
 	try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
 	with Not_found -> id in
       GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
+  | GHole (loc,x,naming,arg) -> GHole (loc,subst_binder_type_vars l x,naming,arg)
   | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *)
 
 let ldots_var = Id.of_string ".."
@@ -1128,13 +1137,15 @@ let match_notation_constr u c (metas,pat) =
   List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
     match typ with
     | NtnTypeConstr ->
-       ((Id.List.assoc x terms, scl)::terms',termlists',binders')
+      let term = try Id.List.assoc x terms with Not_found -> raise No_match in
+       ((term, scl)::terms',termlists',binders')
     | NtnTypeOnlyBinder ->
        ((find_binder x, scl)::terms',termlists',binders')
     | NtnTypeConstrList ->
        (terms',(Id.List.assoc x termlists,scl)::termlists',binders')
     | NtnTypeBinderList ->
-       (terms',termlists',(Id.List.assoc x binderlists,scl)::binders'))
+      let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in
+       (terms',termlists',(bl, scl)::binders'))
     metas ([],[],[])
 
 (* Matching cases pattern *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 156e00368..ed44704df 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -106,7 +106,7 @@ type showable =
   | ShowTree
   | ShowProofNames
   | ShowIntros of bool
-  | ShowMatch of lident
+  | ShowMatch of reference
   | ShowThesis
 
 type comment =
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 3864df6c9..ef4b50130 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1929,13 +1929,15 @@ let compile_constant env sigma prefix ~interactive con cb =
           arg|])))::
             [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix
 
-let loaded_native_files = ref ([] : string list)
+module StringOrd = struct type t = string let compare = String.compare end
+module StringSet = Set.Make(StringOrd)
 
-let is_loaded_native_file s = String.List.mem s !loaded_native_files
+let loaded_native_files = ref StringSet.empty
+
+let is_loaded_native_file s = StringSet.mem s !loaded_native_files
 
 let register_native_file s =
-  if not (is_loaded_native_file s) then
-    loaded_native_files := s :: !loaded_native_files
+  loaded_native_files := StringSet.add s !loaded_native_files
 
 let is_code_loaded ~interactive name =
   match !name with
diff --git a/library/library.ml b/library/library.ml
index 12090183a..d44f796a7 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -452,13 +452,13 @@ let intern_from_file f =
 module DPMap = Map.Make(DirPath)
 
 let rec intern_library (needed, contents) (dir, f) from =
-  Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
   (* Look if in the current logical environment *)
   try (find_library dir).libsum_digests, (needed, contents)
   with Not_found ->
   (* Look if already listed and consequently its dependencies too *)
   try (DPMap.find dir contents).library_digests, (needed, contents)
   with Not_found ->
+  Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
   (* [dir] is an absolute name which matches [f] which must be in loadpath *)
   let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
   let m = intern_from_file f in
@@ -468,16 +468,18 @@ let rec intern_library (needed, contents) (dir, f) from =
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
   Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
-  m.library_digests, intern_library_deps (needed, contents) dir m (Some f)
+  m.library_digests, intern_library_deps (needed, contents) dir m f
 
 and intern_library_deps libs dir m from =
   let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in
   (dir :: needed, DPMap.add dir m contents )
 
 and intern_mandatory_library caller from libs (dir,d) =
-  let digest, libs = intern_library libs (dir, None) from in
+  let digest, libs = intern_library libs (dir, None) (Some from) in
   if not (Safe_typing.digest_match ~actual:digest ~required:d) then
-    errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir);
+    errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++
+    str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
+    over library " ++ pr_dirpath dir);
   libs
 
 let rec_intern_library libs (dir, f) =
@@ -551,12 +553,20 @@ let in_require : require_obj -> obj =
 
 let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
 
+let warn_require_in_module =
+  CWarnings.create ~name:"require-in-module" ~category:"deprecated"
+                   (fun () -> strbrk "Require inside a module is" ++
+                              strbrk " deprecated and strongly discouraged. " ++
+                              strbrk "You can Require a module at toplevel " ++
+                              strbrk "and optionally Import it inside another one.")
+
 let require_library_from_dirpath modrefl export =
   let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
   let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
   let modrefl = List.map fst modrefl in
     if Lib.is_module_or_modtype () then
       begin
+        warn_require_in_module ();
 	add_anonymous_leaf (in_require (needed,modrefl,None));
 	Option.iter (fun exp ->
 	  add_anonymous_leaf (in_import_library (modrefl,exp)))
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index be47293fc..e50b0520b 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -816,9 +816,11 @@ END
 
 TACTIC EXTEND is_evar
 | [ "is_evar" constr(x) ] ->
-    [ match kind_of_term x with
+    [ Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
+      match Evarutil.kind_of_term_upto sigma x with
         | Evar _ -> Proofview.tclUNIT ()
         | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar")
+      end
     ]
 END
 
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 09454f3e8..153ca5bf5 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1564,6 +1564,10 @@ let newfail n s =
 
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
+  (** For compatibility *)
+  let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
+  let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
+  let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in
   let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
@@ -1575,12 +1579,17 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
         let gls = List.rev (Evd.fold_undefined fold undef []) in
 	match clause, prf with
 	| Some id, Some p ->
-            let tac = Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
+            let tac = Tacticals.New.tclTHENLIST [
+              Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h };
+              beta_hyp id;
+              Proofview.Unsafe.tclNEWGOALS gls;
+            ] in
             Proofview.Unsafe.tclEVARS undef <*>
 	    assert_replacing id newt tac
 	| Some id, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_hyp_no_check (LocalAssum (id, newt))
+            convert_hyp_no_check (LocalAssum (id, newt)) <*>
+            beta_hyp id
 	| None, Some p ->
             Proofview.Unsafe.tclEVARS undef <*>
             Proofview.Goal.enter { enter = begin fun gl ->
@@ -1595,12 +1604,6 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             Proofview.Unsafe.tclEVARS undef <*>
             convert_concl_no_check newt DEFAULTcast
   in
-  let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
-  let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
-  let opt_beta = match clause with
-  | None -> Proofview.tclUNIT ()
-  | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp)
-  in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -1625,7 +1628,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
       let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
       treat sigma res <*>
       (** For compatibility *)
-      beta <*> opt_beta <*> Proofview.shelve_unifiable
+      beta <*> Proofview.shelve_unifiable
     with
     | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
       raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index aa7e096a9..8b2e1ee1a 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1813,13 +1813,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      (* spiwack: until the tactic is in the monad *)
-      Proofview.Trace.name_tactic (fun () -> Pp.str"<reduce>") begin
       Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
         let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
         Sigma.Unsafe.of_pair (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl), sigma)
       end }
-      end
   | TacChange (None,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 2acccfdf5..bec891f7f 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -103,6 +103,9 @@ open Error
 
 let current_file = ref ""
 
+let get_current_file () =
+  !current_file
+
 let set_current_file ~fname =
   current_file := fname
 
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index d99ba3557..3b4891d9a 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -17,7 +17,13 @@ type location_table
 val location_table : unit -> location_table
 val restore_location_table : location_table -> unit
 
-(** [set_current_file fname] sets the filename in locations emitted by the lexer *)
+
+(** [get_current_file fname] returns the filename used in locations emitted by
+    the lexer *)
+val get_current_file : unit -> string
+
+(** [set_current_file fname] sets the filename used in locations emitted by the
+    lexer *)
 val set_current_file : fname:string -> unit
 
 val check_ident : string -> unit
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index b0ff8b64f..1e3c4b880 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -88,7 +88,7 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
       | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
       | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
-      | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id)
+      | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id)
       | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis
       | IDENT "Guarded" -> VernacCheckGuard
       (* Hints for Auto and EAuto *)
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 52bf5ed3d..6974f8d99 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -8,7 +8,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria)      2013                             *)
+(*  Frédéric Besson (Irisa/Inria)      2013-2016                        *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -19,24 +19,24 @@ Require Import VarMap.
 Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
+
 Ltac preprocess :=
   zify ; unfold Z.succ in * ; unfold Z.pred in *.
 
-Ltac lia :=
-  preprocess;
-  xlia ;
-  abstract (
-      intros __wit __varmap __ff ;
-      change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
-
-Ltac nia :=
-  preprocess;
-  xnlia ;
-  abstract (
-      intros __wit __varmap __ff ;
-      change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
+Ltac zchange := 
+  intros __wit __varmap __ff ;
+  change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
+  apply (ZTautoChecker_sound __ff __wit).
+
+Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity.
+
+Ltac zchecker_abstract := abstract (zchange ; vm_cast_no_check (eq_refl true)).
+
+Ltac zchecker := zchecker_abstract || zchecker_no_abstract .
+
+Ltac lia := preprocess; xlia ; zchecker.
+               
+Ltac nia := preprocess; xnlia ; zchecker.
 
 
 (* Local Variables: *)
diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v
new file mode 100644
index 000000000..e3414b849
--- /dev/null
+++ b/plugins/micromega/Lqa.v
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria)      2016                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import QMicromega.
+Require Import QArith.
+Require Import RingMicromega.
+Require Import VarMap.
+Require Coq.micromega.Tauto.
+Declare ML Module "micromega_plugin".
+
+Ltac rchange := 
+  intros __wit __varmap __ff ;
+  change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
+  apply (QTautoChecker_sound __ff __wit).
+
+Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.
+Ltac rchecker_abstract   := abstract (rchange ; vm_cast_no_check (eq_refl true)).
+
+Ltac rchecker := (rchecker_abstract || rchecker_no_abstract).
+
+(** Here, lra stands for linear rational arithmetic *)
+Ltac lra := lra_Q ; rchecker.
+
+(** Here, nra stands for non-linear rational arithmetic *)
+Ltac nra := xnqa ; rchecker.
+
+Ltac xpsatz dom d :=
+  let tac := lazymatch dom with
+  | Q =>
+    (sos_Q || psatz_Q d) ;
+      (* If csdp is not installed, the previous step might not produce any
+    progress: the rest of the tactical will then fail. Hence the 'try'. *)
+      try  rchecker
+  | _ => fail "Unsupported domain"
+  end in tac.
+
+Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
+Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
+
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v
new file mode 100644
index 000000000..4d9cf22dd
--- /dev/null
+++ b/plugins/micromega/Lra.v
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria)      2016                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import RMicromega.
+Require Import QMicromega.
+Require Import Rdefinitions.
+Require Import RingMicromega.
+Require Import VarMap.
+Require Coq.micromega.Tauto.
+Declare ML Module "micromega_plugin".
+
+Ltac rchange := 
+  intros __wit __varmap __ff ;
+  change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
+  apply (RTautoChecker_sound __ff __wit).
+
+Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.
+Ltac rchecker_abstract   := abstract (rchange ; vm_cast_no_check (eq_refl true)).
+
+Ltac rchecker := rchecker_abstract || rchecker_no_abstract.
+
+(** Here, lra stands for linear real arithmetic *)
+Ltac lra := unfold Rdiv in * ;   lra_R ; rchecker.
+
+(** Here, nra stands for non-linear real arithmetic *)
+Ltac nra := unfold Rdiv in * ; xnra ; rchecker.
+
+Ltac xpsatz dom d :=
+  let tac := lazymatch dom with
+  | R =>
+    (sos_R || psatz_R d) ;
+    (* If csdp is not installed, the previous step might not produce any
+    progress: the rest of the tactical will then fail. Hence the 'try'. *)
+    try rchecker
+  | _ => fail "Unsupported domain"
+ end in tac.
+
+Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
+Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
+
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index fafd8a5f2..c81c025a5 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -8,7 +8,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2016                             *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -21,50 +21,30 @@ Require Import Rdefinitions.
 Require Import RingMicromega.
 Require Import VarMap.
 Require Coq.micromega.Tauto.
-Declare ML Module "micromega_plugin".
+Require Lia.
+Require Lra.
+Require Lqa.
 
-Ltac preprocess := 
-    zify ; unfold Z.succ in * ; unfold Z.pred in *.
+Declare ML Module "micromega_plugin".
 
-Ltac lia :=
-  preprocess;
-  xlia ;
-  abstract (
-  intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
+Ltac lia := Lia.lia.
 
-Ltac nia :=
-  preprocess;
-  xnlia ;
-  abstract (
-  intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
+Ltac nia := Lia.nia.
 
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | Z =>
-    (sos_Z || psatz_Z d) ;
-      abstract(
-    intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-    apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))
+    (sos_Z || psatz_Z d) ; Lia.zchecker
   | R =>
     (sos_R || psatz_R d) ;
     (* If csdp is not installed, the previous step might not produce any
     progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try (abstract(intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-        apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
-  | Q =>
-    (sos_Q || psatz_Q d) ;
+    try Lra.rchecker
+  | Q => (sos_Q || psatz_Q d) ;
     (* If csdp is not installed, the previous step might not produce any
     progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try  (abstract(intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-        apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
+    try  Lqa.rchecker
   | _ => fail "Unsupported domain"
   end in tac.
 
@@ -73,22 +53,9 @@ Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
 
 Ltac psatzl dom :=
   let tac := lazymatch dom with
-  | Z => lia
-  | Q =>
-    psatzl_Q ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try (abstract(intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-        apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
-  | R =>
-    unfold Rdiv in * ; 
-    psatzl_R ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try abstract((intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-        apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
+  | Z => Lia.lia
+  | Q => Lqa.lra
+  | R => Lra.lra
   | _ => fail "Unsupported domain"
   end in tac.
 
@@ -97,13 +64,7 @@ Ltac lra :=
   first [ psatzl R | psatzl Q ].
 
 Ltac nra := 
-  unfold Rdiv in * ; 
-  xnra ;     
-  abstract 
-    (intros __wit __varmap __ff ;
-     change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-     apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
-                                                                       
+  first [ Lra.nra | Lqa.nra ].  
 
 
 (* Local Variables: *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index b8e5e66ca..faf3b3e69 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1437,7 +1437,36 @@ let rcst_domain_spec  = lazy {
 
 open Proofview.Notations
 
- 
+(** Naive topological sort of constr according to the subterm-ordering *)
+
+(* An element is minimal x is minimal w.r.t y if 
+   x <= y or (x and y are incomparable) *)
+
+let is_min le x y =
+  if le x y then true
+  else    if le y x then false else true
+
+let is_minimal le l c = List.for_all (is_min le c) l
+    
+let find_rem p l =
+  let rec xfind_rem  acc l =
+    match l with
+    | [] -> (None, acc)
+    | x :: l -> if p x then (Some x, acc @ l)
+      else xfind_rem (x::acc) l in
+  xfind_rem [] l
+
+let find_minimal le l = find_rem (is_minimal le l) l
+  
+let rec mk_topo_order le l =
+  match find_minimal le l with
+  | (None , _) -> []
+  | (Some v,l') -> v ::  (mk_topo_order le l')
+
+    
+let topo_sort_constr l = mk_topo_order Termops.dependent l
+
+
 (**
   * Instanciate the current Coq goal with a Micromega formula, a varmap, and a
   * witness.
@@ -1464,7 +1493,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
       ]
       (Tacmach.pf_concl gl))
    ;
-   Tactics.generalize env ;
+      Tactics.generalize (topo_sort_constr env) ;
    Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
   ] 
   end }
@@ -1774,7 +1803,7 @@ let micromega_order_changer cert env ff  =
          ("__wit", cert, cert_typ)
         ]
         (Tacmach.pf_concl gl)));
-      Tactics.generalize env ;
+      Tactics.generalize (topo_sort_constr env) ;
       Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
      ]
   end }
@@ -1851,7 +1880,7 @@ module Cache = PHashtable(struct
   let hash  = Hashtbl.hash
 end)
 
-let csdp_cache = "csdp.cache"
+let csdp_cache = ".csdp.cache"
 
 (**
   * Build the command to call csdpcert, and launch it. This in turn will call
@@ -1997,9 +2026,9 @@ module CacheQ = PHashtable(struct
   let hash  = Hashtbl.hash
 end)
 
-let memo_zlinear_prover = CacheZ.memo "lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s)
-let memo_nlia = CacheZ.memo "nlia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s)
-let memo_nra = CacheQ.memo "nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
+let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s)
+let memo_nlia = CacheZ.memo ".nia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s)
+let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
 
 
  
@@ -2064,7 +2093,6 @@ let non_linear_prover_Z str o  = {
   pp_f    =  fun o x -> pp_pol pp_z o (fst x)
 }
 
-
 let linear_Z =   {
   name    = "lia";
  get_option = get_lia_option;
@@ -2100,11 +2128,7 @@ let tauto_lia ff =
   * solvers
   *)
 
-let psatzl_Z =
- micromega_gen parse_zarith  Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
-  [ linear_Z ] 
-
-let psatzl_Q =
+let lra_Q =
  micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
   [ linear_prover_Q ] 
 
@@ -2112,7 +2136,7 @@ let psatz_Q i  =
  micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
   [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ]
 
-let psatzl_R  =
+let lra_R  =
  micromega_genr [ linear_prover_R ]
 
 let psatz_R i  =
@@ -2136,21 +2160,21 @@ let sos_R  =
  micromega_genr  [ non_linear_prover_R "pure_sos" None ] 
 
 
-let xlia  =
-  try 
-    micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
+let xlia  =  micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ linear_Z ] 
-  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 let xnlia  =
-  try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ nlinear_Z ] 
-  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 let nra  = 
  micromega_genr  [ nlinear_prover_R ] 
 
+let nqa  =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
+  [ nlinear_prover_R ]
+
+   
 
 (* Local Variables: *)
 (* coding: utf-8 *)
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index e6b5cc60d..974dcee87 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -37,6 +37,12 @@ TACTIC EXTEND NRA
 [ "xnra"  ] -> [  (Coq_micromega.nra)]
 END
 
+TACTIC EXTEND NQA
+[ "xnqa"  ] -> [  (Coq_micromega.nqa)]
+END
+
+
+  
 TACTIC EXTEND Sos_Z
 | [ "sos_Z" ] -> [ (Coq_micromega.sos_Z) ]
    END
@@ -50,11 +56,11 @@ TACTIC EXTEND Sos_R
 END
 
 TACTIC EXTEND LRA_Q
-[ "psatzl_Q"  ] -> [   (Coq_micromega.psatzl_Q) ]
+[ "lra_Q"  ] -> [   (Coq_micromega.lra_Q) ]
 END
 
 TACTIC EXTEND LRA_R
-[ "psatzl_R"  ] -> [   (Coq_micromega.psatzl_R) ]
+[ "lra_R"  ] -> [   (Coq_micromega.lra_R) ]
 END
 
 TACTIC EXTEND PsatzR
diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget
index bf6a1a7db..cb4b2b8a5 100644
--- a/plugins/micromega/vo.itarget
+++ b/plugins/micromega/vo.itarget
@@ -10,4 +10,6 @@ Tauto.vo
 VarMap.vo
 ZCoeff.vo
 ZMicromega.vo
-Lia.vo
\ No newline at end of file
+Lia.vo
+Lqa.vo
+Lra.vo
\ No newline at end of file
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 935e2d076..a00e4bab3 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -793,6 +793,22 @@ end
 
 let do_not_tag _ x = x
 
+let split_token tag s =
+  let len = String.length s in
+  let rec parse_string off i =
+    if Int.equal i len then
+      if Int.equal off i then mt () else tag (str (String.sub s off (i - off)))
+    else if s.[i] == ' ' then
+      if Int.equal off i then parse_space 1 (succ i)
+      else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i)
+    else parse_string off (succ i)
+  and parse_space spc i =
+    if Int.equal i len then str (String.make spc ' ')
+    else if s.[i] == ' ' then parse_space (succ spc) (succ i)
+    else str (String.make spc ' ') ++ parse_string i (succ i)
+  in
+  parse_string 0 0
+
 (** Instantiating Make with tagging functions that only add style
     information. *)
 include Make (struct
@@ -801,7 +817,7 @@ include Make (struct
     let tag_evar        = tag Tag.evar
     let tag_type        = tag Tag.univ
     let tag_unparsing   = function
-    | UnpTerminal s -> tag Tag.notation
+    | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s
     | _ -> do_not_tag ()
     let tag_constr_expr = do_not_tag
     let tag_path = tag Tag.path
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 0d47b34df..40ce28dc0 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -591,7 +591,7 @@ module Make
           | ShowTree -> keyword "Show Tree"
           | ShowProofNames -> keyword "Show Conjectures"
           | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
-          | ShowMatch id -> keyword "Show Match " ++ pr_lident id
+          | ShowMatch id -> keyword "Show Match " ++ pr_reference id
           | ShowThesis -> keyword "Show Thesis"
         in
         return (pr_showable s)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 139862b8f..28952b9a7 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -93,7 +93,7 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
   (** Select the goals *)
   let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
-  let trace () = Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)) in
+  let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT ()) >>= fun () ->
   Proofview.Unsafe.tclEVARS sigma >>= fun () ->
   Proofview.Unsafe.tclSETGOALS comb
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 73a90f611..2d1f725ef 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -229,10 +229,8 @@ module Make(T : Task) = struct
     | (Die | TQueue.BeingDestroyed) ->
         giveback_exec_token (); kill proc; exit ()
     | Sys_error _ | Invalid_argument _ | End_of_file ->
-        giveback_exec_token ();
         T.on_task_cancellation_or_expiration_or_slave_death !last_task;
-        kill proc;
-        exit ()
+        giveback_exec_token (); kill proc; exit ()
   end
 
   module Pool = WorkerPool.Make(Model)
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 5e4e34114..cf4143dbb 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -482,6 +482,18 @@ let start_proof_com kind thms hook =
 
 (* Saving a proof *)
 
+let keep_admitted_vars = ref true
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "keep section variables in admitted proofs";
+      optkey   = ["Keep"; "Admitted"; "Variables"];
+      optread  = (fun () -> !keep_admitted_vars);
+      optwrite = (fun b -> keep_admitted_vars := b) }
+
 let save_proof ?proof = function
   | Vernacexpr.Admitted ->
       let pe =
@@ -495,7 +507,8 @@ let save_proof ?proof = function
               error "Admitted requires an explicit statement";
             let typ = Option.get const_entry_type in
             let ctx = Evd.evar_context_universe_context (fst universes) in
-            Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
+            let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
+            Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
         | None ->
             let pftree = Pfedit.get_pftreestate () in
             let id, k, typ = Pfedit.current_proof_statement () in
@@ -504,7 +517,8 @@ let save_proof ?proof = function
             let pproofs, _univs =
               Proof_global.return_proof ~allow_partial:true () in
             let sec_vars =
-              match  Pfedit.get_used_variables(), pproofs with
+              if not !keep_admitted_vars then None
+              else match  Pfedit.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
               | None, (pproof, _) :: _ -> 
                   let env = Global.env () in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1672b7bd1..f9f8e8715 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1500,9 +1500,11 @@ let head_of_constr h c =
   let c = head_of_constr c in
   letin_tac None (Name h) c None Locusops.allHyps
 
-let not_evar c = match kind_of_term c with
-| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
-| _ -> Proofview.tclUNIT ()
+let not_evar c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match Evarutil.kind_of_term_upto sigma c with
+  | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
+  | _ -> Proofview.tclUNIT ()
 
 let is_ground c gl =
   if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7519339ca..b54624f89 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -871,14 +871,17 @@ let reduction_clause redexp cl =
 	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
 
 let reduce redexp cl =
+  let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in
+  Proofview.Trace.name_tactic trace begin
   Proofview.Goal.enter { enter = begin fun gl ->
-  let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
-  let redexps = reduction_clause redexp cl in
+  let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
+  let redexps = reduction_clause redexp cl' in
   let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
   Tacticals.New.tclMAP (fun (where,redexp) ->
     e_reduct_option ~check
       (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps
   end }
+  end
 
 (* Unfolding occurrences of a constant *)
 
@@ -4945,7 +4948,7 @@ module New = struct
   let reduce_after_refine =
     reduce
       (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]})
-      {onhyps=None; concl_occs=AllOccurrences }
+      {onhyps=Some []; concl_occs=AllOccurrences }
 
   let refine ?unsafe c =
     Refine.refine ?unsafe c <*>
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
new file mode 100644
index 000000000..75dd38fde
--- /dev/null
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/bugs/closed/3920.v b/test-suite/bugs/closed/3920.v
new file mode 100644
index 000000000..a4adb23cc
--- /dev/null
+++ b/test-suite/bugs/closed/3920.v
@@ -0,0 +1,7 @@
+Require Import Setoid.
+Axiom P : nat -> Prop.
+Axiom P_or : forall x y, P (x + y) <-> P x \/ P y.
+Lemma foo (H : P 3) : False.
+eapply or_introl in H.
+erewrite <- P_or in H.
+(* Error: No such hypothesis: H *)
diff --git a/test-suite/bugs/closed/4764.v b/test-suite/bugs/closed/4764.v
new file mode 100644
index 000000000..e545cc1b7
--- /dev/null
+++ b/test-suite/bugs/closed/4764.v
@@ -0,0 +1,5 @@
+Notation prop_fun x y := (fun (x : Prop) => y).
+Definition foo := fun (p : Prop) => p.
+Definition bar := fun (_ : Prop) => O.
+Print foo.
+Print bar.
diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v
new file mode 100644
index 000000000..9a35bcf95
--- /dev/null
+++ b/test-suite/bugs/closed/4893.v
@@ -0,0 +1,4 @@
+Goal True.
+evar (P: Prop).
+assert (H : P); [|subst P]; [exact I|].
+let T := type of H in not_evar T.
diff --git a/test-suite/bugs/closed/5043.v b/test-suite/bugs/closed/5043.v
new file mode 100644
index 000000000..4e6a0f878
--- /dev/null
+++ b/test-suite/bugs/closed/5043.v
@@ -0,0 +1,8 @@
+Unset Keep Admitted Variables.
+
+Section a.
+  Context (x : Type).
+  Definition foo : Type.
+  Admitted.
+End a.
+Check foo : Type.
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
deleted file mode 100644
index 8e5708cf0..000000000
--- a/test-suite/csdp.cache
+++ /dev/null
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index 47e6005b9..d001e8f7f 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -6,32 +6,29 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import Psatz.
+Require Import Lqa.
 Require Import QArith.
 
 Lemma plus_minus : forall x y,
   0 == x + y -> 0 ==  x -y -> 0 == x /\ 0 == y.
 Proof.
   intros.
-  psatzl Q.
+  lra.
 Qed.
 
-
-
-
 (* Other (simple) examples *)
 Open Scope Q_scope.
 
 Lemma binomial : forall x y:Q, ((x+y)^2 == x^2 + (2 # 1) *x*y + y^2).
 Proof.
   intros.
-  psatzl Q.
+  lra.
 Qed.
 
 
 Lemma hol_light19 : forall m n, (2 # 1) * m + n == (n + m) + m.
 Proof.
-  intros ; psatzl Q.
+  intros ; lra.
 Qed.
 Open Scope Z_scope.
 Open Scope Q_scope.
@@ -60,7 +57,11 @@ Lemma vcgen_25 : forall
   (( 1# 1) == (-2 # 1) * i + it).
 Proof.
   intros.
-  psatzl Q.
+  lra.
+Qed.
+
+Goal forall x : Q, x * x >= 0.
+  intro; nra. 
 Qed.
 
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 2eed7e951..89c08c770 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -6,7 +6,7 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import Psatz.
+Require Import Lra.
 Require Import Reals.
 
 Open Scope R_scope.
@@ -15,7 +15,7 @@ Lemma yplus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
-  psatzl R.
+  lra.
 Qed.
 
 (* Other (simple) examples *)
@@ -23,13 +23,13 @@ Qed.
 Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2).
 Proof.
   intros.
-  psatzl R.
+  lra.
 Qed.
 
 
 Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
 Proof.
-  intros ; psatzl R.
+  intros ; lra.
 Qed.
 
 
@@ -57,7 +57,7 @@ Lemma vcgen_25 : forall
   (( 1 ) = (-2  ) * i + it).
 Proof.
   intros.
-  psatzl R.
+  lra.
 Qed.
 
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
@@ -72,5 +72,5 @@ Proof.
 Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
-intros; split_Rabs; psatzl R.
+intros; split_Rabs; lra.
 Qed.
\ No newline at end of file
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 0ec1dbfbc..1f148becc 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -33,4 +33,13 @@ Lemma compact_proof : forall z,
 Proof.
  intros.
  lia.
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma dummy_ex : exists (x:Z),  x = x.
+Proof.
+  eexists.
+  lia.
+  Unshelve.
+  exact Z0.
+Qed.
+  
\ No newline at end of file
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index b5c91e347..fff86d6fa 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -1,3 +1,5 @@
+Require Coq.Unicode.Utf8.
+
 (** The purpose of this file is to test printing of the destructive
     patterns used in binders ([fun] and [forall]). *)
 
@@ -37,7 +39,7 @@ End WithParameters.
 (** Some test involving unicode notations. *)
 Module WithUnicode.
 
-  Require Import Coq.Unicode.Utf8.
+  Import Coq.Unicode.Utf8.
 
   Check λ '((x,y) : A*B),  (y,x).
   Check ∀ '(x,y), swap (x,y) = (y,x).
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 21b78b533..8ae1a9195 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -76,3 +76,7 @@ Require Coq.Lists.List.
 Require Coq.Vectors.VectorDef.
 Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
 Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.
+
+(** In 8.4, the statement of admitted lemmas did not depend on the section
+    variables. *)
+Unset Keep Admitted Variables.
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6dba2c51e..de3d14483 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -81,7 +81,6 @@ let open_file_twice_if verbosely longfname =
   let in_chan = open_utf8_file_in longfname in
   let verb_ch =
     if verbosely then Some (open_utf8_file_in longfname) else None in
-  CLexer.set_current_file longfname;
   let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
   (in_chan, longfname, (po, verb_ch))
 
@@ -190,6 +189,8 @@ let rec vernac_com checknav (loc,com) =
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
 	let st = save_translator_coqdoc () in
+        let old_lexer_file = CLexer.get_current_file () in
+        CLexer.set_current_file f;
 	if !Flags.beautify_file then
 	  begin
 	    chan_beautify := open_out (f^beautify_suffix);
@@ -199,9 +200,11 @@ let rec vernac_com checknav (loc,com) =
 	  try
             Flags.silently (read_vernac_file verbosely) f;
 	    restore_translator_coqdoc st;
+            CLexer.set_current_file old_lexer_file;
 	  with reraise ->
             let reraise = CErrors.push reraise in
 	    restore_translator_coqdoc st;
+            CLexer.set_current_file old_lexer_file;
 	    iraise reraise
 	end
 
@@ -271,12 +274,16 @@ let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
 let load_vernac verb file =
   chan_beautify :=
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
+    let old_lexer_file = CLexer.get_current_file () in
   try
+    CLexer.set_current_file file;
     Flags.silently (read_vernac_file verb) file;
     if !Flags.beautify_file then close_out !chan_beautify;
+    CLexer.set_current_file old_lexer_file;
   with any ->
     let (e, info) = CErrors.push any in
     if !Flags.beautify_file then close_out !chan_beautify;
+    CLexer.set_current_file old_lexer_file;
     iraise (disable_drop e, info)
 
 let warn_file_no_extension =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 40c7c7010..10bbdc358 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -122,9 +122,7 @@ let show_intro all =
     [Not_found] is raised if the given string isn't the qualid of
     a known inductive type. *)
 
-let make_cases s =
-  let qualified_name = Libnames.qualid_of_string s in
-  let glob_ref = Nametab.locate qualified_name in
+let make_cases_aux glob_ref =
   match glob_ref with
     | Globnames.IndRef i ->
 	let {Declarations.mind_nparams = np}
@@ -144,11 +142,16 @@ let make_cases s =
 	  carr tarr []
     | _ -> raise Not_found
 
+let make_cases s =
+  let qualified_name = Libnames.qualid_of_string s in
+  let glob_ref = Nametab.locate qualified_name in
+  make_cases_aux glob_ref
+
 (** Textual display of a generic "match" template *)
 
 let show_match id =
   let patterns =
-    try make_cases (Id.to_string (snd id))
+    try make_cases_aux (Nametab.global id)
     with Not_found -> error "Unknown inductive type."
   in
   let pr_branch l =