From 30efd8d3501ff724e6f75acf7c2355a107da1c70 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 30 Nov 2015 12:36:04 +0100
Subject: Test for bug #4149.

---
 test-suite/bugs/closed/4149.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/4149.v

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.
-- 
cgit v1.2.3


From 315aac9ae0d411c10849c421d5dfd8e134919233 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 1 Dec 2015 11:30:35 +0100
Subject: vio: fix argument parsing (progress on #4442)

---
 stm/vio_checking.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3


From 16504ad480a920e1800d52f5adbea8ddecefbeb0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 2 Dec 2015 14:28:29 +0100
Subject: Fix a bug in externalisation which prevented printing of projections
 using dot notation.

---
 interp/constrextern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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
 	
-- 
cgit v1.2.3


From c62eb0470975c9b5960a49a90b49b4aa191efd1c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 2 Dec 2015 15:37:14 +0100
Subject: Add an option to deactivate compatibility printing of primitive
 projections (off by default).

---
 pretyping/detyping.ml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b5228094a2..67261def0b 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 
-- 
cgit v1.2.3


From 42c68765690710b16f3e878bf1d914eaa75d8291 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 2 Dec 2015 17:35:25 +0100
Subject: Fix bug #4444: Next Obligation performed after a Section opening was
 using the wrong context.

This is very bad style but currently unavoidable, at least we don't
throw an anomaly anymore.
---
 toplevel/obligations.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index e091d825cd..f2b0380786 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -320,6 +320,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
@@ -643,7 +644,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 ->
@@ -667,8 +668,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
@@ -858,7 +859,7 @@ let rec solve_obligation prg num tac =
   let evd = Evd.from_ctx prg.prg_ctx in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac 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 hook in
+  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type 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
@@ -993,8 +994,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 ".");
@@ -1011,10 +1013,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 =
-- 
cgit v1.2.3


From 2374a23fb7ebfa547eb16ce2ab8dc9efb2a3f855 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 2 Dec 2015 17:52:07 +0100
Subject: Univs/Program: update the universe context with global universe
 constraints at the time of Next Obligation/Solve Obligations so that
 interleaving definitions and obligation solving commands works properly.

---
 toplevel/obligations.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index f2b0380786..314789ced6 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -857,6 +857,7 @@ 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 hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
   let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type hook in
@@ -893,9 +894,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
-- 
cgit v1.2.3


From 9205d8dc7b9e97b6c2f0815fddc5673c21d11089 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 2 Nov 2015 12:26:53 +0100
Subject: Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in
 WG.

---
 CHANGES                               | 8 ++++++++
 doc/refman/RefMan-ext.tex             | 4 ++--
 parsing/g_constr.ml4                  | 2 +-
 parsing/g_ltac.ml4                    | 4 ++--
 test-suite/bugs/closed/3249.v         | 4 ++--
 test-suite/bugs/closed/3285.v         | 2 +-
 test-suite/bugs/closed/3286.v         | 8 ++++----
 test-suite/bugs/closed/3314.v         | 4 ++--
 test-suite/bugs/closed/3330.v         | 2 +-
 test-suite/bugs/closed/3347.v         | 2 +-
 test-suite/bugs/closed/3354.v         | 2 +-
 test-suite/bugs/closed/3467.v         | 2 +-
 test-suite/bugs/closed/3487.v         | 2 +-
 test-suite/bugs/closed/3682.v         | 2 +-
 test-suite/bugs/closed/3684.v         | 2 +-
 test-suite/bugs/closed/3690.v         | 2 +-
 test-suite/bugs/closed/3881.v         | 2 +-
 test-suite/bugs/closed/HoTT_coq_077.v | 2 +-
 test-suite/bugs/closed/HoTT_coq_114.v | 2 +-
 test-suite/bugs/opened/3248.v         | 4 ++--
 test-suite/bugs/opened/3277.v         | 2 +-
 test-suite/bugs/opened/3278.v         | 8 ++++----
 test-suite/bugs/opened/3304.v         | 2 +-
 test-suite/bugs/opened/3459.v         | 4 ++--
 test-suite/success/polymorphism.v     | 4 ++--
 25 files changed, 45 insertions(+), 37 deletions(-)

diff --git a/CHANGES b/CHANGES
index 07d6281717..662b7b9a24 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,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
@@ -83,6 +87,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/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/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/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/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/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.
-- 
cgit v1.2.3


From 7a33a6284ba4e0953f82cf436fe324cdb95497e7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Dec 2015 12:10:29 +0100
Subject: Update history of revisions.

---
 dev/doc/versions-history.tex | 1 +
 1 file changed, 1 insertion(+)

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] \\
-- 
cgit v1.2.3


From cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Dec 2015 15:18:42 +0100
Subject: Dead code from August 2014 in apply in.

---
 intf/tacexpr.mli     |  2 +-
 parsing/g_tactic.ml4 |  2 +-
 printing/pptactic.ml |  3 +--
 tactics/tacintern.ml |  4 ++--
 tactics/tacinterp.ml |  8 ++++----
 tactics/tactics.ml   | 12 ++++++------
 tactics/tactics.mli  |  4 ++--
 7 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index eb4e5ae7d3..8c55a57051 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -136,7 +136,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_tactic.ml4 b/parsing/g_tactic.ml4
index c94ac846f1..8e5e1f1fb8 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -399,7 +399,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/printing/pptactic.ml b/printing/pptactic.ml
index a669aef9a8..bc559460e0 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -581,8 +581,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/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 ee21a51598..693b382cac 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -902,9 +902,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
@@ -1835,8 +1835,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 8daa7c4b86..d4480ec922 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2287,7 +2287,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
@@ -2312,12 +2312,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, fun _ sigma -> sigma, l)) 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 *)
@@ -4553,7 +4553,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 ade89fc989..b9a0184180 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
 
-- 
cgit v1.2.3


From 6ab4479dfa0f9b8fd4df4342fdfdab6c25b62fb7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Dec 2015 12:10:53 +0100
Subject: Improving syntax of pat/constr introduction pattern so that
 pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.

Open to other suggestions of syntax though.
---
 doc/refman/RefMan-tac.tex   | 11 +++++++----
 parsing/g_tactic.ml4        | 10 ++++++++--
 test-suite/success/intros.v |  9 +++++++++
 3 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1551b8eefd..03c4f6a365 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/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 8e5e1f1fb8..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:
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.
-- 
cgit v1.2.3


From a80351f98adeada2b9219679de130e28c1b41479 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Dec 2015 14:04:33 +0100
Subject: Slight simplification of code for pat/constr.

---
 tactics/tactics.ml | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d4480ec922..3e6cea5ddd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2216,19 +2216,9 @@ 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 begin fun gl ->
-        let sigma = Proofview.Goal.sigma gl in
-        let env = Proofview.Goal.env gl in
-        let sigma,c = f env sigma 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 env sigma = let (sigma,c) = f env sigma in (sigma,(c,NoBindings)) 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 ->
-- 
cgit v1.2.3


From 6316e8b380a9942cd587f250eb4a69668e52019e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Dec 2015 18:24:03 +0100
Subject: Adding a target report to test-suite's Makefile to get a short
 summary.

---
 Makefile.build      | 2 +-
 test-suite/Makefile | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/Makefile.build b/Makefile.build
index 0455a247bd..98ef81f38c 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/test-suite/Makefile b/test-suite/Makefile
index 31b2129001..7150d1fd4f 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
 #######################################################################
-- 
cgit v1.2.3