Merge branch 'v8.5'

42 files changed, 130 insertions, 86 deletions

diff --git a/CHANGES b/CHANGES
index a77889fc4..9da642b0f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,10 @@ Vernacular commands
   introducing it.
 - New command "Show id" to show goal named id.
 
+Specification language
+
+- Syntax "$(tactic)$" changed to "ltac: tactic".
+
 Tactics
 
 - New flag "Regular Subst Tactic" which fixes "subst" in situations where
@@ -104,6 +108,10 @@ Logic
 - The VM now supports inductive types with up to 8388851 non-constant
   constructors and up to 8388607 constant ones.
 
+Specification language
+
+- Syntax "$(tactic)$" changed to "ltac: tactic".
+
 Tactics
 
 - A script using the admit tactic can no longer be concluded by either
diff --git a/Makefile.build b/Makefile.build
index 957592640..37c8e4c67 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -494,7 +494,7 @@ check: validate test-suite
 test-suite: world $(ALLSTDLIB).v
 	$(MAKE) $(MAKE_TSOPTS) clean
 	$(MAKE) $(MAKE_TSOPTS) all
-	$(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi
+	$(MAKE) $(MAKE_TSOPTS) report
 
 ##################################################################
 # partial targets: 1) core ML parts
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 1b1d3500a..492e75a7b 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -223,6 +223,7 @@ version & date & comments \\
 Coq ``V6'' archive & 20 March 1996 & new cvs repository on pauillac.inria.fr with code ported \\
  & & to Caml Special Light (to later become Objective Caml)\\
  & & has implicit arguments and coercions\\
+ & & has coinductive types\\
 
 Coq V6.1beta& released 18 November 1996 & \feature{coercions} [23-5-1996], \feature{user-level implicit arguments} [23-5-1996]\\
  & & \feature{omega} [10-9-1996] \\
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b77118e1f..80e12898f 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1998,7 +1998,7 @@ variables, use
 \end{quote}
 
 \subsection{Solving existential variables using tactics}
-\ttindex{\textdollar( \ldots )\textdollar}
+\ttindex{ltac:( \ldots )}
 
 \def\expr{\textrm{\textsl{tacexpr}}}
 
@@ -2012,7 +2012,7 @@ binding as well as those introduced by tactic binding. The expression {\expr}
 can be any tactic expression as described at section~\ref{TacticLanguage}.
 
 \begin{coq_example*}
-Definition foo (x : nat) : nat := $( exact x )$.
+Definition foo (x : nat) : nat := ltac:(exact x).
 \end{coq_example*}
 
 This construction is useful when one wants to define complicated terms using
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fae0bd5e5..b855a0eac 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -828,7 +828,9 @@ either:
     \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]}
     \item the rewriting orientations: {\tt ->} or {\tt <-}
     \end{itemize}
-  \item the on-the-fly application of a lemma: $p${\tt /{\term}}
+  \item the on-the-fly application of lemmas: $p${\tt /{\term$_1$}}
+    \ldots {\tt /{\term$_n$}} where $p$ itself is not an on-the-fly
+    application of lemmas pattern
   \end{itemize}
 \item the wildcard: {\tt \_}
 \end{itemize}
@@ -896,9 +898,10 @@ introduction pattern~$p$:
   itself is erased; if the term to substitute is a variable, it is
   substituted also in the context of goal and the variable is removed
   too;
-\item introduction over a pattern $p${\tt /{\term}} first applies
-  {\term} on the hypothesis to be introduced (as in {\tt apply
-  }{\term} {\tt in}), prior to the application of the introduction
+\item introduction over a pattern $p${\tt /{\term$_1$}} \ldots {\tt
+  /{\term$_n$}} first applies {\term$_1$},\ldots, {\term$_n$} on the
+  hypothesis to be introduced (as in {\tt apply }{\term}$_1$, \ldots,
+  {\term}$_n$ {\tt in}), prior to the application of the introduction
   pattern $p$;
 \item introduction on the wildcard depends on whether the product is
   dependent or not: in the non-dependent case, it erases the
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5160f07af..ba20f9fa0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -447,8 +447,8 @@ let is_projection nargs = function
   | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
     (try
        let n = Recordops.find_projection_nparams r + 1 in
-	 if n <= nargs then None
-	 else Some n
+	 if n <= nargs then Some n
+	 else None
      with Not_found -> None)
   | _ -> None
 	
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 124d4c0fe..73130d380 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -142,7 +142,7 @@ type 'a gen_atomic_tactic_expr =
   | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-      (clear_flag * 'nam * 'dtrm intro_pattern_expr located option) option
+      ('nam * 'dtrm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacFix of Id.t option * int
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e2e6795f7..8df91da24 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -218,7 +218,7 @@ GEXTEND Gram
 	  CGeneralization (!@loc, Implicit, None, c)
       | "`("; c = operconstr LEVEL "200"; ")" ->
 	  CGeneralization (!@loc, Explicit, None, c)
-      | "$("; tac = Tactic.tactic; ")$" ->
+      | "ltac:"; "("; tac = Tactic.tactic_expr; ")" ->
           let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in
           CHole (!@loc, None, IntroAnonymous, Some arg)
       ] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index a4dba506d..4a9ca23f1 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -134,8 +134,8 @@ GEXTEND Gram
   ;
   (* Tactic arguments *)
   tactic_arg:
-    [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
-      | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n)
+    [ [ "ltac:"; a = tactic_expr LEVEL "0" -> arg_of_expr a
+      | "ltac:"; n = natural -> TacGeneric (genarg_of_int n)
       | a = tactic_top_or_arg -> a
       | r = reference -> Reference r
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c94ac846f..b7559a198 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -296,11 +296,17 @@ GEXTEND Gram
       | "**" -> !@loc, IntroForthcoming false ]]
   ;
   simple_intropattern:
+    [ [ pat = simple_intropattern_closed; l = LIST0 ["/"; c = constr -> c] ->
+          let loc0,pat = pat in
+          let f c pat =
+            let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
+            IntroAction (IntroApplyOn (c,(loc,pat))) in
+          !@loc, List.fold_right f l pat ] ]
+  ;
+  simple_intropattern_closed:
     [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat)
       | pat = equality_intropattern -> !@loc, IntroAction pat
       | "_" -> !@loc, IntroAction IntroWildcard 
-      | pat = simple_intropattern; "/"; c = constr ->
-          !@loc, IntroAction (IntroApplyOn (c,pat))
       | pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
   ;
   simple_binding:
@@ -399,7 +405,7 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   in_hyp_as:
-    [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (None,id,ipat)
+    [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
       | -> None ] ]
   ;
   orient:
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index df15be9b3..dab82fa22 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -166,6 +166,18 @@ let _ = declare_bool_option
 	    optread  = print_primproj_params;
 	    optwrite = (:=) print_primproj_params_value }
 
+let print_primproj_compatibility_value = ref true
+let print_primproj_compatibility () = !print_primproj_compatibility_value
+
+let _ = declare_bool_option
+	  { optsync  = true;
+            optdepr  = false;
+	    optname  = "backwards-compatible printing of primitive projections";
+	    optkey   = ["Printing";"Primitive";"Projection";"Compatibility"];
+	    optread  = print_primproj_compatibility;
+	    optwrite = (:=) print_primproj_compatibility_value }
+
+	  
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
 
@@ -476,7 +488,7 @@ let rec detype flags avoid env sigma t =
 	  GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), 
 		[detype flags avoid env sigma c])
       else 
-	if Projection.unfolded p then
+	if print_primproj_compatibility () && Projection.unfolded p then
 	  (** Print the compatibility match version *)
 	  let c' = 
 	    try 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 72d2eedcc..766222156 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -586,8 +586,7 @@ module Make
 
   let pr_in_hyp_as prc pr_id = function
     | None -> mt ()
-    | Some (clear,id,ipat) ->
-      pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat
+    | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
 
   let pr_clauses default_is_concl pr_id = function
     | { onhyps=Some []; concl_occs=occs }
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 06bf955c8..ce930cacb 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -43,7 +43,7 @@ let schedule_vio_checking j fs =
   let rec filter_argv b = function
     | [] -> []
     | "-schedule-vio-checking" :: rest -> filter_argv true rest
-    | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
+    | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest)
     | _ :: rest when b -> filter_argv b rest
     | s :: rest -> s :: filter_argv b rest in
   let pack = function
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index fb22da83a..1778221b0 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -400,8 +400,8 @@ let intern_red_expr ist = function
   | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
 
-let intern_in_hyp_as ist lf (clear,id,ipat) =
-  (clear,intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
+let intern_in_hyp_as ist lf (id,ipat) =
+  (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
 
 let intern_hyp_list ist = List.map (intern_hyp ist)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1928b44b4..f1fd52608 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -907,9 +907,9 @@ let interp_intro_pattern_option ist env sigma = function
       let sigma, ipat = interp_intro_pattern ist env sigma ipat in
       sigma, Some ipat
 
-let interp_in_hyp_as ist env sigma (clear,id,ipat) =
+let interp_in_hyp_as ist env sigma (id,ipat) =
   let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
-  sigma,(clear,interp_hyp ist env sigma id,ipat)
+  sigma,(interp_hyp ist env sigma id,ipat)
 
 let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
@@ -1852,8 +1852,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma,tac = match cl with
           | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
           | Some cl ->
-              let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in
-              sigma, Tactics.apply_delayed_in a ev clear id l cl in
+              let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in
+              sigma, Tactics.apply_delayed_in a ev id l cl in
         Tacticals.New.tclWITHHOLES ev tac sigma
       end }
       end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f99ab4bbf..4fb206ec9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2254,19 +2254,12 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
           Proofview.tclUNIT () (* apply_in_once do a replacement *)
         else
           Proofview.V82.tactic (clear [id]) in
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let sigma = Tacmach.New.project gl in
-        let env = Proofview.Goal.env gl in
-        let (c, sigma) = run_delayed env sigma f in
-        Tacticals.New.tclWITHHOLES false
-          (Tacticals.New.tclTHENFIRST
-             (* Skip the side conditions of the apply *)
-             (apply_in_once false true true true naming id
-                (None,(sigma,(c,NoBindings)))
-                (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id)))
-             (tac thin None []))
-          sigma
-      end }
+      let f = { delayed = fun env sigma ->
+        let Sigma (c, sigma, p) = f.delayed env sigma in
+        Sigma ((c, NoBindings), sigma, p)
+      } in
+      apply_in_delayed_once false true true true naming id (None,(loc,f))
+        (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
 
 and prepare_intros_loc loc dft destopt = function
   | IntroNaming ipat ->
@@ -2325,7 +2318,7 @@ let assert_as first hd ipat t =
 (* apply in as *)
 
 let general_apply_in sidecond_first with_delta with_destruct with_evars
-    with_clear id lemmas ipat =
+    id lemmas ipat =
   let tac (naming,lemma) tac id =
     apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
       naming id lemma tac in
@@ -2350,12 +2343,12 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
     Tacticals.New.tclTHENFIRST (tclMAPFIRST tac lemmas_target) (ipat_tac id)
 *)
 
-let apply_in simple with_evars clear_flag id lemmas ipat =
+let apply_in simple with_evars id lemmas ipat =
   let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, { delayed = fun _ sigma -> Sigma.here l sigma })) lemmas in
-  general_apply_in false simple simple with_evars clear_flag id lemmas ipat
+  general_apply_in false simple simple with_evars id lemmas ipat
 
-let apply_delayed_in simple with_evars clear_flag id lemmas ipat =
-  general_apply_in false simple simple with_evars clear_flag id lemmas ipat
+let apply_delayed_in simple with_evars id lemmas ipat =
+  general_apply_in false simple simple with_evars id lemmas ipat
 
 (*****************************)
 (* Tactics abstracting terms *)
@@ -4680,7 +4673,7 @@ module Simple = struct
   let case   c = general_case_analysis false None (c,NoBindings)
 
   let apply_in id c =
-    apply_in false false None id [None,(Loc.ghost, (c, NoBindings))] None
+    apply_in false false id [None,(Loc.ghost, (c, NoBindings))] None
 
 end
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 8a4717b7b..129837d08 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -196,12 +196,12 @@ val eapply_with_bindings  : constr with_bindings -> unit Proofview.tactic
 val cut_and_apply         : constr -> unit Proofview.tactic
 
 val apply_in :
-  advanced_flag -> evars_flag -> clear_flag -> Id.t -> 
+  advanced_flag -> evars_flag -> Id.t -> 
     (clear_flag * constr with_bindings located) list ->
     intro_pattern option -> unit Proofview.tactic
 
 val apply_delayed_in :
-  advanced_flag -> evars_flag -> clear_flag -> Id.t -> 
+  advanced_flag -> evars_flag -> Id.t -> 
     (clear_flag * delayed_open_constr_with_bindings located) list ->
     intro_pattern option -> unit Proofview.tactic
 
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6274183b3..742395422 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -154,6 +154,9 @@ summary.log:
 	$(SHOW) SUMMARY
 	$(HIDE)$(MAKE) --quiet summary > "$@"
 
+report: summary.log
+	$(HIDE)if grep -F 'Error!' summary.log ; then false; fi
+
 #######################################################################
 # Regression (and progression) tests
 #######################################################################
diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v
index d41d23173..71d457b00 100644
--- a/test-suite/bugs/closed/3249.v
+++ b/test-suite/bugs/closed/3249.v
@@ -5,7 +5,7 @@ Ltac ret_and_left T :=
   lazymatch eval hnf in t with
     | ?a /\ ?b => constr:(proj1 T)
     | forall x : ?T', @?f x =>
-      constr:(fun x : T' => $(let fx := constr:(T x) in
+      constr:(fun x : T' => ltac:(let fx := constr:(T x) in
                               let t := ret_and_left fx in
-                              exact t)$)
+                              exact t))
   end.
diff --git a/test-suite/bugs/closed/3285.v b/test-suite/bugs/closed/3285.v
index 25162329e..68e6b7386 100644
--- a/test-suite/bugs/closed/3285.v
+++ b/test-suite/bugs/closed/3285.v
@@ -1,7 +1,7 @@
 Goal True.
 Proof.
 match goal with
-  | _ => let x := constr:($(fail)$) in idtac
+  | _ => let x := constr:(ltac:(fail)) in idtac
   | _ => idtac
 end.
 Abort.
diff --git a/test-suite/bugs/closed/3286.v b/test-suite/bugs/closed/3286.v
index b08b7ab3c..701480fc8 100644
--- a/test-suite/bugs/closed/3286.v
+++ b/test-suite/bugs/closed/3286.v
@@ -6,20 +6,20 @@ Ltac make_apply_under_binders_in lem H :=
     | forall x : ?T, @?P x
       => let ret := constr:(fun x' : T =>
                               let Hx := H x' in
-                              $(let ret' := tac lem Hx in
-                                exact ret')$) in
+                              ltac:(let ret' := tac lem Hx in
+                                exact ret')) in
          match eval cbv zeta in ret with
            | fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in
                                       constr:(Some P')
          end
-    | _ => let ret := constr:($(match goal with
+    | _ => let ret := constr:(ltac:(match goal with
                                   | _ => (let H' := fresh in
                                           pose H as H';
                                           apply lem in H';
                                           exact (Some H'))
                                   | _ => exact (@None nat)
                                 end
-                               )$) in
+                               )) in
            let ret' := (eval cbv beta zeta in ret) in
            constr:(ret')
     | _ => constr:(@None nat)
diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v
index fb3791af5..a5782298c 100644
--- a/test-suite/bugs/closed/3314.v
+++ b/test-suite/bugs/closed/3314.v
@@ -1,9 +1,9 @@
 Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Definition Lift
-: $(let U1 := constr:(Type) in
+: ltac:(let U1 := constr:(Type) in
     let U0 := constr:(Type : U1) in
-    exact (U0 -> U1))$
+    exact (U0 -> U1))
   := fun T => T.
 
 Fail Check nat:Prop. (* The command has indeed failed with message:
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index e6a50449d..e3b5e9435 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -8,7 +8,7 @@ Inductive foo : Type@{l} := bar : foo .
 Section MakeEq.
   Variables (a : foo@{i}) (b : foo@{j}).
 
-  Let t := $(let ty := type of b in exact ty)$.
+  Let t := ltac:(let ty := type of b in exact ty).
   Definition make_eq (x:=b) := a : t.
 End MakeEq.
 
diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v
index 63d5c7a57..dcf5394ea 100644
--- a/test-suite/bugs/closed/3347.v
+++ b/test-suite/bugs/closed/3347.v
@@ -1,7 +1,7 @@
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *)
 Set Universe Polymorphism.
-Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
+Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing).
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
 Inductive Unit : Type1 := tt : Unit.
 Fail Check Unit : Set. (* [Check Unit : Set] should fail if [Type1] is defined correctly *)
diff --git a/test-suite/bugs/closed/3354.v b/test-suite/bugs/closed/3354.v
index 14b66db36..a635285f2 100644
--- a/test-suite/bugs/closed/3354.v
+++ b/test-suite/bugs/closed/3354.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
-Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
+Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing).
 Inductive Empty : Type1 := .
 Fail Check Empty : Set.
 (* Toplevel input, characters 15-116:
diff --git a/test-suite/bugs/closed/3467.v b/test-suite/bugs/closed/3467.v
index 7e3711624..88ae03057 100644
--- a/test-suite/bugs/closed/3467.v
+++ b/test-suite/bugs/closed/3467.v
@@ -1,5 +1,5 @@
 Module foo.
-  Notation x := $(exact I)$.
+  Notation x := ltac:(exact I).
 End foo.
 Module bar.
   Include foo.
diff --git a/test-suite/bugs/closed/3487.v b/test-suite/bugs/closed/3487.v
index 03c60a8ba..1321a8598 100644
--- a/test-suite/bugs/closed/3487.v
+++ b/test-suite/bugs/closed/3487.v
@@ -1,4 +1,4 @@
-Notation bar := $(exact I)$.
+Notation bar := ltac:(exact I).
 Notation foo := bar (only parsing).
 Class baz := { x : False }.
 Instance: baz.
diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v
index 2a282d221..9d37d1a2d 100644
--- a/test-suite/bugs/closed/3682.v
+++ b/test-suite/bugs/closed/3682.v
@@ -3,4 +3,4 @@ Class Foo.
 Definition bar `{Foo} (x : Set) := Set.
 Instance: Foo.
 Definition bar1 := bar nat.
-Definition bar2 := bar $(admit)$.
+Definition bar2 := bar ltac:(admit).
diff --git a/test-suite/bugs/closed/3684.v b/test-suite/bugs/closed/3684.v
index f7b137386..130d57779 100644
--- a/test-suite/bugs/closed/3684.v
+++ b/test-suite/bugs/closed/3684.v
@@ -1,5 +1,5 @@
 Require Import TestSuite.admit.
 Definition foo : Set.
 Proof.
-  refine ($(abstract admit)$).
+  refine (ltac:(abstract admit)).
 Qed.
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index df9f5f476..c24173abf 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -18,7 +18,7 @@ Top.8}
    Top.6
    Top.7
    Top.8 |=  *) *)
-Definition bar := $(let t := eval compute in foo in exact t)$.
+Definition bar := ltac:(let t := eval compute in foo in exact t).
 Check @bar. (* bar@{Top.13 Top.14 Top.15
 Top.16}
      : Type@{Top.16+1}
diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v
index 4408ab885..070d1e9c7 100644
--- a/test-suite/bugs/closed/3881.v
+++ b/test-suite/bugs/closed/3881.v
@@ -8,7 +8,7 @@ Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Axiom admit : forall {T}, T.
 Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity).
-Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *)
+Notation "g 'o' f" := ltac:(let g' := g in let f' := f in exact (fun x => g' (f' x))) (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *)
 Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope.
 Arguments eq_refl {_ _}.
 Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end.
diff --git a/test-suite/bugs/closed/4149.v b/test-suite/bugs/closed/4149.v
new file mode 100644
index 000000000..b81c680cd
--- /dev/null
+++ b/test-suite/bugs/closed/4149.v
@@ -0,0 +1,4 @@
+Goal forall A, A -> Type.
+Proof.
+  intros; eauto.
+Qed.
diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v
index db3b60eda..017780c1f 100644
--- a/test-suite/bugs/closed/HoTT_coq_077.v
+++ b/test-suite/bugs/closed/HoTT_coq_077.v
@@ -30,7 +30,7 @@ Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B)
            (p : prod A B) : P p
   := u (fst p) (snd p).
 
-Notation typeof x := ($(let T := type of x in exact T)$) (only parsing).
+Notation typeof x := (ltac:(let T := type of x in exact T)) (only parsing).
 
 (* Check for eta *)
 Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect').
diff --git a/test-suite/bugs/closed/HoTT_coq_114.v b/test-suite/bugs/closed/HoTT_coq_114.v
index 341128338..3535e6c41 100644
--- a/test-suite/bugs/closed/HoTT_coq_114.v
+++ b/test-suite/bugs/closed/HoTT_coq_114.v
@@ -1 +1 @@
-Inductive test : $(let U := type of Type in exact U)$ := t.
+Inductive test : ltac:(let U := type of Type in exact U) := t.
diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v
index 9e7d1eb5d..33c408a28 100644
--- a/test-suite/bugs/opened/3248.v
+++ b/test-suite/bugs/opened/3248.v
@@ -3,7 +3,7 @@ Ltac ret_and_left f :=
   let T := type of f in
   lazymatch eval hnf in T with
     | ?T' -> _ =>
-      let ret := constr:(fun x' : T' => $(tac (f x'))$) in
+      let ret := constr:(fun x' : T' => ltac:(tac (f x'))) in
       exact ret
     | ?T' => exact f
   end.
@@ -12,6 +12,6 @@ Goal forall A B : Prop, forall x y : A, True.
 Proof.
   intros A B x y.
   pose (f := fun (x y : A) => conj x y).
-  pose (a := $(ret_and_left f)$).
+  pose (a := ltac:(ret_and_left f)).
   Fail unify (a x y) (conj x y).
 Abort.
diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/3277.v
index 19ed787d1..5f4231363 100644
--- a/test-suite/bugs/opened/3277.v
+++ b/test-suite/bugs/opened/3277.v
@@ -4,4 +4,4 @@ Goal True.
   evarr _.
 Admitted.
 Goal True.
-  Fail exact $(evarr _)$. (* Error: Cannot infer this placeholder. *)
+  Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *)
diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v
index ced535afd..1c6deae94 100644
--- a/test-suite/bugs/opened/3278.v
+++ b/test-suite/bugs/opened/3278.v
@@ -1,8 +1,8 @@
 Module a.
   Check let x' := _ in
-             $(exact x')$.
+             ltac:(exact x').
 
-  Notation foo x := (let x' := x in $(exact x')$).
+  Notation foo x := (let x' := x in ltac:(exact x')).
 
   Fail Check foo _. (* Error:
 Cannot infer an internal placeholder of type "Type" in environment:
@@ -12,10 +12,10 @@ x' := ?42 : ?41
 End a.
 
 Module b.
-  Notation foo x := (let x' := x in let y := ($(exact I)$ : True) in I).
+  Notation foo x := (let x' := x in let y := (ltac:(exact I) : True) in I).
   Notation bar x := (let x' := x in let y := (I : True) in I).
 
-  Check let x' := _ in $(exact I)$. (* let x' := ?5 in I *)
+  Check let x' := _ in ltac:(exact I). (* let x' := ?5 in I *)
   Check bar _. (* let x' := ?9 in let y := I in I *)
   Fail Check foo _. (* Error:
 Cannot infer an internal placeholder of type "Type" in environment:
diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/3304.v
index 529cc737d..66668930c 100644
--- a/test-suite/bugs/opened/3304.v
+++ b/test-suite/bugs/opened/3304.v
@@ -1,3 +1,3 @@
-Fail Notation "( x , y , .. , z )" := $(let r := constr:(prod .. (prod x y) .. z) in r)$.
+Fail Notation "( x , y , .. , z )" := ltac:(let r := constr:(prod .. (prod x y) .. z) in r).
 (* The command has indeed failed with message:
 => Error: Special token .. is for use in the Notation command. *)
diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v
index 9e6107b30..762611f75 100644
--- a/test-suite/bugs/opened/3459.v
+++ b/test-suite/bugs/opened/3459.v
@@ -7,9 +7,9 @@ Proof.
 (* This line used to fail with a Not_found up to some point, and then
    to produce an ill-typed term *)
 match goal with
-  | [ |- context G[2] ] => let y := constr:(fun x => $(let r := constr:(@eq Set x x) in
+  | [ |- context G[2] ] => let y := constr:(fun x => ltac:(let r := constr:(@eq Set x x) in
                                                        clear x;
-                                                       exact r)$) in
+                                                       exact r)) in
                            pose y
 end.
 (* Add extra test for typability (should not fail when bug closed) *)
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 35ba94fb6..741f372ff 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -69,3 +69,12 @@ intros H (H1,?)/H.
 change (1=1) in H0.
 exact H1.
 Qed.
+
+(* Checking iterated pat/c1.../cn introduction patterns and side conditions *)
+
+Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D.
+intros * H H0 H1.
+intros H2/H/H0.
+- exact H2.
+- exact H1.
+Qed.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index d6bbfe29a..878875bd9 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -242,7 +242,7 @@ Fail Check (Prop : Set).
 Fail Check (Set : Set).
 Check (Set : Type).
 Check (Prop : Type).
-Definition setType := $(let t := type of Set in exact t)$.
+Definition setType := ltac:(let t := type of Set in exact t).
 
 Definition foo (A : Prop) := A.
 
@@ -303,7 +303,7 @@ Set Printing Universes.
 Axiom admit : forall A, A.
 Record R := {O : Type}.
 
-Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}.
+Definition RL (x : R@{i}) : ltac:(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) ) := {|O := @O x|}.
 Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl.
 Definition RLRL' : forall x : R, RL x = RL (RL x).
   intros. apply eq_refl.
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 66bf9b383..bfa49fab8 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -309,6 +309,7 @@ type program_info_aux = {
   prg_reduce : constr -> constr;
   prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook;
   prg_opaque : bool;
+  prg_sign: named_context_val;
 }
 
 type program_info = program_info_aux Ephemeron.key
@@ -634,7 +635,7 @@ let declare_obligation prg obl body ty uctx =
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
 
-let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls kind reduce hook =
+let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls impls kind reduce hook =
   let obls', b = 
     match b with
     | None ->
@@ -658,8 +659,8 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
-      prg_hook = hook;
-      prg_opaque = opaque; }
+      prg_hook = hook; prg_opaque = opaque;
+      prg_sign = sign }
 
 let map_cardinal m =
   let i = ref 0 in
@@ -877,10 +878,11 @@ let rec solve_obligation prg num tac =
   let obl = subst_deps_obl obls obl in
   let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
   let evd = Evd.from_ctx prg.prg_ctx in
+  let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
   let terminator guard hook = Proof_global.make_terminator (obligation_terminator prg.prg_name num guard hook) in
   let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
-  let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type ~terminator hook in
+  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
   let () = trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
             Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in
   let _ = Pfedit.by (snd (get_default_tactic ())) in
@@ -914,9 +916,11 @@ and solve_obligation_by_tac prg obls i tac =
 		  | Some t -> t
 		  | None -> snd (get_default_tactic ())
 	    in
+	    let evd = Evd.from_ctx !prg.prg_ctx in
+	    let evd = Evd.update_sigma_env evd (Global.env ()) in
 	    let t, ty, ctx = 
 	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac 
-	        (pi2 !prg.prg_kind) !prg.prg_ctx
+	        (pi2 !prg.prg_kind) (Evd.evar_universe_context evd)
 	    in
 	    let uctx = Evd.evar_context_universe_context ctx in
 	    let () = prg := {!prg with prg_ctx = ctx} in
@@ -1015,8 +1019,9 @@ let show_term n =
 
 let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
     ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
+  let sign = Decls.initialize_named_context_for_proof () in
   let info = str (Id.to_string n) ++ str " has type-checked" in
-  let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
+  let prg = init_prog_info sign ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose msg_info (info ++ str ".");
@@ -1033,10 +1038,11 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
 
 let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
     ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
+  let sign = Decls.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind)
+     let prg = init_prog_info sign ~opaque n (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
      in progmap_add n (Ephemeron.create prg)) l;
     let _defined =