115 files changed, 338 insertions, 130 deletions

diff --git a/.gitignore b/.gitignore
index 7434f62127..35cdf9b4e8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -122,10 +122,10 @@ g_*.ml
 ide/project_file.ml
 parsing/compat.ml
 parsing/cLexer.ml
-ltac/coretactics.ml
-ltac/extratactics.ml
-ltac/extraargs.ml
-ltac/profile_ltac_tactics.ml
+plugins/ltac/coretactics.ml
+plugins/ltac/extratactics.ml
+plugins/ltac/extraargs.ml
+plugins/ltac/profile_ltac_tactics.ml
 ide/coqide_main.ml
 plugins/ssrmatching/ssrmatching.ml
 
diff --git a/.travis.yml b/.travis.yml
index de16f2d0b4..5ed0809a52 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -30,6 +30,7 @@ env:
   - TEST_TARGET="ci-cpdt"
   - TEST_TARGET="ci-geocoq"
   - TEST_TARGET="ci-fiat-crypto"
+  - TEST_TARGET="ci-fiat-parsers"
   - TEST_TARGET="ci-flocq"
   - TEST_TARGET="ci-hott"
   - TEST_TARGET="ci-iris-coq"
diff --git a/Makefile.ci b/Makefile.ci
index e4b5832f60..897318c4dd 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,5 +1,5 @@
 CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \
-           ci-color ci-math-classes ci-tlc ci-fiat-crypto \
+           ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \
            ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \
            ci-unimath
 
diff --git a/Makefile.common b/Makefile.common
index 2cf4d01695..df705034e7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -55,14 +55,14 @@ MKDIR:=install -d
 CORESRCDIRS:=\
   config 	lib		kernel	intf	kernel/byterun	library \
   engine 	pretyping	interp	proofs	parsing 	printing \
-  tactics 	vernac		stm		toplevel 	ltac
+  tactics 	vernac		stm		toplevel
 
 PLUGINDIRS:=\
   omega		romega 		micromega 	quote \
   setoid_ring 	extraction 	fourier \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          decl_mode	btauto \
-  ssrmatching
+  ssrmatching	ltac
 
 SRCDIRS:=\
   $(CORESRCDIRS)  \
@@ -77,14 +77,13 @@ BYTERUN:=$(addprefix kernel/byterun/, \
   coq_fix_code.o coq_memory.o coq_values.o coq_interp.o )
 
 # LINK ORDER:
-# Beware that highparsing.cma should appear before ltac.cma
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
 CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
-	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma
+	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma
 
 TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
@@ -120,6 +119,7 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
         string_syntax_plugin.cmo )
 DECLMODECMO:=plugins/decl_mode/decl_mode_plugin.cmo
 DERIVECMO:=plugins/derive/derive_plugin.cmo
+LTACCMO:=plugins/ltac/ltac_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 
 PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
@@ -127,7 +127,7 @@ PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
         $(FOURIERCMO) $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
-	$(DERIVECMO) $(SSRMATCHINGCMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(LTACCMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)
diff --git a/Makefile.dev b/Makefile.dev
index 8c1812da18..ea6b8b9194 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -121,10 +121,9 @@ pretyping: pretyping/pretyping.cma
 highparsing: parsing/highparsing.cma
 stm: stm/stm.cma
 toplevel: toplevel/toplevel.cma
-ltac: ltac/ltac.cma
 
 .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
-.PHONY: engine highparsing stm toplevel ltac
+.PHONY: engine highparsing stm toplevel
 
 ######################
 ### 3) theories files
@@ -183,6 +182,7 @@ RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO))
 EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO))
 CCVO:=
 DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO))
+LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO))
 
 omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
 micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
@@ -194,9 +194,10 @@ funind: $(FUNINDCMO) $(FUNINDVO)
 cc: $(CCVO) $(CCCMO)
 rtauto: $(RTAUTOVO) $(RTAUTOCMO)
 btauto: $(BTAUTOVO) $(BTAUTOCMO)
+ltac: $(LTACVO) $(LTACCMO)
 
 .PHONY: omega micromega setoid_ring nsatz extraction
-.PHONY: fourier funind cc rtauto btauto
+.PHONY: fourier funind cc rtauto btauto ltac
 
 #################################
 ### Misc other development rules
diff --git a/configure.ml b/configure.ml
index 48e167c99f..e711367510 100644
--- a/configure.ml
+++ b/configure.ml
@@ -261,7 +261,7 @@ module Prefs = struct
   let withdoc = ref false
   let geoproof = ref false
   let byteonly = ref false
-  let debug = ref false
+  let debug = ref true
   let profile = ref false
   let annotate = ref false
   let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
@@ -336,7 +336,9 @@ let args_options = Arg.align [
   "-byteonly", Arg.Set Prefs.byteonly,
     " Compiles only bytecode version of Coq";
   "-debug", Arg.Set Prefs.debug,
-    " Add debugging information in the Coq executables";
+    " Deprecated";
+  "-nodebug", Arg.Clear Prefs.debug,
+    " Do not add debugging information in the Coq executables";
   "-profile", Arg.Set Prefs.profile,
     " Add profiling information in the Coq executables";
   "-annotate", Arg.Set Prefs.annotate,
diff --git a/dev/base_include b/dev/base_include
index 0abcefc38e..242405ae29 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -17,7 +17,7 @@
 #directory "grammar";;
 #directory "intf";;
 #directory "stm";;
-#directory "ltac";;
+#directory "vernac";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
@@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_tac    = Pcoq.parse_string Pltac.tactic;;
+let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
new file mode 100755
index 0000000000..15d73078fd
--- /dev/null
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+fiat_parsers_CI_BRANCH=master
+fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git
+
+git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} fiat
+
+( cd fiat && make -j ${NJOBS} parsers )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index aaffc9d484..0c07564c02 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git_checkout mz-8.6 https://github.com/ejgallego/HoTT.git HoTT
+git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT
 
 ( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} )
diff --git a/dev/core.dbg b/dev/core.dbg
index 38b9b29463..698db63d23 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -12,6 +12,7 @@ load_printer proofs.cma
 load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
+load_printer vernac.cma
 load_printer stm.cma
 load_printer toplevel.cma
 load_printer highparsing.cma
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index f54f3fcc8e..8d2d055908 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -40,6 +40,24 @@ important things:
 - Some printing functions were moved from Pptactic to Pputils
 - A part of Tacexpr has been moved to Tactypes
 
+The folder itself has been turned into a plugin. This does not change much,
+but because it is a packed plugin, it may wreak havoc for third-party plugins
+depending on any module defined in the ltac/ directory. Namely, even if
+everything looks OK at compile time, a plugin can fail to load at link time
+because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with
+an error of the form:
+
+Error: while loading myplugin.cmxs, no implementation available for Foo.
+
+In particular, most EXTEND macros will trigger this problem even if they
+seemingly do not use any Ltac module, as their expansion do.
+
+The solution is simple, and consists in adding a statement "open Ltac_plugin"
+in each file using a Ltac module, before such a module is actually called. An
+alternative solution would be to fully qualify Ltac modules, e.g. turning any
+call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not
+work for EXTEND macros though.
+
 ** Error handling **
 
 - All error functions now take an optional parameter `?loc:Loc.t`. For
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 46caca8d6f..3850c05fd9 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -20,7 +20,7 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \
 	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
 	-I $COQTOP/library -I $COQTOP/engine \
-	-I $COQTOP/pretyping -I $COQTOP/parsing \
+	-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
         -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
@@ -32,6 +32,6 @@ exec $OCAMLDEBUG \
         -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
 	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
         -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
-        -I $COQTOP/plugins/xml \
+        -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
         -I $COQTOP/ide \
 	"$@"
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4fcad88202..dc354b130b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -234,7 +234,7 @@ let ppenvwithcst e = pp
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
    str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
 
-let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x))
+let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
 let ppobj obj = Format.print_string (Libobject.object_tag obj)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c102d8e117..3ed8733df5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1591,7 +1591,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let idl_tmp = Array.map
           (fun ((loc,id),bl,ty,_) ->
             let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
-            let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbl in
+            let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> 
+                      Loc.raise ~loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in
             (List.rev rbl,
              intern_type env' ty,env')) dl in
 	let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 948d624a27..66d3c91859 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -927,19 +927,19 @@ let locate_notation prglob ntn scope =
   match ntns with
   | [] -> str "Unknown notation"
   | _ ->
-    t (str "Notation            " ++
-    tab () ++ str "Scope     " ++ tab () ++ fnl () ++
+    str "Notation" ++ fnl () ++
     prlist (fun (ntn,l) ->
       let scope = find_default ntn scopes in
       prlist
 	(fun (sc,r,(_,df)) ->
 	  hov 0 (
-	    pr_notation_info prglob df r ++ tbrk (1,2) ++
-	    (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++
-	    tbrk (1,2) ++
-	    (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ())
+	    pr_notation_info prglob df r ++
+	    (if String.equal sc default_scope then mt ()
+             else (spc () ++ str ": " ++ str sc)) ++
+	    (if Option.equal String.equal (Some sc) scope
+             then spc () ++ str "(default interpretation)" else mt ())
 	    ++ fnl ()))
-	l) ntns)
+	l) ntns
 
 let collect_notation_in_scope scope sc known =
   assert (not (String.equal scope default_scope));
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 37bbe0ce87..87ca253253 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -23,12 +23,9 @@ type ppbox =
   | PpHOVB of int
   | PpHVB of int
   | PpVB of int
-  | PpTB
 
 type ppcut =
   | PpBrk of int * int
-  | PpTbrk of int * int
-  | PpTab
   | PpFnl
 
 let ppcmd_of_box = function
@@ -36,13 +33,10 @@ let ppcmd_of_box = function
   | PpHOVB n -> hov n
   | PpHVB n -> hv n
   | PpVB n -> v n
-  | PpTB   -> t
 
 let ppcmd_of_cut = function
-  | PpTab -> tab ()
   | PpFnl -> fnl ()
   | PpBrk(n1,n2) -> brk(n1,n2)
-  | PpTbrk(n1,n2) -> tbrk(n1,n2)
 
 type unparsing =
   | UnpMetaVar of int * parenRelation
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index de7a42eee5..09dc369437 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -23,12 +23,9 @@ type ppbox =
   | PpHOVB of int
   | PpHVB of int
   | PpVB of int
-  | PpTB
 
 type ppcut =
   | PpBrk of int * int
-  | PpTbrk of int * int
-  | PpTab
   | PpFnl
 
 val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 407cec0842..fd57b70ca9 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -60,6 +60,9 @@ let rec cases_pattern_fold_names f a = function
   | CPatPrim _ | CPatAtom _ -> a
   | CPatCast _ -> assert false
 
+let ids_of_pattern =
+  cases_pattern_fold_names Id.Set.add Id.Set.empty
+
 let ids_of_pattern_list =
   List.fold_left
     (Loc.located_fold_left
@@ -173,7 +176,8 @@ let split_at_annot bl na =
               (List.rev ans, LocalRawAssum (r, k, t) :: rest)
             end
 	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
-        | LocalPattern _ :: rest -> assert false
+        | LocalPattern (loc,_,_) :: rest ->
+            Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
             user_err ~loc 
 			 (str "No parameter named " ++ Nameops.pr_id id ++ str".")
@@ -196,8 +200,9 @@ let map_local_binders f g e bl =
         (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl)
     | LocalRawDef((loc,na),ty) ->
         (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl)
-    | LocalPattern _ ->
-        assert false in
+    | LocalPattern (loc,pat,t) ->
+        let ids = ids_of_pattern pat in
+        (Id.Set.fold g ids e, LocalPattern (loc,pat,Option.map (f e) t)::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 810c346990..94ca4c72dd 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -299,7 +299,7 @@ and pp_bytecodes c =
   | Ksequence (l1, l2) :: c ->
       pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
   | i :: c ->
-      tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
+      pp_instr i ++ fnl () ++ pp_bytecodes c
 
 (*spiwack: moved this type in this file  because I needed it for
   retroknowledge which can't depend from cbytegen *)
diff --git a/lib/pp.ml b/lib/pp.ml
index f3bb475392..a51b4458fb 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -72,8 +72,6 @@ open Pp_control
       this block is small enough to fit on a single line
    \item[hovbox:] Horizontal or Vertical block: breaks lead to new line
       only when necessary to print the content of the block
-   \item[tbox:] Tabulation block: go to tabulation marks and no line breaking
-      (except if no mark yet on the reste of the line)
    \end{description}
  *)
 
@@ -82,7 +80,6 @@ type block_type =
   | Pp_vbox of int
   | Pp_hvbox of int
   | Pp_hovbox of int
-  | Pp_tbox
 
 type str_token =
 | Str_def of string
@@ -92,14 +89,11 @@ type 'a ppcmd_token =
   | Ppcmd_print of 'a
   | Ppcmd_box of block_type * ('a ppcmd_token Glue.t)
   | Ppcmd_print_break of int * int
-  | Ppcmd_set_tab
-  | Ppcmd_print_tbreak of int * int
   | Ppcmd_white_space of int
   | Ppcmd_force_newline
   | Ppcmd_print_if_broken
   | Ppcmd_open_box of block_type
   | Ppcmd_close_box
-  | Ppcmd_close_tbox
   | Ppcmd_comment of string list
   | Ppcmd_open_tag of Tag.t
   | Ppcmd_close_tag
@@ -161,8 +155,6 @@ let utf8_length s =
 let str s = Glue.atom(Ppcmd_print (Str_def s))
 let stras (i, s) = Glue.atom(Ppcmd_print (Str_len (s, i)))
 let brk (a,b) = Glue.atom(Ppcmd_print_break (a,b))
-let tbrk (a,b) = Glue.atom(Ppcmd_print_tbreak (a,b))
-let tab () = Glue.atom(Ppcmd_set_tab)
 let fnl () = Glue.atom(Ppcmd_force_newline)
 let pifb () = Glue.atom(Ppcmd_print_if_broken)
 let ws n = Glue.atom(Ppcmd_white_space n)
@@ -212,16 +204,13 @@ let h n s = Glue.atom(Ppcmd_box(Pp_hbox n,s))
 let v n s = Glue.atom(Ppcmd_box(Pp_vbox n,s))
 let hv n s = Glue.atom(Ppcmd_box(Pp_hvbox n,s))
 let hov n s = Glue.atom(Ppcmd_box(Pp_hovbox n,s))
-let t s = Glue.atom(Ppcmd_box(Pp_tbox,s))
 
 (* Opening and closing of boxes *)
 let hb n = Glue.atom(Ppcmd_open_box(Pp_hbox n))
 let vb n = Glue.atom(Ppcmd_open_box(Pp_vbox n))
 let hvb n = Glue.atom(Ppcmd_open_box(Pp_hvbox n))
 let hovb n = Glue.atom(Ppcmd_open_box(Pp_hovbox n))
-let tb () = Glue.atom(Ppcmd_open_box Pp_tbox)
 let close () = Glue.atom(Ppcmd_close_box)
-let tclose () = Glue.atom(Ppcmd_close_tbox)
 
 (* Opening and closed of tags *)
 let open_tag t = Glue.atom(Ppcmd_open_tag t)
@@ -263,7 +252,6 @@ let pp_dirs ?pp_tag ft =
     | Pp_vbox n   -> Format.pp_open_vbox ft n
     | Pp_hvbox n  -> Format.pp_open_hvbox ft n
     | Pp_hovbox n -> Format.pp_open_hovbox ft n
-    | Pp_tbox     -> Format.pp_open_tbox ft ()
   in
   let rec pp_cmd = function
     | Ppcmd_print tok         ->
@@ -280,11 +268,8 @@ let pp_dirs ?pp_tag ft =
         Format.pp_close_box ft ()
     | Ppcmd_open_box bty      -> pp_open_box bty
     | Ppcmd_close_box         -> Format.pp_close_box ft ()
-    | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
     | Ppcmd_white_space n     -> Format.pp_print_break ft n 0
     | Ppcmd_print_break(m,n)  -> Format.pp_print_break ft m n
-    | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
-    | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n
     | Ppcmd_force_newline     -> Format.pp_force_newline ft ()
     | Ppcmd_print_if_broken   -> Format.pp_print_if_newline ft ()
     | Ppcmd_comment coms      -> List.iter (pr_com ft) coms
diff --git a/lib/pp.mli b/lib/pp.mli
index 8342a983de..f17908262c 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -15,8 +15,6 @@ type std_ppcmds
 val str   : string -> std_ppcmds
 val stras : int * string -> std_ppcmds
 val brk   : int * int -> std_ppcmds
-val tbrk  : int * int -> std_ppcmds
-val tab   : unit -> std_ppcmds
 val fnl   : unit -> std_ppcmds
 val pifb  : unit -> std_ppcmds
 val ws    : int -> std_ppcmds
@@ -58,7 +56,6 @@ val h : int -> std_ppcmds -> std_ppcmds
 val v : int -> std_ppcmds -> std_ppcmds
 val hv : int -> std_ppcmds -> std_ppcmds
 val hov : int -> std_ppcmds -> std_ppcmds
-val t : std_ppcmds -> std_ppcmds
 
 (** {6 Opening and closing of boxes} *)
 
@@ -66,9 +63,7 @@ val hb : int -> std_ppcmds
 val vb : int -> std_ppcmds
 val hvb : int -> std_ppcmds
 val hovb : int -> std_ppcmds
-val tb : unit -> std_ppcmds
 val close : unit -> std_ppcmds
-val tclose : unit -> std_ppcmds
 
 (** {6 Opening and closing of tags} *)
 
diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4
index f3e2c99f4c..2980274487 100644
--- a/plugins/btauto/g_btauto.ml4
+++ b/plugins/btauto/g_btauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "btauto_plugin"
 
 TACTIC EXTEND btauto
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 6f6811334d..7e76854b16 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Cctac
 open Stdarg
 
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index f68c01b18b..2b63ed6d6e 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Names
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index e19dc86c45..deb2ede1d5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Pp
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 18a35c6cfb..a71d20f0dc 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "decl_mode_plugin"
 
+open Ltac_plugin
 open Compat
 open Pp
 open Decl_expr
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 59a0bb5a2d..f5de638ed2 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Pp
 open Decl_expr
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index e1d6bb4a84..3ed959cf2c 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -12,6 +12,7 @@ DECLARE PLUGIN "extraction_plugin"
 
 (* ML names *)
 
+open Ltac_plugin
 open Genarg
 open Stdarg
 open Pcoq.Prim
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 260e86ad67..e28d6aa626 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
 open Formula
 open Sequent
 open Ground
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 628af4e719..d6cd7e2a08 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Formula
 open Sequent
 open Rules
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 7c665ae7b5..1960fa8355 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open FourierR
 
 DECLARE PLUGIN "fourier_plugin"
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6603a95a84..368b23be30 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*i camlp4deps: "grammar/grammar.cma" i*)
+open Ltac_plugin
 open Compat
 open Util
 open Term
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c8b4e48337..70333b063d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Tacexpr
 open Declarations
 open CErrors
diff --git a/ltac/tauto.mli b/plugins/ltac/Ltac.v
index e69de29bb2..e69de29bb2 100644
--- a/ltac/tauto.mli
+++ b/plugins/ltac/Ltac.v
diff --git a/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 28ff6df838..28ff6df838 100644
--- a/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
diff --git a/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index c5b26e6d56..c5b26e6d56 100644
--- a/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
diff --git a/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli
index e67540c055..e67540c055 100644
--- a/ltac/evar_tactics.mli
+++ b/plugins/ltac/evar_tactics.mli
diff --git a/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 53b726432c..53b726432c 100644
--- a/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
diff --git a/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index b12187e18a..b12187e18a 100644
--- a/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
diff --git a/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 1223f6eb4b..1223f6eb4b 100644
--- a/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
diff --git a/ltac/extratactics.mli b/plugins/ltac/extratactics.mli
index 18334dafe7..18334dafe7 100644
--- a/ltac/extratactics.mli
+++ b/plugins/ltac/extratactics.mli
diff --git a/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index a37cf306e1..4ec42c676f 100644
--- a/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -149,15 +149,6 @@ TACTIC EXTEND autounfold_one
     [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ]
       END
 
-TACTIC EXTEND autounfoldify
-| [ "autounfoldify" constr(x) ] -> [
-    let db = match Term.kind_of_term x with
-      | Term.Const (c,_) -> Names.Label.to_string (Names.con_label c)
-      | _ -> assert false
-    in Eauto.autounfold ["core";db] Locusops.onConcl 
-  ]
-END
-
 TACTIC EXTEND unify
 | ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ]
 | ["unify" constr(x) constr(y) "with" preident(base)  ] -> [
diff --git a/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index a28132a4b0..a28132a4b0 100644
--- a/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
diff --git a/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 905653281c..905653281c 100644
--- a/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
diff --git a/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 54229bb2ae..54229bb2ae 100644
--- a/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
diff --git a/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index d286a58708..d286a58708 100644
--- a/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
diff --git a/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b1c4f58eb8..b1c4f58eb8 100644
--- a/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
diff --git a/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 685c07c9a8..685c07c9a8 100644
--- a/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
diff --git a/ltac/ltac.mllib b/plugins/ltac/ltac_plugin.mlpack
index af1c7149da..af1c7149da 100644
--- a/ltac/ltac.mllib
+++ b/plugins/ltac/ltac_plugin.mlpack
diff --git a/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1d21118ae8..1d21118ae8 100644
--- a/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
diff --git a/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 810e1ec39a..810e1ec39a 100644
--- a/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
diff --git a/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fccee6e40a..fccee6e40a 100644
--- a/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
diff --git a/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 86e3ea5484..86e3ea5484 100644
--- a/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
diff --git a/ltac/pptacticsig.mli b/plugins/ltac/pptacticsig.mli
index 74ddd377ad..74ddd377ad 100644
--- a/ltac/pptacticsig.mli
+++ b/plugins/ltac/pptacticsig.mli
diff --git a/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 2514ededb0..2514ededb0 100644
--- a/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
diff --git a/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli
index e5e2e41975..e5e2e41975 100644
--- a/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
diff --git a/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 8cb76d81c5..8cb76d81c5 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
diff --git a/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3c5a109c0d..3c5a109c0d 100644
--- a/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
diff --git a/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 35c4483513..35c4483513 100644
--- a/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
diff --git a/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 42552c4846..42552c4846 100644
--- a/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
diff --git a/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index bfa423db20..bfa423db20 100644
--- a/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
diff --git a/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index df38a42cb9..df38a42cb9 100644
--- a/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
diff --git a/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 0b67f8726e..0b67f8726e 100644
--- a/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
diff --git a/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2e2b55be74..2e2b55be74 100644
--- a/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
diff --git a/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 969c118fb5..969c118fb5 100644
--- a/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
diff --git a/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index e3c2b4ad51..e3c2b4ad51 100644
--- a/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
diff --git a/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 94e14223aa..94e14223aa 100644
--- a/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
diff --git a/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9c25a16457..9c25a16457 100644
--- a/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
diff --git a/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 763e0dc22e..4b5d87fc3c 100644
--- a/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -782,6 +782,7 @@ let intern_ltac ist tac =
 let () =
   Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
   Genintern.register_intern0 wit_ref (lift intern_global_reference);
+  Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
   Genintern.register_intern0 wit_ident intern_ident';
   Genintern.register_intern0 wit_var (lift intern_hyp);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
diff --git a/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 71ca354fa1..71ca354fa1 100644
--- a/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
diff --git a/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 32bcdfb6a4..fda9142eda 100644
--- a/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2023,9 +2023,6 @@ let () =
 let () =
   declare_uniform wit_string
 
-let () =
-  declare_uniform wit_pre_ident
-
 let lift f = (); fun ist x -> Ftactic.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
@@ -2053,9 +2050,13 @@ let interp_destruction_arg' ist c = Ftactic.nf_enter { enter = begin fun gl ->
   Ftactic.return (interp_destruction_arg ist gl c)
 end }
 
+let interp_pre_ident ist env sigma s =
+  s |> Id.of_string |> interp_ident ist env sigma |> Id.to_string
+
 let () =
   register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
   register_interp0 wit_ref (lift interp_reference);
+  register_interp0 wit_pre_ident (lift interp_pre_ident);
   register_interp0 wit_ident (lift interp_ident);
   register_interp0 wit_var (lift interp_hyp);
   register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
diff --git a/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 6f64981eff..6f64981eff 100644
--- a/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
diff --git a/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 55de583613..b09bdda65c 100644
--- a/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -291,6 +291,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
 let () =
   Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
   Genintern.register_subst0 wit_ref subst_global_reference;
+  Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
   Genintern.register_subst0 wit_ident (fun _ v -> v);
   Genintern.register_subst0 wit_var (fun _ v -> v);
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
diff --git a/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index c1bf272579..c1bf272579 100644
--- a/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
diff --git a/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5cbddc7f64..5cbddc7f64 100644
--- a/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
diff --git a/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 520fb41eff..520fb41eff 100644
--- a/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
diff --git a/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index ef45ee47e1..ef45ee47e1 100644
--- a/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
diff --git a/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli
index 090207bcc3..090207bcc3 100644
--- a/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
diff --git a/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index a5ba3b8371..a5ba3b8371 100644
--- a/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
diff --git a/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli
index ed759a76db..ed759a76db 100644
--- a/ltac/tactic_option.mli
+++ b/plugins/ltac/tactic_option.mli
diff --git a/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 756958c2f0..756958c2f0 100644
--- a/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
diff --git a/plugins/ltac/tauto.mli b/plugins/ltac/tauto.mli
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/plugins/ltac/tauto.mli
diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget
new file mode 100644
index 0000000000..a28fb770be
--- /dev/null
+++ b/plugins/ltac/vo.itarget
@@ -0,0 +1 @@
+Ltac.vo
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 79020ed037..ccb6daa116 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,6 +16,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Stdarg
 open Tacarg
 
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 5f906a8dad..195dec3627 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -1,5 +1,3 @@
-DECLARE PLUGIN "nsatz_plugin"
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
@@ -10,6 +8,8 @@ DECLARE PLUGIN "nsatz_plugin"
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 27115abecc..6b711a1761 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -17,6 +17,7 @@
 
 DECLARE PLUGIN "omega_plugin"
 
+open Ltac_plugin
 open Names
 open Coq_omega
 open Stdarg
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index e7e6ecef98..f2c021f595 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Names
 open Misctypes
 open Tacexpr
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 2f38688d1f..9a54ad7789 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Ltac_plugin
 open Names
 open Refl_omega
 open Stdarg
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index d27b04834e..7e58ef9a3e 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "rtauto_plugin"
 
 TACTIC EXTEND rtauto
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 367a133330..35d6768c13 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -8,6 +8,7 @@
 
 module Search = Explore.Make(Proof_search)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Term
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 0987c44ae2..707ff79a6c 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Pp
 open Util
 open Libnames
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 657efe175b..59f23a6379 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Pp
 open CErrors
 open Util
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index fc988a2c5f..f4f6efa4a6 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -15,6 +15,7 @@ let frozen_lexer = CLexer.freeze () ;;
 (*i camlp4use: "pa_extend.cmo" i*)
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Names
 open Pp
 open Pcoq
diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v
new file mode 100644
index 0000000000..b2f00ffc65
--- /dev/null
+++ b/test-suite/bugs/closed/2417.v
@@ -0,0 +1,15 @@
+Parameter x y : nat.
+Axiom H : x = y.
+Hint Rewrite H : mybase.
+
+Ltac bar base := autorewrite with base.
+
+Tactic Notation "foo" ident(base) := autorewrite with base.
+
+Goal x = 0.
+  bar mybase.
+  now_show (y = 0).
+  Undo 2.
+  foo mybase.
+  now_show (y = 0).
+Abort.
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index a547685070..4b4f81dbce 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
            (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
 p = q.
 
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
 
+Set Default Proof Mode "Classic".
+
 Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
             (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
        @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index fc4c171e2c..8687eaab00 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,7 +2,9 @@
 (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
+Set Default Proof Mode "Classic".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
 Delimit Scope type_scope with type.
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index d34a2b8b1b..816bc845fd 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -4,6 +4,8 @@ Unset Strict Universe Declaration.
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *)
 
+Declare ML Module "ltac_plugin".
+
 Set Universe Polymorphism.
 Class Contr_internal (A : Type) := BuildContr { center : A }.
 Arguments center A {_}.
@@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A
 Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}.
 Check @contr_paths_contr0@{i}.
 Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *)
-(** It should have length 1, just like contr_paths_contr0 *)
\ No newline at end of file
+(** It should have length 1, just like contr_paths_contr0 *)
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 08628377f0..c6fcc24b6b 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -5,6 +5,7 @@ then from 269 lines to 255 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index ae17fb145d..64c7fd8eb1 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -5,6 +5,7 @@ then from 285 lines to 271 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -223,4 +224,4 @@ v = _) r,
     | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good"
     | [ |- ?G ] => fail 1 "bad" G
     end.
-    Fail rewrite concat_p_pp.
\ No newline at end of file
+    Fail rewrite concat_p_pp.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index da140c9318..64dd8c304f 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -2,6 +2,7 @@
 (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -1004,4 +1005,4 @@ Proof.
   Fail Timeout 1 Time rewrite !loops_functor_group.
   (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *)
   Timeout 1 do 3 rewrite loops_functor_group.
-Abort.
\ No newline at end of file
+Abort.
diff --git a/test-suite/bugs/closed/5346.v b/test-suite/bugs/closed/5346.v
new file mode 100644
index 0000000000..0118c18704
--- /dev/null
+++ b/test-suite/bugs/closed/5346.v
@@ -0,0 +1,29 @@
+Inductive comp : Type -> Type :=
+| Ret {T} : forall (v:T), comp T
+| Bind {T T'} : forall (p: comp T') (p': T' -> comp T), comp T.
+
+Notation "'do' x .. y <- p1 ; p2" :=
+  (Bind p1 (fun x => .. (fun y => p2) ..))
+    (at level 60, right associativity,
+     x binder, y binder).
+
+Definition Fst1 A B (p: comp (A*B)) : comp A :=
+  do '(a, b) <- p;
+    Ret a.
+
+Definition Fst2 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => Bind p (fun '(a, b) => Ret a)
+  end.
+
+Definition Fst3 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => do a <- p;
+          Ret (fst a)
+  end.
+
+Definition Fst A B (p: comp (A * B)) : comp A :=
+  match tt with
+  | _ => do '(a, b) <- p;
+          Ret a
+  end.
diff --git a/test-suite/success/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v
new file mode 100644
index 0000000000..f12b4d1f45
--- /dev/null
+++ b/test-suite/success/hintdb_in_ltac.v
@@ -0,0 +1,14 @@
+Definition x := 0.
+
+Hint Unfold x : mybase.
+
+Ltac autounfoldify base := autounfold with base.
+
+Tactic Notation "autounfoldify_bis" ident(base) := autounfold with base.
+
+Goal x = 0.
+  progress autounfoldify mybase.
+  Undo.
+  progress autounfoldify_bis mybase.
+  trivial.
+Qed.
diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v
new file mode 100644
index 0000000000..f5c25540ef
--- /dev/null
+++ b/test-suite/success/hintdb_in_ltac_bis.v
@@ -0,0 +1,15 @@
+Parameter Foo : Prop.
+Axiom H : Foo.
+
+Hint Resolve H : mybase.
+
+Ltac foo base := eauto with base.
+
+Tactic Notation "bar" ident(base) :=
+  typeclasses eauto with base.
+
+Goal Foo.
+  progress foo mybase.
+  Undo.
+  progress bar mybase.
+Qed.
\ No newline at end of file
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 58d3a2b38c..5a3d5631d5 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -24,7 +24,7 @@ Section Between.
 
   Lemma bet_eq : forall k l, l = k -> between k l.
   Proof.
-    induction 1; auto with arith.
+    intros * ->; auto with arith.
   Qed.
 
   Hint Resolve bet_eq: arith.
@@ -37,9 +37,7 @@ Section Between.
 
   Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
   Proof.
-    intros k l H; induction H as [|l H].
-    intros; absurd (S k <= k); auto with arith.
-    destruct H; auto with arith.
+    induction 1 as [|* [|]]; auto with arith.
   Qed.
   Hint Resolve between_Sk_l: arith.
 
@@ -74,32 +72,32 @@ Section Between.
 
   Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r.
   Proof.
-    red; auto with arith.
+    split; assumption.
   Qed.
   Hint Resolve in_int_intro: arith.
 
   Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
   Proof.
-    induction 1; intros.
-    apply le_lt_trans with r; auto with arith.
+    intros * [].
+    eapply le_lt_trans; eassumption.
   Qed.
 
   Lemma in_int_p_Sq :
-    forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat.
+    forall p q r, in_int p (S q) r -> in_int p q r \/ r = q.
   Proof.
-    induction 1; intros.
-    elim (le_lt_or_eq r q); auto with arith.
+    intros p q r [].
+    destruct (le_lt_or_eq r q); auto with arith.
   Qed.
 
   Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r.
   Proof.
-    induction 1; auto with arith.
+    intros * []; auto with arith.
   Qed.
   Hint Resolve in_int_S: arith.
 
   Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
   Proof.
-    induction 1; auto with arith.
+    intros * []; auto with arith.
   Qed.
   Hint Immediate in_int_Sp_q: arith.
 
@@ -107,10 +105,9 @@ Section Between.
     forall k l, between k l -> forall r, in_int k l r -> P r.
   Proof.
     induction 1; intros.
-    absurd (k < k); auto with arith.
-    apply in_int_lt with r; auto with arith.
-    elim (in_int_p_Sq k l r); intros; auto with arith.
-    rewrite H2; trivial with arith.
+    - absurd (k < k). { auto with arith. }
+      eapply in_int_lt; eassumption.
+    - destruct (in_int_p_Sq k l r) as [| ->]; auto with arith.
   Qed.
 
   Lemma in_int_between :
@@ -120,17 +117,17 @@ Section Between.
   Qed.
 
   Lemma exists_in_int :
-    forall k l, exists_between k l ->  exists2 m : nat, in_int k l m & Q m.
+    forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m.
   Proof.
-    induction 1.
-    case IHexists_between; intros p inp Qp; exists p; auto with arith.
-    exists l; auto with arith.
+    induction 1 as [* ? (p, ?, ?)|].
+    - exists p; auto with arith.
+    - exists l; auto with arith.
   Qed.
 
   Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l.
   Proof.
-    destruct 1; intros.
-    elim H0; auto with arith.
+    intros * (?, lt_r_l) ?.
+    induction lt_r_l; auto with arith.
   Qed.
 
   Lemma between_or_exists :
@@ -139,9 +136,11 @@ Section Between.
       (forall n:nat, in_int k l n -> P n \/ Q n) ->
       between k l \/ exists_between k l.
   Proof.
-    induction 1; intros; auto with arith.
-    elim IHle; intro; auto with arith.
-    elim (H0 m); auto with arith.
+    induction 1 as [|m ? IHle].
+    - auto with arith.
+    - intros P_or_Q.
+      destruct IHle; auto with arith.
+      destruct (P_or_Q m); auto with arith.
   Qed.
 
   Lemma between_not_exists :
@@ -150,14 +149,14 @@ Section Between.
       (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l.
   Proof.
     induction 1; red; intros.
-    absurd (k < k); auto with arith.
-    absurd (Q l); auto with arith.
-    elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'.
-    replace l with l'; auto with arith.
-    elim inl'; intros.
-    elim (le_lt_or_eq l' l); auto with arith; intros.
-    absurd (exists_between k l); auto with arith.
-    apply in_int_exists with l'; auto with arith.
+    - absurd (k < k); auto with arith.
+    - absurd (Q l). { auto with arith. }
+      destruct (exists_in_int k (S l)) as (l',[],?).
+      + auto with arith.
+      + replace l with l'. { trivial. }
+        destruct (le_lt_or_eq l' l); auto with arith.
+        absurd (exists_between k l). { auto with arith. }
+        eapply in_int_exists; eauto with arith.
   Qed.
 
   Inductive P_nth (init:nat) : nat -> nat -> Prop :=
@@ -168,15 +167,16 @@ Section Between.
 
   Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l.
   Proof.
-    induction 1; intros; auto with arith.
-    apply le_trans with (S k); auto with arith.
+    induction 1.
+    - auto with arith.
+    - eapply le_trans; eauto with arith.
   Qed.
 
   Definition eventually (n:nat) :=  exists2 k : nat, k <= n & Q k.
 
   Lemma event_O : eventually 0 -> Q 0.
   Proof.
-    induction 1; intros.
+    intros (x, ?, ?).
     replace 0 with x; auto with arith.
   Qed.
 
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index ddaf08bf71..11d80dbc33 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -262,6 +262,11 @@ Inductive comparison : Set :=
   | Lt : comparison
   | Gt : comparison.
 
+Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'.
+Proof.
+  destruct c, c'; intro H; reflexivity || destruct H; discriminate.
+Qed.
+
 Definition CompOpp (r:comparison) :=
   match r with
     | Eq => Eq
@@ -326,7 +331,6 @@ Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
  CompSpec eq lt x y c -> CompSpecT eq lt x y c.
 Proof. intros. apply CompareSpec2Type; assumption. Defined.
 
-
 (******************************************************************)
 (** * Misc Other Datatypes *)
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 85123cc444..fb1a7ab1c1 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -125,6 +125,25 @@ Proof.
   [apply Hl | apply Hr]; assumption.
 Qed.
 
+Theorem imp_iff_compat_l : forall A B C : Prop,
+  (B <-> C) -> ((A -> B) <-> (A -> C)).
+Proof.
+  intros ? ? ? [Hl Hr]; split; intros H ?; [apply Hl | apply Hr]; apply H; assumption.
+Qed.
+
+Theorem imp_iff_compat_r : forall A B C : Prop,
+  (B <-> C) -> ((B -> A) <-> (C -> A)).
+Proof.
+  intros ? ? ? [Hl Hr]; split; intros H ?; [apply H, Hr | apply H, Hl]; assumption.
+Qed.
+
+Theorem not_iff_compat : forall A B : Prop,
+  (A <-> B) -> (~ A <-> ~B).
+Proof.
+  intros; apply imp_iff_compat_r; assumption.
+Qed.
+
+
 (** Some equivalences *)
 
 Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False).
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 48fbe0793c..edcd53005e 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -88,9 +88,12 @@ Open Scope type_scope.
 
 (** ML Tactic Notations *)
 
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
 Declare ML Module "extratactics".
 Declare ML Module "g_auto".
 Declare ML Module "g_class".
 Declare ML Module "g_eqdecide".
 Declare ML Module "g_rewrite".
+
+Global Set Default Proof Mode "Classic".
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 7baf102aaa..d6385ee314 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -813,6 +813,34 @@ Proof.
   rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'.
 Qed.
 
+Lemma compare_cont_Lt_not_Lt p q :
+  compare_cont Lt p q <> Lt <-> p > q.
+Proof.
+  rewrite compare_cont_Lt_Lt.
+  unfold gt, le, compare.
+  now destruct compare_cont; split; try apply comparison_eq_stable.
+Qed.
+
+Lemma compare_cont_Lt_not_Gt p q :
+  compare_cont Lt p q <> Gt <-> p <= q.
+Proof.
+  apply not_iff_compat, compare_cont_Lt_Gt.
+Qed.
+
+Lemma compare_cont_Gt_not_Lt p q :
+  compare_cont Gt p q <> Lt <-> p >= q.
+Proof.
+  apply not_iff_compat, compare_cont_Gt_Lt.
+Qed.
+
+Lemma compare_cont_Gt_not_Gt p q :
+  compare_cont Gt p q <> Gt <-> p < q.
+Proof.
+  rewrite compare_cont_Gt_Gt.
+  unfold ge, lt, compare.
+  now destruct compare_cont; split; try apply comparison_eq_stable.
+Qed.
+
 (** We can express recursive equations for [compare] *)
 
 Lemma compare_xO_xO p q : (p~0 ?= q~0) = (p ?= q).
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 5aa397f8a9..1e3ab66876 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1367,7 +1367,7 @@ Lemma inj_testbit a n : 0<=n ->
  Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n).
 Proof. apply Z.testbit_Zpos. Qed.
 
-(** Some results concerning Z.neg *)
+(** Some results concerning Z.neg and Z.pos *)
 
 Lemma inj_neg p q : Z.neg p = Z.neg q -> p = q.
 Proof. now injection 1. Qed.
@@ -1375,18 +1375,54 @@ Proof. now injection 1. Qed.
 Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q.
 Proof. split. apply inj_neg. intros; now f_equal. Qed.
 
+Lemma inj_pos p q : Z.pos p = Z.pos q -> p = q.
+Proof. now injection 1. Qed.
+
+Lemma inj_pos_iff p q : Z.pos p = Z.pos q <-> p = q.
+Proof. split. apply inj_pos. intros; now f_equal. Qed.
+
 Lemma neg_is_neg p : Z.neg p < 0.
 Proof. reflexivity. Qed.
 
 Lemma neg_is_nonpos p : Z.neg p <= 0.
 Proof. easy. Qed.
 
+Lemma pos_is_pos p : 0 < Z.pos p.
+Proof. reflexivity. Qed.
+
+Lemma pos_is_nonneg p : 0 <= Z.pos p.
+Proof. easy. Qed.
+
+Lemma neg_le_pos p q : Zneg p <= Zpos q.
+Proof. easy. Qed.
+
+Lemma neg_lt_pos p q : Zneg p < Zpos q.
+Proof. easy. Qed.
+
+Lemma neg_le_neg p q : (q <= p)%positive -> Zneg p <= Zneg q.
+Proof. intros; unfold Z.le; simpl. now rewrite <- Pos.compare_antisym. Qed.
+
+Lemma neg_lt_neg p q : (q < p)%positive -> Zneg p < Zneg q.
+Proof. intros; unfold Z.lt; simpl. now rewrite <- Pos.compare_antisym. Qed.
+
+Lemma pos_le_pos p q : (p <= q)%positive -> Zpos p <= Zpos q.
+Proof. easy. Qed.
+
+Lemma pos_lt_pos p q : (p < q)%positive -> Zpos p < Zpos q.
+Proof. easy. Qed.
+
 Lemma neg_xO p : Z.neg p~0 = 2 * Z.neg p.
 Proof. reflexivity. Qed.
 
 Lemma neg_xI p : Z.neg p~1 = 2 * Z.neg p - 1.
 Proof. reflexivity. Qed.
 
+Lemma pos_xO p : Z.pos p~0 = 2 * Z.pos p.
+Proof. reflexivity. Qed.
+
+Lemma pos_xI p : Z.pos p~1 = 2 * Z.pos p + 1.
+Proof. reflexivity. Qed.
+
 Lemma opp_neg p : - Z.neg p = Z.pos p.
 Proof. reflexivity. Qed.
 
@@ -1402,6 +1438,9 @@ Proof. reflexivity. Qed.
 Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p.
 Proof. reflexivity. Qed.
 
+Lemma add_pos_pos p q : Z.pos p + Z.pos q = Z.pos (p+q).
+Proof. reflexivity. Qed.
+
 Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p).
 Proof. apply Z.divide_Zpos_Zneg_r. Qed.
 
@@ -1412,6 +1451,10 @@ Lemma testbit_neg a n : 0<=n ->
  Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)).
 Proof. apply Z.testbit_Zneg. Qed.
 
+Lemma testbit_pos a n : 0<=n ->
+ Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n).
+Proof. apply Z.testbit_Zpos. Qed.
+
 End Pos2Z.
 
 Module Z2Pos.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 73dee0cf24..18915216a0 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -339,7 +339,7 @@ Notation Zle_0_1 := Z.le_0_1 (compat "8.3").
 
 Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
 Proof.
-  easy.
+  exact Pos2Z.neg_le_pos.
 Qed.
 
 Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0.
@@ -350,12 +350,12 @@ Qed.
 (* weaker but useful (in [Z.pow] for instance) *)
 Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p.
 Proof.
- easy.
+  exact Pos2Z.pos_is_nonneg.
 Qed.
 
 Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0.
 Proof.
- easy.
+  exact Pos2Z.neg_is_neg.
 Qed.
 
 Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 624b9ced7d..4842a89151 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -50,9 +50,9 @@ let section s =
 let lib_dirs =
   ["kernel"; "lib"; "library"; "parsing";
    "pretyping"; "interp"; "printing"; "intf";
-   "proofs"; "tactics"; "tools"; "ltacprof";
+   "proofs"; "tactics"; "tools";
    "vernac"; "stm"; "toplevel"; "grammar"; "config";
-   "ltac"; "engine"]
+   "engine"]
 
 
 let usage () =
diff --git a/tools/gallina-db.el b/tools/gallina-db.el
index baabebb13a..9664f69f8b 100644
--- a/tools/gallina-db.el
+++ b/tools/gallina-db.el
@@ -163,7 +163,7 @@ for DB structure."
 
 (defun coq-sort-menu-entries (menu)
   (sort menu 
-	'(lambda (x y) (string< 
+	(lambda (x y) (string< 
 			(downcase (elt x 0)) 
 			(downcase (elt y 0))))))
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d9f8ed8815..cc1c44fe31 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -603,8 +603,6 @@ let init_toplevel arglist =
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   Lib.init();
-  (* Default Proofb Mode starts with an alternative default. *)
-  Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic";
   begin
     try
       let extras = parse_args arglist in
diff --git a/vernac/record.ml b/vernac/record.ml
index d5faafaf89..b494430c28 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -110,7 +110,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
       List.iter 
 	(function LocalRawDef (b, _) -> error default_binder_kind b
 	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls
-           | LocalPattern _ -> assert false) ps
+           | LocalPattern (loc,_,_) ->
+              Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
   in 
   let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
   let t', template = match t with 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0bf81e7e58..8b7d654572 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -165,7 +165,7 @@ let show_match id =
 let print_path_entry p =
   let dir = pr_dirpath (Loadpath.logical p) in
   let path = str (Loadpath.physical p) in
-  (dir ++ str " " ++ tbrk (0, 0) ++ path)
+  Pp.hov 2 (dir ++ spc () ++ path)
 
 let print_loadpath dir =
   let l = Loadpath.get_load_paths () in
@@ -175,9 +175,8 @@ let print_loadpath dir =
     let filter p = is_dirpath_prefix_of dir (Loadpath.logical p) in
     List.filter filter l
   in
-  Pp.t (str "Logical Path:                 " ++
-                tab () ++ str "Physical path:" ++ fnl () ++
-                prlist_with_sep fnl print_path_entry l)
+  str "Logical Path / Physical path:" ++ fnl () ++
+    prlist_with_sep fnl print_path_entry l
 
 let print_modules () =
   let opened = Library.opened_libraries ()