Merge branch 'v8.5'

42 files changed, 130 insertions, 86 deletions

diff --git a/CHANGES b/CHANGES
index a77889fc42..9da642b0f6 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 957592640f..37c8e4c674 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 1b1d3500a4..492e75a7bb 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 b77118e1f9..80e12898f0 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 fae0bd5e51..b855a0eacc 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 5160f07af0..ba20f9fa06 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 124d4c0fef..73130d3804 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 e2e6795f73..8df91da24b 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 a4dba506d2..4a9ca23f15 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 c94ac846f1..b7559a1989 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 df15be9b30..dab82fa22b 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 72d2eedcc3..766222156a 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 06bf955c82..ce930cacb7 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 fb22da83aa..1778221b02 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 1928b44b47..f1fd526082 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 f99ab4bbf9..4fb206ec94 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 8a4717b7ba..129837d082 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 6274183b36..7423954222 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 d41d231739..71d457b002 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 25162329ef..68e6b7386f 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 b08b7ab3cc..701480fc83 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 fb3791af55..a5782298c3 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 e6a50449da..e3b5e94356 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 63d5c7a57b..dcf5394eaf 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 14b66db362..a635285f2c 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 7e37116249..88ae030578 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 03c60a8baa..1321a8598c 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 2a282d221f..9d37d1a2d0 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 f7b137386b..130d57779d 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 df9f5f4761..c24173abf1 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 4408ab885d..070d1e9c71 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 0000000000..b81c680cd7
--- /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 db3b60edae..017780c1f3 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 341128338e..3535e6c41f 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 9e7d1eb5dd..33c408a28c 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 19ed787d1e..5f4231363a 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 ced535afd5..1c6deae94b 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 529cc737df..66668930c7 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 9e6107b30a..762611f751 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 35ba94fb67..741f372ff2 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 d6bbfe29ac..878875bd92 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 66bf9b383d..bfa49fab86 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 =