Merge branch 'v8.6'

40 files changed, 487 insertions, 259 deletions

diff --git a/CHANGES b/CHANGES
index b2a174c91..f780c4d12 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,4 +1,4 @@
-Changes beyong V8.6
+Changes beyond V8.6
 ===================
 
 Tactics
diff --git a/configure.ml b/configure.ml
index 7e125d87c..c3ba953de 100644
--- a/configure.ml
+++ b/configure.ml
@@ -430,7 +430,7 @@ let dll = if os_type_win32 then ".dll" else ".so"
 
 let vcs =
   let git_dir = try Sys.getenv "GIT_DIR" with Not_found -> ".git" in
-  if dir_exists git_dir then "git"
+  if Sys.file_exists git_dir then "git"
   else if Sys.file_exists ".svn/entries" then "svn"
   else if dir_exists "{arch}" then "gnuarch"
   else "none"
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index 588709873..aeaaea7e4 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -29,13 +29,28 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
   | Uniform x ->
     (** We dispatch the uniform result on each goal under focus, as we know
         that the [m] argument was actually dependent. *)
-    Proofview.Goal.goals >>= fun l ->
-    let ans = List.map (fun _ -> x) l in
+    Proofview.Goal.goals >>= fun goals ->
+    let ans = List.map (fun g -> (g,x)) goals in
     Proofview.tclUNIT ans
-  | Depends l -> Proofview.tclUNIT l
+  | Depends l ->
+    Proofview.Goal.goals >>= fun goals ->
+    Proofview.tclUNIT (List.combine goals l)
+  in
+  (* After the tactic has run, some goals which were previously
+     produced may have been solved by side effects. The values
+     attached to such goals must be discarded, otherwise the list of
+     result would not have the same length as the list of focused
+     goals, which is an invariant of the [Ftactic] module. It is the
+     reason why a goal is attached to each result above. *)
+  let filter (g,x) =
+    g >>= fun g ->
+    Proofview.Goal.unsolved g >>= function
+    | true -> Proofview.tclUNIT (Some x)
+    | false -> Proofview.tclUNIT None
   in
   Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
-  Proofview.tclUNIT (Depends (List.concat l))
+  Proofview.Monad.List.map_filter filter (List.concat l) >>= fun filtered ->
+  Proofview.tclUNIT (Depends filtered)
 
 let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
 let set_sigma r =
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 1ebc857d8..d7fb65126 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -685,6 +685,21 @@ let unshelve l p =
   let l = undefined p.solution l in
   { p with comb = p.comb@l }
 
+let mark_in_evm ~goal evd content =
+  let info = Evd.find evd content in
+  let info =
+    if goal then
+      { info with Evd.evar_source = match info.Evd.evar_source with
+            | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
+            | loc,_ -> loc,Evar_kinds.GoalEvar }
+    else info
+  in
+  let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
+  | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
+  | Some () -> info
+  in
+  Evd.add evd content info
+
 let with_shelf tac =
   let open Proof in
   Pv.get >>= fun pv ->
@@ -697,8 +712,11 @@ let with_shelf tac =
   let fgoals = Evd.future_goals solution in
   let pgoal = Evd.principal_future_goal solution in
   let sigma = Evd.restore_future_goals sigma fgoals pgoal in
-  Pv.set { npv with shelf; solution = sigma } >>
-  tclUNIT (CList.rev_append gls' gls, ans)
+  (* Ensure we mark and return only unsolved goals *)
+  let gls' = undefined sigma (CList.rev_append gls' gls) in
+  let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
+  let npv = { npv with shelf; solution = sigma } in
+  Pv.set npv >> tclUNIT (gls', ans)
 
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
     interval [[0,m-1]].*)
@@ -929,6 +947,8 @@ module Unsafe = struct
       { step with comb = step.comb @ gls }
     end
 
+  let tclSETENV = Env.set
+
   let tclGETGOALS = Comb.get
 
   let tclSETGOALS = Comb.set
@@ -943,20 +963,13 @@ module Unsafe = struct
     { p with solution = Evd.reset_future_goals p.solution }
 
   let mark_as_goal evd content =
-    let info = Evd.find evd content in
-    let info =
-      { info with Evd.evar_source = match info.Evd.evar_source with
-      | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
-      | loc,_ -> loc,Evar_kinds.GoalEvar }
-    in
-    let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
-    | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
-    | Some () -> info
-    in
-    Evd.add evd content info
+    mark_in_evm ~goal:true evd content
 
   let advance = advance
 
+  let mark_as_unresolvable p gl =
+    { p with solution = mark_in_evm ~goal:false p.solution gl }
+
   let typeclass_resolvable = typeclass_resolvable
 
 end
@@ -1129,6 +1142,10 @@ module Goal = struct
     in
     tclUNIT (CList.map_filter map step.comb)
 
+  let unsolved { self=self } =
+    tclEVARMAP >>= fun sigma ->
+    tclUNIT (not (Option.is_empty (advance sigma self)))
+
   (* compatibility *)
   let goal { self=self } = self
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index bc68f11ff..725445251 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -326,8 +326,9 @@ val unshelve : Goal.goal list -> proofview -> proofview
 (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
 val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool
 
-(** [with_shelf tac] executes [tac] and returns its result together with the set
-    of goals shelved by [tac]. The current shelf is unchanged. *)
+(** [with_shelf tac] executes [tac] and returns its result together with
+    the set of goals shelved by [tac]. The current shelf is unchanged
+    and the returned list contains only unsolved goals. *)
 val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
 
 (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
@@ -409,6 +410,9 @@ module Unsafe : sig
   (** Like {!tclEVARS} but also checks whether goals have been solved. *)
   val tclEVARSADVANCE : Evd.evar_map -> unit tactic
 
+  (** Set the global environment of the tactic *)
+  val tclSETENV : Environ.env -> unit tactic
+
   (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently
       being proved, appending them to the list of focused goals. If a
       goal is already solved, it is not added. *)
@@ -431,6 +435,9 @@ module Unsafe : sig
       and makes it unresolvable for type classes. *)
   val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
 
+  (** Make an evar unresolvable for type classes. *)
+  val mark_as_unresolvable : proofview -> Evar.t -> proofview
+
   (** [advance sigma g] returns [Some g'] if [g'] is undefined and is
       the current avatar of [g] (for instance [g] was changed by [clear]
       into [g']). It returns [None] if [g] has been (partially)
@@ -518,6 +525,10 @@ module Goal : sig
       FIXME: encapsulate the level in an existential type. *)
   val goals : ([ `LZ ], 'r) t tactic list tactic
 
+  (** [unsolved g] is [true] if [g] is still unsolved in the current
+      proof state. *)
+  val unsolved : ('a, 'r) t -> bool tactic
+
   (** Compatibility: avoid if possible *)
   val goal : ([ `NF ], 'r) t -> Evar.t
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f7fcbb4ee..4aff82403 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -481,7 +481,7 @@ let explicitize loc inctx impl (cf,f) args =
           (!print_implicits && !print_implicits_explicit_args) ||
           (is_needed_for_correct_partial_application tail imp) ||
 	  (!print_implicits_defensive &&
-	   (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) &&
+	   (not (is_inferable_implicit inctx n imp) || !Flags.beautify) &&
 	   is_significant_implicit (Lazy.force a))
 	in
         if visible then
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index eb564f3b3..b455381ea 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -22,8 +22,7 @@ open Constrexpr_ops
 let asymmetric_patterns = ref (false)
 let _ = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
-  Goptions.optname =
-    "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments";
+  Goptions.optname = "no parameters in constructors";
   Goptions.optkey = ["Asymmetric";"Patterns"];
   Goptions.optread = (fun () -> !asymmetric_patterns);
   Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
diff --git a/kernel/entries.mli b/kernel/entries.mli
index b736b2113..77081947e 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -98,7 +98,12 @@ type module_entry =
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
 
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type seff_env =
+  [ `Nothing
+  (* The proof term and its universes.
+     Same as the constant_body's but not in an ephemeron *)
+  | `Opaque of Constr.t * Univ.universe_context_set ]
 
 type side_eff =
   | SEsubproof of constant * Declarations.constant_body * seff_env
diff --git a/lib/monad.ml b/lib/monad.ml
index a1714a41b..2e55e9698 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -64,6 +64,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 
@@ -138,6 +141,14 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
       | a::b::l -> f a >> f b >> iter f l
 
 
+    let rec map_filter f = function
+      | [] -> return []
+      | a::l ->
+        f a >>= function
+        | None -> map_filter f l
+        | Some b ->
+          map_filter f l >>= fun filtered ->
+          return (b::filtered)
 
     let rec fold_left2 r f x l1 l2 =
       match l1,l2 with
diff --git a/lib/monad.mli b/lib/monad.mli
index c8655efa0..f7de71f53 100644
--- a/lib/monad.mli
+++ b/lib/monad.mli
@@ -66,6 +66,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 
diff --git a/lib/pp.ml b/lib/pp.ml
index 7f4bc149d..8291e7462 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -77,17 +77,6 @@ open Pp_control
    \end{description}
  *)
 
-let comments = ref []
-
-let rec split_com comacc acc pos = function
-    [] -> comments := List.rev acc; comacc
-  | ((b,e),c as com)::coms ->
-      (* Take all comments that terminates before pos, or begin exactly
-         at pos (used to print comments attached after an expression) *)
-      if e<=pos || pos=b then split_com (c::comacc) acc pos coms
-      else  split_com comacc (com::acc) pos coms
-
-
 type block_type =
   | Pp_hbox of int
   | Pp_vbox of int
@@ -111,7 +100,7 @@ type 'a ppcmd_token =
   | Ppcmd_open_box of block_type
   | Ppcmd_close_box
   | Ppcmd_close_tbox
-  | Ppcmd_comment of int
+  | Ppcmd_comment of string list
   | Ppcmd_open_tag of Tag.t
   | Ppcmd_close_tag
 
@@ -177,7 +166,7 @@ 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)
-let comment n = Glue.atom(Ppcmd_comment n)
+let comment l = Glue.atom(Ppcmd_comment l)
 
 (* derived commands *)
 let mt () = Glue.empty
@@ -321,8 +310,7 @@ let pp_dirs ?pp_tag ft =
         com_brk ft; Format.pp_force_newline ft ()
     | Ppcmd_print_if_broken   ->
         com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ()))
-    | Ppcmd_comment i         ->
-        let coms = split_com [] [] i !comments in
+    | Ppcmd_comment coms      ->
 (*        Format.pp_open_hvbox ft 0;*)
         List.iter (pr_com ft) coms(*;
         Format.pp_close_box ft ()*)
diff --git a/lib/pp.mli b/lib/pp.mli
index 3bd560812..f607e99db 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -23,8 +23,7 @@ val ws    : int -> std_ppcmds
 val mt    : unit -> std_ppcmds
 val ismt  : std_ppcmds -> bool
 
-val comment  : int -> std_ppcmds
-val comments : ((int * int) * string) list ref
+val comment  : string list -> std_ppcmds
 
 (** {6 Manipulation commands} *)
 
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index 3168898a3..b1c4f58eb 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -63,8 +63,17 @@ let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c
 let subst_strategy s str = str
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
-let pr_raw_strategy _ _ _ (s : raw_strategy) = Pp.str "<strategy>"
-let pr_glob_strategy _ _ _ (s : glob_strategy) = Pp.str "<strategy>"
+let pr_raw_strategy prc prlc _ (s : raw_strategy) =
+  let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in
+  Rewrite.pr_strategy prc prr s
+let pr_glob_strategy prc prlc _ (s : glob_strategy) =
+  let prr = Pptactic.pr_red_expr
+    (Ppconstr.pr_constr_expr,
+    Ppconstr.pr_lconstr_expr,
+    Pputils.pr_or_by_notation Libnames.pr_reference,
+    Ppconstr.pr_constr_expr)
+  in
+  Rewrite.pr_strategy prc prr s
 
 ARGUMENT EXTEND rewstrategy
     PRINTED BY pr_strategy
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index a332e2871..217f5f42e 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1703,6 +1703,40 @@ let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> (
   | StratEval r -> StratEval (g r)
   | StratFold c -> StratFold (f c)
 
+let pr_ustrategy = function
+| Subterms -> str "subterms"
+| Subterm -> str "subterm"
+| Innermost -> str "innermost"
+| Outermost -> str "outermost"
+| Bottomup -> str "bottomup"
+| Topdown -> str "topdown"
+| Progress -> str "progress"
+| Try -> str "try"
+| Any -> str "any"
+| Repeat -> str "repeat"
+
+let paren p = str "(" ++ p ++ str ")"
+
+let rec pr_strategy prc prr = function
+| StratId -> str "id"
+| StratFail -> str "fail"
+| StratRefl -> str "refl"
+| StratUnary (s, str) ->
+  pr_ustrategy s ++ spc () ++ paren (pr_strategy prc prr str)
+| StratBinary (Choice, str1, str2) ->
+  str "choice" ++ spc () ++ paren (pr_strategy prc prr str1) ++ spc () ++
+    paren (pr_strategy prc prr str2)
+| StratBinary (Compose, str1, str2) ->
+  pr_strategy prc prr str1 ++ str ";" ++ spc () ++ pr_strategy prc prr str2
+| StratConstr (c, true) -> prc c
+| StratConstr (c, false) -> str "<-" ++ spc () ++ prc c
+| StratTerms cl -> str "terms" ++ spc () ++ pr_sequence prc cl
+| StratHints (old, id) ->
+  let cmd = if old then "old_hints" else "hints" in
+  str cmd ++ spc () ++ str id
+| StratEval r -> str "eval" ++ spc () ++ prr r
+| StratFold c -> str "fold" ++ spc () ++ prc c
+
 let rec strategy_of_ast = function
   | StratId -> Strategies.id
   | StratFail -> Strategies.fail
diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli
index f448c8543..35c448351 100644
--- a/ltac/rewrite.mli
+++ b/ltac/rewrite.mli
@@ -62,6 +62,9 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat
 val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
   ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
 
+val pr_strategy : ('a -> Pp.std_ppcmds) -> ('b -> Pp.std_ppcmds) ->
+  ('a, 'b) strategy_ast -> Pp.std_ppcmds
+
 (** Entry point for user-level "rewrite_strat" *)
 val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic
 
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index f19759470..a7b413f57 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -340,34 +340,46 @@ let comm_loc bp = match !comment_begin with
 | None -> comment_begin := Some bp
 | _ -> ()
 
-let current = Buffer.create 8192
-let between_com = ref true
-
-type com_state = int option * string * bool
-let restore_com_state (o,s,b) =
+let comments = ref []
+let current_comment = Buffer.create 8192
+let between_commands = ref true
+
+let rec split_comments comacc acc pos = function
+    [] -> comments := List.rev acc; comacc
+  | ((b,e),c as com)::coms ->
+      (* Take all comments that terminates before pos, or begin exactly
+         at pos (used to print comments attached after an expression) *)
+      if e<=pos || pos=b then split_comments (c::comacc) acc pos coms
+      else split_comments comacc (com::acc) pos coms
+
+let extract_comments pos = split_comments [] [] pos !comments
+
+type comments_state = int option * string * bool * ((int * int) * string) list
+let restore_comments_state (o,s,b,c) =
   comment_begin := o;
-  Buffer.clear current; Buffer.add_string current s;
-  between_com := b
-let dflt_com = (None,"",true)
-let com_state () =
-  let s = (!comment_begin, Buffer.contents current, !between_com) in
-  restore_com_state dflt_com; s
+  Buffer.clear current_comment; Buffer.add_string current_comment s;
+  between_commands := b;
+  comments := c
+let default_comments_state = (None,"",true,[])
+let comments_state () =
+  let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) in
+  restore_comments_state default_comments_state; s
 
-let real_push_char c = Buffer.add_char current c
+let real_push_char c = Buffer.add_char current_comment c
 
 (* Add a char if it is between two commands, if it is a newline or
    if the last char is not a space itself. *)
 let push_char c =
   if
-    !between_com || List.mem c ['\n';'\r'] ||
+    !between_commands || List.mem c ['\n';'\r'] ||
     (List.mem c [' ';'\t']&&
-     (Int.equal (Buffer.length current) 0 ||
-      not (let s = Buffer.contents current in
+     (Int.equal (Buffer.length current_comment) 0 ||
+      not (let s = Buffer.contents current_comment in
            List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r'])))
   then
     real_push_char c
 
-let push_string s = Buffer.add_string current s
+let push_string s = Buffer.add_string current_comment s
 
 let null_comment s =
   let rec null i =
@@ -375,12 +387,12 @@ let null_comment s =
   null (String.length s - 1)
 
 let comment_stop ep =
-  let current_s = Buffer.contents current in
-  if !Flags.xml_export && Buffer.length current > 0 &&
-    (!between_com || not(null_comment current_s)) then
+  let current_s = Buffer.contents current_comment in
+  if !Flags.xml_export && Buffer.length current_comment > 0 &&
+    (!between_commands || not(null_comment current_s)) then
       Hook.get f_xml_output_comment current_s;
-  (if Flags.do_beautify() && Buffer.length current > 0 &&
-    (!between_com || not(null_comment current_s)) then
+  (if Flags.do_beautify() && Buffer.length current_comment > 0 &&
+    (!between_commands || not(null_comment current_s)) then
     let bp = match !comment_begin with
         Some bp -> bp
       | None ->
@@ -389,10 +401,10 @@ let comment_stop ep =
              ++ str current_s ++str"' ending at  "
              ++ int ep);
           ep-1 in
-    Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
-  Buffer.clear current;
+    comments := ((bp,ep),current_s) :: !comments);
+  Buffer.clear current_comment;
   comment_begin := None;
-  between_com := false
+  between_commands := false
 
 (* Does not unescape!!! *)
 let rec comm_string loc bp = parser
@@ -548,16 +560,16 @@ let rec next_token loc = parser bp
       | KEYWORD ("." | "...") ->
         if not (blank_or_eof s) then
 	  err (set_loc_pos loc bp (ep+1)) Undefined_token;
-	between_com := true;
+	between_commands := true;
       | _ -> ()
       in
       (t, set_loc_pos loc bp ep)
   | [< ' ('-'|'+'|'*' as c); s >] ->
-      let t,new_between_com =
-        if !between_com then process_sequence loc bp c s, true
+      let t,new_between_commands =
+        if !between_commands then process_sequence loc bp c s, true
         else process_chars loc bp c s,false
       in
-      comment_stop bp; between_com := new_between_com; t
+      comment_stop bp; between_commands := new_between_commands; t
   | [< ''?'; s >] ep ->
       let t = parse_after_qmark loc bp s in
       comment_stop bp; (t, set_loc_pos loc ep bp)
@@ -590,9 +602,9 @@ let rec next_token loc = parser bp
             (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
         | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) ->
             let t = process_chars loc bp (Stream.next s) s in
-            let new_between_com = match t with
-              (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in
-            comment_stop bp; between_com := new_between_com; t
+            let new_between_commands = match t with
+              (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in
+            comment_stop bp; between_commands := new_between_commands; t
         | EmptyStream ->
             comment_stop bp; (EOI, set_loc_pos loc bp (bp+1))
 
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 3b4891d9a..3ad49eb74 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -34,12 +34,12 @@ type frozen_t
 val freeze : unit -> frozen_t
 val unfreeze : frozen_t -> unit
 
-type com_state
-val com_state: unit -> com_state
-val restore_com_state: com_state -> unit
-
 val xml_output_comment : (string -> unit) Hook.t
 
+(* Retrieve the comments lexed at a given location of the stream
+   currently being processeed *)
+val extract_comments : int -> string list
+
 val terminal : string -> Tok.t
 
 (** The lexer of Coq: *)
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 389c34fa5..58b74da26 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -138,12 +138,21 @@ module type LexerSig = sig
     exception E of t
     val to_string : t -> string
   end
+  type comments_state
+  val default_comments_state : comments_state
+  val comments_state : unit -> comments_state
+  val restore_comments_state : comments_state -> unit
 end
 
 ELSE
 
-module type LexerSig =
-  Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+module type LexerSig = sig
+  include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+  type comments_state
+  val default_comments_state : comments_state
+  val comments_state : unit -> comments_state
+  val restore_comments_state : comments_state -> unit
+end
 
 END
 
@@ -162,10 +171,13 @@ module type GrammarSig = sig
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+  type coq_parsable
+  val parsable : char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
 end
@@ -181,14 +193,33 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+  type coq_parsable = parsable * L.comments_state ref
+  let parsable c =
+    let state = ref L.default_comments_state in (parsable c, state)
   let action = Gramext.action
   let entry_create = Entry.create
-  let entry_parse e p =
-    try Entry.parse e p
+  let entry_parse e (p,state) =
+    L.restore_comments_state !state;
+    try
+      let c = Entry.parse e p in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      c
     with Exc_located (loc,e) ->
+      L.restore_comments_state L.default_comments_state;
       let loc' = Loc.get_loc (Exninfo.info e) in
       let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
       Loc.raise ~loc e
+  let with_parsable (p,state) f x =
+    L.restore_comments_state !state;
+    try
+      let a = f x in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      a
+    with e ->
+      L.restore_comments_state L.default_comments_state;
+      raise e
 
   let entry_print ft x = Entry.print ft x
   let srules' = Gramext.srules
@@ -202,12 +233,13 @@ module type GrammarSig = sig
     with module Loc = CompatLoc and type Token.t = Tok.t
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type parsable
-  val parsable : char Stream.t -> parsable
+  type coq_parsable
+  val parsable : char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
   val srules' : production_rule list -> symbol
 end
 
@@ -217,13 +249,31 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   include Camlp4.Struct.Grammar.Static.Make (L)
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type parsable = char Stream.t
-  let parsable s = s
+  type comments_state = int option * string * bool * ((int * int) * string) list
+  type coq_parsable = char Stream.t * L.comments_state ref
+  let parsable s = let state = ref L.default_comments_state in (s, state)
   let action = Action.mk
   let entry_create = Entry.mk
-  let entry_parse e s =
-    try parse e (*FIXME*)CompatLoc.ghost s
-    with Exc_located (loc,e) -> raise_coq_loc loc e
+  let entry_parse e (s,state) =
+    L.restore_comments_state !state;
+    try
+      let c = parse e (*FIXME*)CompatLoc.ghost s in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      c
+    with Exc_located (loc,e) ->
+      L.restore_comments_state L.default_comments_state;
+      raise_coq_loc loc e
+  let with_parsable (p,state) f x =
+    L.restore_comments_state !state;
+    try
+      let a = f x in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      a
+    with e ->
+      L.restore_comments_state L.default_comments_state;
+      raise e
   let entry_print ft x = Entry.print ft x
   let srules' = srules (entry_create "dummy")
 end
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0d30b3e4c..02fb515b0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1870,22 +1870,16 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
-let add_subst c len (rel_subst,var_subst) =
-  match kind_of_term c with
-  | Rel n -> (n,len) :: rel_subst, var_subst
-  | Var id -> rel_subst, (id,len) :: var_subst
-  | _ -> assert false
-
 let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
-  let (rel_subst,var_subst), len =
+  let subst, len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match kind_of_term tm with
-	  | Rel _ | Var _ when dependent tm c
+	  | Rel n when dependent tm c
 		&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
-	      (add_subst tm len subst, len - signlen)
-	  | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
+	      ((n, len) :: subst, len - signlen)
+	  | Rel n when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
 		  NotInd _ -> (subst, len - signlen)
@@ -1894,36 +1888,28 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match kind_of_term arg with
-			  | Rel _ | Var _ when dependent arg c ->
-			      (add_subst arg len subst, pred len)
+			  | Rel n when dependent arg c ->
+			      ((n, len) :: subst, pred len)
 			  | _ -> (subst, pred len))
 			(subst, len) realargs
 		    in
 		    let subst =
-		      if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs
-		      then add_subst tm len subst else subst
+		      if dependent tm c && List.for_all isRel realargs
+		      then (n, len) :: subst else subst
 		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
-      (List.rev tomatchs) arsign (([],[]), nar)
+      (List.rev tomatchs) arsign ([], nar)
   in
   let rec predicate lift c =
     match kind_of_term c with
       | Rel n when n > lift ->
 	  (try
 	      (* Make the predicate dependent on the matched variable *)
-	      let idx = Int.List.assoc (n - lift) rel_subst in
+	      let idx = Int.List.assoc (n - lift) subst in
 		mkRel (idx + lift)
 	    with Not_found ->
-	      (* A variable that is not matched, lift over the arsign *)
+	      (* A variable that is not matched, lift over the arsign. *)
 	      mkRel (n + nar))
-      | Var id ->
-	  (try
-	      (* Make the predicate dependent on the matched variable *)
-	      let idx = Id.List.assoc id var_subst in
-		mkRel (idx + lift)
-	    with Not_found ->
-	      (* A variable that is not matched *)
-	      c)
       | _ ->
 	  map_constr_with_binders succ predicate lift c
   in
@@ -1944,39 +1930,38 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
-    match pred with
+    match pred, tycon with
     (* No return clause *)
-    | None ->
-        let sigma,t =
-          match tycon with
-          | Some t -> sigma, t
-          | None ->
-             (* No type constraint: we first create a generic evar type constraint *)
-             let src = (loc, Evar_kinds.CasesType false) in
-             let sigma = Sigma.Unsafe.of_evar_map sigma in
-             let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
-             let sigma = Sigma.to_evar_map sigma in
-             sigma, t in
-        (* First strategy: we build an "inversion" predicate, also replacing the *)
-        (* dependencies with existential variables *)
+    | None, Some t when not (noccur_with_meta 0 max_int t) ->
+	(* If the tycon is not closed w.r.t real variables, we try *)
+        (* two different strategies *)
+	(* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
 	(* Optional second strategy: we abstract the tycon wrt to the dependencies *)
         let p2 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
-        (* Third strategy: we take the type constraint as it is; of course we could *)
-        (* need something inbetween, abstracting some but not all of the dependencies *)
-        (* the "inversion" strategy deals with that but unification may not be *)
-        (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *)
-        (* work (yet) when a constructor has a type not precise enough for the inversion *)
-        (* see log message for details *)
-        let pred3 = lift (List.length (List.flatten arsign)) t in
 	(match p2 with
-	 | Some (sigma2,pred2) when not (Constr.equal pred2 pred3) ->
-             [sigma1, pred1; sigma2, pred2; sigma, pred3]
-	 | _ ->
-             [sigma1, pred1; sigma, pred3])
+	 | Some (sigma2,pred2) -> [sigma1, pred1; sigma2, pred2]
+	 | None -> [sigma1, pred1])
+    | None, _ ->
+	(* No dependent type constraint, or no constraints at all: *)
+	(* we use two strategies *)
+        let sigma,t = match tycon with
+	| Some t -> sigma,t
+	| None -> 
+          let sigma = Sigma.Unsafe.of_evar_map sigma in
+          let Sigma ((t, _), sigma, _) =
+	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
+          let sigma = Sigma.to_evar_map sigma in
+	    sigma, t
+	in
+        (* First strategy: we build an "inversion" predicate *)
+	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+	(* Second strategy: we use the evar or tycon as a non dependent pred *)
+        let pred2 = lift (List.length (List.flatten arsign)) t in
+	[sigma1, pred1; sigma, pred2]
     (* Some type annotation *)
-    | Some rtntyp ->
+    | Some rtntyp, _ ->
       (* We extract the signature of the arity *)
       let envar = List.fold_right push_rel_context arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index fa5a70899..c94650f1e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -129,7 +129,7 @@ end) = struct
     str "`" ++ str hd ++ c ++ str tl
 
   let pr_com_at n =
-    if Flags.do_beautify() && not (Int.equal n 0) then comment n
+    if Flags.do_beautify() && not (Int.equal n 0) then comment (CLexer.extract_comments n)
     else mt()
 
   let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 33382fe83..491688913 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -17,7 +17,11 @@ open Genredexpr
 let pr_located pr (loc, x) =
   if Flags.do_beautify () && loc <> Loc.ghost then
     let (b, e) = Loc.unloc loc in
-    Pp.comment b ++ pr x ++ Pp.comment e
+    (* Side-effect: order matters *)
+    let before = Pp.comment (CLexer.extract_comments b) in
+    let x = pr x in
+    let after = Pp.comment (CLexer.extract_comments e) in
+    before ++ x ++ after
   else pr x
 
 let pr_or_var pr = function
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7c00106e2..5d7249aff 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -261,7 +261,7 @@ module Make
 
   let pr_decl_notation prc ((loc,ntn),c,scopt) =
     fnl () ++ keyword "where " ++ qs ntn ++ str " := "
-    ++ Flags.without_option Flags.beautify_file prc c ++
+    ++ Flags.without_option Flags.beautify prc c ++
       pr_opt (fun sc -> str ": " ++ str sc) scopt
 
   let pr_binders_arg =
@@ -381,7 +381,7 @@ module Make
     | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
 
   let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) =
-    let pr_pure_lconstr c = Flags.without_option Flags.beautify_file pr_lconstr c in
+    let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
     let annot = pr_guard_annot pr_lconstr_expr bl ro in
     pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
     ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
@@ -676,7 +676,7 @@ module Make
       | VernacNotation (_,c,((_,s),l),opt) ->
         return (
           hov 2 (keyword "Notation" ++ spc() ++ qs s ++
-                   str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++
+                   str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
                    (match opt with
                      | None -> mt()
                      | Some sc -> str" :" ++ spc() ++ str sc))
@@ -758,7 +758,7 @@ module Make
         let pr_constructor (coe,(id,c)) =
           hov 2 (pr_lident id ++ str" " ++
                    (if coe then str":>" else str":") ++
-                   Flags.without_option Flags.beautify_file pr_spc_lconstr c)
+                   Flags.without_option Flags.beautify pr_spc_lconstr c)
         in
         let pr_constructor_list b l = match l with
           | Constructors [] -> mt()
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 16278b456..0a3b08c04 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -351,7 +351,14 @@ let run_tactic env tac pr =
     Proofview.apply env tac sp
   in
   let sigma = Proofview.return proofview in
-  let shelf = (undef sigma pr.shelf)@retrieved@(undef sigma to_shelve) in
+  let to_shelve = undef sigma to_shelve in
+  let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in
+  let proofview =
+    List.fold_left
+      Proofview.Unsafe.mark_as_unresolvable
+      proofview
+      to_shelve
+  in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
   { pr with proofview ; shelf ; given_up },(status,info_trace)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index ecc461f78..d4920e505 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -53,6 +53,23 @@ let typecheck_proof c concl env sigma =
 let (pr_constrv,pr_constr) =
   Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
 
+(* Get the side-effect's constant declarations to update the monad's
+  * environmnent *)
+let add_if_undefined kn cb env =
+  try ignore(Environ.lookup_constant kn env); env
+  with Not_found -> Environ.add_constant kn cb env
+
+(* Add the side effects to the monad's environment, if not already done. *)
+let add_side_effect env = function
+  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
+    add_if_undefined kn cb env
+  | { Entries.eff = Entries.SEscheme (l,_) } ->
+    List.fold_left (fun env (_,kn,cb,eff_env) ->
+        add_if_undefined kn cb env) env l
+
+let add_side_effects env effects =
+  List.fold_left (fun env eff -> add_side_effect env eff) env effects
+
 let make_refine_enter ?(unsafe = true) f =
   { enter = fun gl ->
   let gl = Proofview.Goal.assume gl in
@@ -68,6 +85,10 @@ let make_refine_enter ?(unsafe = true) f =
   let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
   let evs = Evd.future_goals sigma in
   let evkmain = Evd.principal_future_goal sigma in
+  (** Redo the effects in sigma in the monad's env *)
+  let privates_csts = Evd.eval_side_effects sigma in
+  let sideff = Safe_typing.side_effects_of_private_constants privates_csts in
+  let env = add_side_effects env sideff in
   (** Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
@@ -96,6 +117,7 @@ let make_refine_enter ?(unsafe = true) f =
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb 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 v) >>= fun v ->
+  Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
   Proofview.tclUNIT v
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1cb71da69..c66fad651 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -374,7 +374,7 @@ and my_find_search_delta db_list local_db hdc concl =
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
 
-and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) =
+and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
     | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
@@ -393,7 +393,14 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
     | Extern tacast -> 
       conclPattern concl p tacast
   in
-  tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic)
+  let pr_hint () =
+    let origin = match dbname with
+    | None -> mt ()
+    | Some n -> str " (in " ++ str n ++ str ")"
+    in
+    pr_hint t ++ origin
+  in
+  tclLOG dbg pr_hint (run_hint t tactic)
 
 and trivial_resolve dbg mod_delta db_list local_db cl =
   try
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 1689bd73c..3ee96353f 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -16,8 +16,6 @@ open Decl_kinds
 open Hints
 open Tactypes
 
-val priority : ('a * full_hint) list -> ('a * full_hint) list
-
 val default_search_depth : int ref
 
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ac945de3c..7dc40079e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -111,6 +111,7 @@ type 'a with_metadata = {
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
   name  : hints_path_atom; (* A potential name to refer to the hint *) 
+  db : string option; (** The database from which the hint comes *)
   code : 'a;     (* the tactic to apply when the concl matches pat *)
 }
 
@@ -413,7 +414,35 @@ let rec subst_hints_path subst hp =
       if p' == p && q' == q then hp else PathOr (p', q')
   | _ -> hp
 
-module Hint_db = struct
+type hint_db_name = string
+
+module Hint_db :
+sig
+type t
+val empty : ?name:hint_db_name -> transparent_state -> bool -> t
+val find : global_reference -> t -> search_entry
+val map_none : t -> full_hint list
+val map_all : global_reference -> t -> full_hint list
+val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list
+val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list
+val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
+val add_one : env -> evar_map -> hint_entry -> t -> t
+val add_list : env -> evar_map -> hint_entry list -> t -> t
+val remove_one : global_reference -> t -> t
+val remove_list : global_reference list -> t -> t
+val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
+val use_dn : t -> bool
+val transparent_state : t -> transparent_state
+val set_transparent_state : t -> transparent_state -> t
+val add_cut : hints_path -> t -> t
+val add_mode : global_reference -> hint_mode array -> t -> t
+val cut : t -> hints_path
+val unfolds : t -> Id.Set.t * Cset.t
+val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
+  t -> 'a -> 'a
+
+end =
+struct
 
   type t = {
     hintdb_state : Names.transparent_state;
@@ -424,20 +453,22 @@ module Hint_db = struct
     hintdb_map : search_entry Constr_map.t;
     (* A list of unindexed entries starting with an unfoldable constant
        or with no associated pattern. *)
-    hintdb_nopat : (global_reference option * stored_data) list
+    hintdb_nopat : (global_reference option * stored_data) list;
+    hintdb_name : string option;
   }
 
   let next_hint_id db =
     let h = db.hintdb_max_id in
     { db with hintdb_max_id = succ db.hintdb_max_id }, h
 
-  let empty st use_dn = { hintdb_state = st;
+  let empty ?name st use_dn = { hintdb_state = st;
 			  hintdb_cut = PathEmpty;
 			  hintdb_unfolds = (Id.Set.empty, Cset.empty);
 			  hintdb_max_id = 0;
 			  use_dn = use_dn;
 			  hintdb_map = Constr_map.empty;
-			  hintdb_nopat = [] }
+			  hintdb_nopat = [];
+			  hintdb_name = name; }
 
   let find key db =
     try Constr_map.find key db.hintdb_map
@@ -505,7 +536,7 @@ module Hint_db = struct
     | _ -> false
 
   let addkv gr id v db =
-    let idv = id, v in
+    let idv = id, { v with db = db.hintdb_name } in
     let k = match gr with
       | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr &&
 	  is_unfold v.code.obj then None else Some gr
@@ -609,8 +640,6 @@ type hint_db = Hint_db.t
 
 type hint_db_table = hint_db Hintdbmap.t ref
 
-type hint_db_name = string
-
 (** Initially created hint databases, for typeclasses and rewrite *)
 
 let typeclasses_db = "typeclass_instances"
@@ -687,6 +716,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    poly = poly;
 	    pat = Some pat;
 	    name = name;
+            db = None;
 	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
@@ -707,6 +737,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	    poly = poly;
             pat = Some pat;
 	    name = name;
+            db = None;
             code = with_uid (Res_pf(c,cty,ctx)); })
 	else begin
 	  if not eapply then failwith "make_apply_entry";
@@ -718,6 +749,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	     poly = poly;
              pat = Some pat;
 	     name = name;
+             db = None;
              code = with_uid (ERes_pf(c,cty,ctx)); })
         end
     | _ -> failwith "make_apply_entry"
@@ -802,6 +834,7 @@ let make_unfold eref =
      poly = false;
      pat = None;
      name = PathHints [g];
+     db = None;
      code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
@@ -811,6 +844,7 @@ let make_extern pri pat tacast =
      poly = false;
      pat = pat;
      name = PathAny;
+     db = None;
      code = with_uid (Extern tacast) })  
 
 let make_mode ref m = 
@@ -834,6 +868,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
 	      poly = poly;
               pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
 	      name = name;
+              db = None;
               code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
 
@@ -847,7 +882,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
 
 let get_db dbname =
   try searchtable_map dbname
-  with Not_found -> Hint_db.empty empty_transparent_state false
+  with Not_found -> Hint_db.empty ~name:dbname empty_transparent_state false
 
 let add_hint dbname hintlist =
   let check (_, h) =
@@ -907,7 +942,7 @@ type hint_obj = {
 let load_autohint _ (kn, h) =
   let name = h.hint_name in
   match h.hint_action with
-  | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
+  | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b)
   | AddTransparency (grs, b) -> add_transparency name grs b
   | AddHints hints -> add_hint name hints
   | RemoveHints grs -> remove_hint name grs
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 9a3817203..48351a317 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -46,11 +46,14 @@ type hints_path_atom =
   (* For forward hints, their names is the list of projections *)
   | PathAny
 
+type hint_db_name = string
+
 type 'a with_metadata = private {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
   name  : hints_path_atom; (** A potential name to refer to the hint *) 
+  db    : hint_db_name option;
   code  : 'a; (** the tactic to apply when the concl matches pat *)
 }
 
@@ -80,7 +83,7 @@ val pp_hint_mode : hint_mode -> Pp.std_ppcmds
 module Hint_db :
   sig
     type t
-    val empty : transparent_state -> bool -> t
+    val empty : ?name:hint_db_name -> transparent_state -> bool -> t
     val find : global_reference -> t -> search_entry
     val map_none : t -> full_hint list
 
@@ -116,8 +119,6 @@ module Hint_db :
     val unfolds : t -> Id.Set.t * Cset.t
   end
 
-type hint_db_name = string
-
 type hint_db = Hint_db.t
 
 type hnf = bool
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
new file mode 100644
index 000000000..b97a8ce64
--- /dev/null
+++ b/test-suite/bugs/closed/4416.v
@@ -0,0 +1,3 @@
+Goal exists x, x.
+unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
+(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
new file mode 100644
index 000000000..e884355fd
--- /dev/null
+++ b/test-suite/bugs/closed/4863.v
@@ -0,0 +1,32 @@
+Require Import Classes.DecidableClass.
+
+Inductive Foo : Set :=
+| foo1 | foo2.
+
+Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
+Proof.
+  intros P H.
+  refine (Build_Decidable _ (if H then true else false) _).
+  intuition congruence.
+Qed.
+
+Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances.
+
+Goal forall (a b : Foo), {a=b}+{a<>b}.
+intros.
+abstract (abstract (decide equality)). (*abstract works here*)
+Qed.
+
+Check ltac:(abstract (exact I)) : True.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split. typeclasses eauto. typeclasses eauto. Qed.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split.
+refine _.
+refine _.
+Defined.
+(*fails*)
diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v
new file mode 100644
index 000000000..bcde510ee
--- /dev/null
+++ b/test-suite/bugs/closed/5123.v
@@ -0,0 +1,33 @@
+(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *)
+
+(*Pose an open constr to prevent immediate typeclass resolution in holes:*)
+Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H.
+
+Inductive vect A : nat -> Type :=
+| vnil : vect A 0
+| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n).
+
+Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}.
+
+Require Bool.
+
+Instance Bool_eqdec : Eqdec bool := Bool.bool_dec.
+
+Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}.
+
+Typeclasses eauto := debug.
+
+Goal True.
+  unshelve opose (@vect_sigT_eqdec _ _ _ _) as H.
+  all:cycle 2.
+  eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*)
+  Focus 5.
+Abort.
+
+Goal True.
+  opose (@vect_sigT_eqdec _ _ _ _) as H.
+  Unshelve.
+  all:cycle 3.
+  eapply existT. (*This does no typeclass resultion, which is correct.*)
+  Focus 5.
+Abort.
\ No newline at end of file
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 356a67efe..8f95484cf 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,41 +87,3 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
-
-(* Check use of the no-dependency strategy when a type constraint is
-   given (and when the "inversion-and-dependencies-as-evars" strategy
-   is not strong enough because of a constructor with a type whose
-   pattern structure is not refined enough for it to be captured by
-   the inversion predicate) *)
-
-Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
-
-Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
-        match y with
-        | F  => f y H1
-        | G _ => f y H2
-        end : Q y z.
-
-(* Check use of the maximal-dependency-in-variable strategy even when
-   no explicit type constraint is given (and when the
-   "inversion-and-dependencies-as-evars" strategy is not strong enough
-   because of a constructor with a type whose pattern structure is not
-   refined enough for it to be captured by the inversion predicate) *)
-
-Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
-        match y with
-        | F  => f y true H1
-        | G b => f y b H2
-        end.
-
-(* Check use of the maximal-dependency-in-variable strategy for "Var"
-   variables *)
-
-Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
-intros z P Q y H1 H2 f.
-Show.
-refine (match y with
-        | F  => f y true H1
-        | G b => f y b H2
-        end).
-Qed.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index dfa438d90..3eaa04144 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -5,7 +5,7 @@ Record Equ (A : Type) (R : A -> A -> Prop).
 Definition equiv {A} R (e : Equ A R) := R.
 Record Refl (A : Type) (R : A -> A -> Prop).
 Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e).
-Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [|shelve|] : foo.
+Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo.
 
 Variable R : nat -> nat -> Prop.
 Lemma bas : Equ nat R.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index ad067eb3d..1db6a71e8 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -357,17 +357,8 @@ the above form:
         | _ => idtac
       end.
 
-    (** [if t then t1 else t2] executes [t] and, if it does not
-        fail, then [t1] will be applied to all subgoals
-        produced.  If [t] fails, then [t2] is executed. *)
-    Tactic Notation
-      "if" tactic(t)
-      "then" tactic(t1)
-      "else" tactic(t2) :=
-      first [ t; first [ t1 | fail 2 ] | t2 ].
-
     Ltac abstract_term t :=
-      if (is_var t) then fail "no need to abstract a variable"
+      tryif (is_var t) then fail "no need to abstract a variable"
       else (let x := fresh "x" in set (x := t) in *; try clearbody x).
 
     Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
       repeat (
         match goal with
         | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
-          if (change T with E.t in H) then fail
-          else if (change T with t in H) then fail
+          tryif (change T with E.t in H) then fail
+          else tryif (change T with t in H) then fail
           else clear H
         | H : ?P |- _ =>
-          if prop (FSet_Prop P) holds by
+          tryif prop (FSet_Prop P) holds by
             (auto 100 with FSet_Prop)
           then fail
           else clear H
@@ -747,7 +738,7 @@ the above form:
     | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
       contradict H; fsetdec_body
     | H: ?P -> False |- ?Q -> False =>
-      if prop (FSet_elt_Prop P) holds by
+      tryif prop (FSet_elt_Prop P) holds by
         (auto 100 with FSet_Prop)
       then (contradict H; fsetdec_body)
       else fsetdec_body
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index f2555791b..9c622fd78 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -357,17 +357,8 @@ the above form:
         | _ => idtac
       end.
 
-    (** [if t then t1 else t2] executes [t] and, if it does not
-        fail, then [t1] will be applied to all subgoals
-        produced.  If [t] fails, then [t2] is executed. *)
-    Tactic Notation
-      "if" tactic(t)
-      "then" tactic(t1)
-      "else" tactic(t2) :=
-      first [ t; first [ t1 | fail 2 ] | t2 ].
-
     Ltac abstract_term t :=
-      if (is_var t) then fail "no need to abstract a variable"
+      tryif (is_var t) then fail "no need to abstract a variable"
       else (let x := fresh "x" in set (x := t) in *; try clearbody x).
 
     Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
       repeat (
         match goal with
         | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
-          if (change T with E.t in H) then fail
-          else if (change T with t in H) then fail
+          tryif (change T with E.t in H) then fail
+          else tryif (change T with t in H) then fail
           else clear H
         | H : ?P |- _ =>
-          if prop (MSet_Prop P) holds by
+          tryif prop (MSet_Prop P) holds by
             (auto 100 with MSet_Prop)
           then fail
           else clear H
@@ -747,7 +738,7 @@ the above form:
     | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
       contradict H; fsetdec_body
     | H: ?P -> False |- ?Q -> False =>
-      if prop (MSet_elt_Prop P) holds by
+      tryif prop (MSet_elt_Prop P) holds by
         (auto 100 with MSet_Prop)
       then (contradict H; fsetdec_body)
       else fsetdec_body
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 6f8fc1b32..0115d8a54 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -434,14 +434,14 @@ Lemma eqb_compare x y :
  (x =? y) = match compare x y with Eq => true | _ => false end.
 Proof.
 apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff.
-destruct compare; now split.
+now destruct compare.
 Qed.
 
 Lemma ltb_compare x y :
  (x <? y) = match compare x y with Lt => true | _ => false end.
 Proof.
 apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff.
-destruct compare; now split.
+now destruct compare.
 Qed.
 
 Lemma leb_compare x y :
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 69d68bd35..71e1f9593 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -23,7 +23,7 @@ type input_buffer = {
   mutable str : string; (* buffer of already read characters *)
   mutable len : int;    (* number of chars in the buffer *)
   mutable bols : int list; (* offsets in str of beginning of lines *)
-  mutable tokens : Gram.parsable; (* stream of tokens *)
+  mutable tokens : Gram.coq_parsable; (* stream of tokens *)
   mutable start : int } (* stream count of the first char of the buffer *)
 
 (* Double the size of the buffer. *)
@@ -274,9 +274,9 @@ let rec discard_to_dot () =
     | End_of_input -> raise End_of_input
     | e when CErrors.noncritical e -> ()
 
-let read_sentence () =
+let read_sentence input =
   try
-    let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in
+    let (loc, _ as r) = Vernac.parse_sentence input in
     CWarnings.set_current_loc loc; r
   with reraise ->
     let reraise = CErrors.push reraise in
@@ -298,7 +298,8 @@ let do_vernac () =
   if !print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
-    Vernac.eval_expr (read_sentence ())
+    let input = (top_buffer.tokens, None) in
+    Vernac.eval_expr input (read_sentence input)
   with
     | End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 00554da30..e40353e0f 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -18,7 +18,7 @@ type input_buffer = {
   mutable str : string; (** buffer of already read characters *)
   mutable len : int;    (** number of chars in the buffer *)
   mutable bols : int list; (** offsets in str of begining of lines *)
-  mutable tokens : Pcoq.Gram.parsable; (** stream of tokens *)
+  mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *)
   mutable start : int } (** stream count of the first char of the buffer *)
 
 (** The input buffer of stdin. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 07bccb532..a37859c9c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,34 +124,37 @@ let set_formatter_translator() =
   Format.set_formatter_output_functions out (fun () -> flush ch);
   Format.set_max_boxes max_int
 
-let pr_new_syntax loc ocom =
+let pr_new_syntax_in_context loc ocom =
   let loc = Loc.unloc loc in
   if !beautify_file then set_formatter_translator();
   let fs = States.freeze ~marshallable:`No in
+  (* Side-effect: order matters *)
+  let before = comment (CLexer.extract_comments (fst loc)) in
   let com = match ocom with
     | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
+  let after = comment (CLexer.extract_comments (snd loc)) in
   if !beautify_file then
-    Feedback.msg_notice (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
+    Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
   else
     Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
+let pr_new_syntax (po,_) loc ocom =
+  (* Reinstall the context of parsing which includes the bindings of comments to locations *)
+  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom
+
 let save_translator_coqdoc () =
   (* translator state *)
   let ch = !chan_beautify in
-  let cl = !Pp.comments in
-  let cs = CLexer.com_state() in
   (* end translator state *)
   let coqdocstate = CLexer.location_table () in
-  ch,cl,cs,coqdocstate
+  ch,coqdocstate
 
-let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
+let restore_translator_coqdoc (ch,coqdocstate) =
   if !Flags.beautify_file then close_out !chan_beautify;
   chan_beautify := ch;
-  Pp.comments := cl;
-  CLexer.restore_com_state cs;
   CLexer.restore_location_table coqdocstate
 
 (* For coqtop -time, we display the position in the file,
@@ -182,7 +185,7 @@ let print_cmd_header loc com =
   Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
   Format.pp_print_flush !Pp_control.std_ft ()
 
-let rec vernac_com checknav (loc,com) =
+let rec vernac_com input checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
@@ -194,7 +197,6 @@ let rec vernac_com checknav (loc,com) =
 	if !Flags.beautify_file then
 	  begin
 	    chan_beautify := open_out (f^beautify_suffix);
-	    Pp.comments := []
           end;
 	begin
 	  try
@@ -214,13 +216,11 @@ let rec vernac_com checknav (loc,com) =
   in
     try
       checknav loc com;
-      if do_beautify () then pr_new_syntax loc (Some com);
+      if do_beautify () then pr_new_syntax input loc (Some com);
       (* XXX: This is not 100% correct if called from an IDE context *)
       if !Flags.time then print_cmd_header loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
-      let a = CLexer.com_state () in
-      interp com;
-      CLexer.restore_com_state a
+      interp com
     with reraise ->
       let (reraise, info) = CErrors.push reraise in
       Format.set_formatter_out_channel stdout;
@@ -240,7 +240,7 @@ and read_vernac_file verbosely s =
     while true do
       let loc_ast = parse_sentence input in
       CWarnings.set_current_loc (fst loc_ast);
-      vernac_com checknav loc_ast;
+      vernac_com input checknav loc_ast;
     done
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
@@ -249,7 +249,7 @@ and read_vernac_file verbosely s =
     match e with
       | End_of_input ->
           if do_beautify () then
-            pr_new_syntax (Loc.make_loc (max_int,max_int)) None
+            pr_new_syntax input (Loc.make_loc (max_int,max_int)) None
       | reraise ->
 	 iraise (disable_drop e, info)
 
@@ -264,7 +264,7 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com checknav loc_ast
+let eval_expr input loc_ast = vernac_com input checknav loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 7bfddd947..2fd86ddc2 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -11,7 +11,7 @@
 (** Read a vernac command on the specified input (parse only).
    Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
 
-val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
+val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option ->
  Loc.t * Vernacexpr.vernac_expr
 
 (** Reads and executes vernac commands from a stream.
@@ -21,7 +21,7 @@ exception End_of_input
 
 val just_parsing : bool ref
 
-val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit
+val eval_expr : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -> unit
 
 (** Set XML hooks *)
 val xml_start_library : (unit -> unit) Hook.t