21 files changed, 260 insertions, 205 deletions

diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.mlg
index 3ae0f45cb7..312ef1e555 100644
--- a/plugins/btauto/g_btauto.ml4
+++ b/plugins/btauto/g_btauto.mlg
@@ -8,11 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 
+}
+
 DECLARE PLUGIN "btauto_plugin"
 
 TACTIC EXTEND btauto
-| [ "btauto" ] -> [ Refl_btauto.Btauto.tac ]
+| [ "btauto" ] -> { Refl_btauto.Btauto.tac }
 END
 
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.mlg
index fb013ac131..685059294f 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.mlg
@@ -8,22 +8,26 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 open Cctac
 open Stdarg
 
+}
+
 DECLARE PLUGIN "cc_plugin"
 
 (* Tactic registration *)
 
 TACTIC EXTEND cc
- [ "congruence" ] -> [ congruence_tac 1000 [] ]
- |[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
+| [ "congruence" ] -> { congruence_tac 1000 [] }
+| [ "congruence" integer(n) ] -> { congruence_tac n [] }
+| [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l }
  |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
-   [ congruence_tac n l ]
+   { congruence_tac n l }
 END
 
 TACTIC EXTEND f_equal
- [ "f_equal" ] -> [ f_equal ]
+| [ "f_equal" ] -> { f_equal }
 END
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.mlg
index 44560ac18e..703e29f964 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.mlg
@@ -8,11 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 open FourierR
 
+}
+
 DECLARE PLUGIN "fourier_plugin"
 
 TACTIC EXTEND fourier
-  [ "fourierz" ] -> [ fourier () ]
+| [ "fourierz" ] -> { fourier () }
 END
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 31496513a7..b2a528a1fd 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -322,8 +322,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
   try
 
   let f = funs.(i) in
-  let env = Global.env () in    
-  let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in
+  let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in
   let new_sorts =
     match sorts with
       | None -> Array.make (Array.length funs) (type_sort)
@@ -344,7 +343,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       (*     let id_of_f = Label.to_id (con_label f) in *)
       let register_with_sort fam_sort =
         let evd' = Evd.from_env (Global.env ()) in
-        let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
+        let evd',s = Evd.fresh_sort_in_family evd' fam_sort in
         let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
         let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
         let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
@@ -354,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
           Evd.const_univ_entry ~poly evd'
         in
         let ce = Declare.definition_entry ~univs value in
-	ignore(
+        ignore(
 	  Declare.declare_constant
 	    name
 	    (DefinitionEntry ce,
@@ -508,8 +507,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
   let i = ref (-1) in
   let sorts =
     List.rev_map (fun (_,x) ->
-		  Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x
-	     )
+                  Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x
+             )
       fas
   in
   (* We create the first priciple by tactic *)
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.mlg
index 61525cb49d..6388906f5e 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Util
 open Locus
 open Tactypes
@@ -18,147 +20,153 @@ open Tacarg
 open Names
 open Logic
 
+let wit_hyp = wit_var
+
+}
+
 DECLARE PLUGIN "ltac_plugin"
 
 (** Basic tactics *)
 
 TACTIC EXTEND reflexivity
-  [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
+| [ "reflexivity" ] -> { Tactics.intros_reflexivity }
 END
 
 TACTIC EXTEND exact
-  [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ]
+| [ "exact" casted_constr(c) ] -> { Tactics.exact_no_check c }
 END
 
 TACTIC EXTEND assumption
-  [ "assumption" ] -> [ Tactics.assumption ]
+| [ "assumption" ] -> { Tactics.assumption }
 END
 
 TACTIC EXTEND etransitivity
-  [ "etransitivity" ] -> [ Tactics.intros_transitivity None ]
+| [ "etransitivity" ] -> { Tactics.intros_transitivity None }
 END
 
 TACTIC EXTEND cut
-  [ "cut" constr(c) ] -> [ Tactics.cut c ]
+| [ "cut" constr(c) ] -> { Tactics.cut c }
 END
 
 TACTIC EXTEND exact_no_check
-  [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
+| [ "exact_no_check" constr(c) ] -> { Tactics.exact_no_check c }
 END
 
 TACTIC EXTEND vm_cast_no_check
-  [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ]
+| [ "vm_cast_no_check" constr(c) ] -> { Tactics.vm_cast_no_check c }
 END
 
 TACTIC EXTEND native_cast_no_check
-  [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ]
+| [ "native_cast_no_check" constr(c) ] -> { Tactics.native_cast_no_check c }
 END
 
 TACTIC EXTEND casetype
-  [ "casetype" constr(c) ] -> [ Tactics.case_type c ]
+| [ "casetype" constr(c) ] -> { Tactics.case_type c }
 END
 
 TACTIC EXTEND elimtype
-  [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ]
+| [ "elimtype" constr(c) ] -> { Tactics.elim_type c }
 END
 
 TACTIC EXTEND lapply
-  [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ]
+| [ "lapply" constr(c) ] -> { Tactics.cut_and_apply c }
 END
 
 TACTIC EXTEND transitivity
-  [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ]
+| [ "transitivity" constr(c) ] -> { Tactics.intros_transitivity (Some c) }
 END
 
 (** Left *)
 
 TACTIC EXTEND left
-  [ "left" ] -> [ Tactics.left_with_bindings false NoBindings ]
+| [ "left" ] -> { Tactics.left_with_bindings false NoBindings }
 END
 
 TACTIC EXTEND eleft
-  [ "eleft" ] -> [ Tactics.left_with_bindings true NoBindings ]
+| [ "eleft" ] -> { Tactics.left_with_bindings true NoBindings }
 END
 
 TACTIC EXTEND left_with
-  [ "left" "with" bindings(bl) ] -> [
+| [ "left" "with" bindings(bl) ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl)
-  ]
+  }
 END
 
 TACTIC EXTEND eleft_with
-  [ "eleft" "with" bindings(bl) ] -> [
+| [ "eleft" "with" bindings(bl) ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl)
-  ]
+  }
 END
 
 (** Right *)
 
 TACTIC EXTEND right
-  [ "right" ] -> [ Tactics.right_with_bindings false NoBindings ]
+| [ "right" ] -> { Tactics.right_with_bindings false NoBindings }
 END
 
 TACTIC EXTEND eright
-  [ "eright" ] -> [ Tactics.right_with_bindings true NoBindings ]
+| [ "eright" ] -> { Tactics.right_with_bindings true NoBindings }
 END
 
 TACTIC EXTEND right_with
-  [ "right" "with" bindings(bl) ] -> [
+| [ "right" "with" bindings(bl) ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl)
-  ]
+  }
 END
 
 TACTIC EXTEND eright_with
-  [ "eright" "with" bindings(bl) ] -> [
+| [ "eright" "with" bindings(bl) ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl)
-  ]
+  }
 END
 
 (** Constructor *)
 
 TACTIC EXTEND constructor
-  [ "constructor" ] -> [ Tactics.any_constructor false None ]
-| [ "constructor" int_or_var(i) ] -> [
+| [ "constructor" ] -> { Tactics.any_constructor false None }
+| [ "constructor" int_or_var(i) ] -> {
     Tactics.constructor_tac false None i NoBindings
-  ]
-| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
+  }
+| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> {
     let tac bl = Tactics.constructor_tac false None i bl in
     Tacticals.New.tclDELAYEDWITHHOLES false bl tac
-  ]
+  }
 END
 
 TACTIC EXTEND econstructor
-  [ "econstructor" ] -> [ Tactics.any_constructor true None ]
-| [ "econstructor" int_or_var(i) ] -> [
+| [ "econstructor" ] -> { Tactics.any_constructor true None }
+| [ "econstructor" int_or_var(i) ] -> {
     Tactics.constructor_tac true None i NoBindings
-  ]
-| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
+  }
+| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> {
     let tac bl = Tactics.constructor_tac true None i bl in
     Tacticals.New.tclDELAYEDWITHHOLES true bl tac
-  ]
+  }
 END
 
 (** Specialize *)
 
 TACTIC EXTEND specialize
-  [ "specialize" constr_with_bindings(c) ] -> [
+| [ "specialize" constr_with_bindings(c) ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None)
-  ]
-| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [
+  }
+| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat))
-  ]
+  }
 END
 
 TACTIC EXTEND symmetry
-  [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
+| [ "symmetry" ] -> { Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} }
 END
 
 TACTIC EXTEND symmetry_in
-| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ]
+| [ "symmetry" "in" in_clause(cl) ] -> { Tactics.intros_symmetry cl }
 END
 
 (** Split *)
 
+{
+
 let rec delayed_list = function
 | [] -> fun _ sigma -> (sigma, [])
 | x :: l ->
@@ -167,147 +175,159 @@ let rec delayed_list = function
     let (sigma, l) = delayed_list l env sigma in
     (sigma, x :: l)
 
+}
+
 TACTIC EXTEND split
-  [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
+| [ "split" ] -> { Tactics.split_with_bindings false [NoBindings] }
 END
 
 TACTIC EXTEND esplit
-  [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
+| [ "esplit" ] -> { Tactics.split_with_bindings true [NoBindings] }
 END
 
 TACTIC EXTEND split_with
-  [ "split" "with" bindings(bl) ] -> [
+| [ "split" "with" bindings(bl) ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl])
-  ]
+  }
 END
 
 TACTIC EXTEND esplit_with
-  [ "esplit" "with" bindings(bl) ] -> [
+| [ "esplit" "with" bindings(bl) ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl])
-  ]
+  }
 END
 
 TACTIC EXTEND exists
-  [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
-| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [
+| [ "exists" ] -> { Tactics.split_with_bindings false [NoBindings] }
+| [ "exists" ne_bindings_list_sep(bll, ",") ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll)
-  ]
+  }
 END
 
 TACTIC EXTEND eexists
-  [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
-| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [
+| [ "eexists" ] -> { Tactics.split_with_bindings true [NoBindings] }
+| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> {
     Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll)
-  ]
+  }
 END
 
 (** Intro *)
 
 TACTIC EXTEND intros_until
-  [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
+| [ "intros" "until" quantified_hypothesis(h) ] -> { Tactics.intros_until h }
 END
 
 TACTIC EXTEND intro
-| [ "intro" ] -> [ Tactics.intro_move None MoveLast ]
-| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ]
-| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ]
-| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ]
-| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ]
-| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ]
-| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ]
-| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ]
-| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ]
-| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ]
+| [ "intro" ] -> { Tactics.intro_move None MoveLast }
+| [ "intro" ident(id) ] -> { Tactics.intro_move (Some id) MoveLast }
+| [ "intro" ident(id) "at" "top" ] -> { Tactics.intro_move (Some id) MoveFirst }
+| [ "intro" ident(id) "at" "bottom" ] -> { Tactics.intro_move (Some id) MoveLast }
+| [ "intro" ident(id) "after" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveAfter h) }
+| [ "intro" ident(id) "before" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveBefore h) }
+| [ "intro" "at" "top" ] -> { Tactics.intro_move None MoveFirst }
+| [ "intro" "at" "bottom" ] -> { Tactics.intro_move None MoveLast }
+| [ "intro" "after" hyp(h) ] -> { Tactics.intro_move None (MoveAfter h) }
+| [ "intro" "before" hyp(h) ] -> { Tactics.intro_move None (MoveBefore h) }
 END
 
 (** Move *)
 
 TACTIC EXTEND move
-  [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ]
-| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ]
-| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ]
-| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
+| [ "move" hyp(id) "at" "top" ] -> { Tactics.move_hyp id MoveFirst }
+| [ "move" hyp(id) "at" "bottom" ] -> { Tactics.move_hyp id MoveLast }
+| [ "move" hyp(id) "after" hyp(h) ] -> { Tactics.move_hyp id (MoveAfter h) }
+| [ "move" hyp(id) "before" hyp(h) ] -> { Tactics.move_hyp id (MoveBefore h) }
 END
 
 (** Rename *)
 
 TACTIC EXTEND rename
-| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ]
+| [ "rename" ne_rename_list_sep(ids, ",") ] -> { Tactics.rename_hyp ids }
 END
 
 (** Revert *)
 
 TACTIC EXTEND revert
-  [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ]
+| [ "revert" ne_hyp_list(hl) ] -> { Tactics.revert hl }
 END
 
 (** Simple induction / destruct *)
 
+{
+
 let simple_induct h =
   Tacticals.New.tclTHEN (Tactics.intros_until h)
     (Tacticals.New.onLastHyp Tactics.simplest_elim)
 
+}
+
 TACTIC EXTEND simple_induction
-  [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ]
+| [ "simple" "induction" quantified_hypothesis(h) ] -> { simple_induct h }
 END
 
+{
+
 let simple_destruct h =
   Tacticals.New.tclTHEN (Tactics.intros_until h)
     (Tacticals.New.onLastHyp Tactics.simplest_case)
 
+}
+
 TACTIC EXTEND simple_destruct
-  [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ]
+| [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h }
 END
 
 (** Double induction *)
 
 TACTIC EXTEND double_induction
-  [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
-  [ Elim.h_double_induction h1 h2 ]
+| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
+  { Elim.h_double_induction h1 h2 }
 END
 
 (* Admit *)
 
 TACTIC EXTEND admit
- [ "admit" ] -> [ Proofview.give_up ]
+|[ "admit" ] -> { Proofview.give_up }
 END
 
 (* Fix *)
 
 TACTIC EXTEND fix
-  [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ]
+| [ "fix" ident(id) natural(n) ] -> { Tactics.fix id n }
 END
 
 (* Cofix *)
 
 TACTIC EXTEND cofix
-  [ "cofix" ident(id) ] -> [ Tactics.cofix id ]
+| [ "cofix" ident(id) ] -> { Tactics.cofix id }
 END
 
 (* Clear *)
 
 TACTIC EXTEND clear
-  [ "clear" hyp_list(ids) ] -> [
+| [ "clear" hyp_list(ids) ] -> {
     if List.is_empty ids then Tactics.keep []
     else Tactics.clear ids
-  ]
-| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
+  }
+| [ "clear" "-" ne_hyp_list(ids) ] -> { Tactics.keep ids }
 END
 
 (* Clearbody *)
 
 TACTIC EXTEND clearbody
-  [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ]
+| [ "clearbody" ne_hyp_list(ids) ] -> { Tactics.clear_body ids }
 END
 
 (* Generalize dependent *)
 
 TACTIC EXTEND generalize_dependent
-  [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ]
+| [ "generalize" "dependent" constr(c) ] -> { Tactics.generalize_dep c }
 END
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
+{
+
 open Tacexpr
 
 let initial_atomic () =
@@ -364,3 +384,5 @@ let initial_tacticals () =
   ]
 
 let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"
+
+}
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 660e29ca82..f24ab2bddb 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -293,7 +293,7 @@ open Vars
 
 let constr_flags () = {
   Pretyping.use_typeclasses = true;
-  Pretyping.solve_unification_constraints = true;
+  Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
   Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true }
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.mlg
index 2251a66204..e57afe3e33 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.mlg
@@ -14,15 +14,19 @@
 (*                           by Eduardo Gimenez                        *)
 (************************************************************************)
 
+{
+
 open Eqdecide
 open Stdarg
 
+}
+
 DECLARE PLUGIN "ltac_plugin"
 
 TACTIC EXTEND decide_equality
-| [ "decide" "equality" ] -> [ decideEqualityGoal ]
+| [ "decide" "equality" ] -> { decideEqualityGoal }
 END
 
 TACTIC EXTEND compare
-| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
+| [ "compare" constr(c1) constr(c2) ] -> { compare c1 c2 }
 END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 09179dad34..4357689ee2 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -115,7 +115,7 @@ let string_of_genarg_arg (ArgumentType arg) =
   let keyword x = tag_keyword (str x)
   let primitive x = tag_primitive (str x)
 
-  let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with
+  let has_type (Val.Dyn (tag, _)) t = match Val.eq tag t with
   | None -> false
   | Some _ -> true
 
@@ -188,7 +188,7 @@ let string_of_genarg_arg (ArgumentType arg) =
     | AN v -> f v
     | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
 
-  let pr_located pr (loc,x) = pr x
+  let pr_located pr (_,x) = pr x
 
   let pr_evaluable_reference = function
     | EvalVarRef id -> pr_id id
@@ -240,7 +240,7 @@ let string_of_genarg_arg (ArgumentType arg) =
     in
     pr_sequence (fun x -> x) l
 
-  let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
+  let pr_extend_gen pr_gen _ { mltac_name = s; mltac_index = i } l =
       let name =
         str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
         str "@" ++ int i
@@ -260,7 +260,7 @@ let string_of_genarg_arg (ArgumentType arg) =
   | Extend.Uentry tag ->
     let ArgT.Any tag = tag in
     ArgT.repr tag
-  | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl
+  | Extend.Uentryl (_, lvl) -> "tactic" ^ string_of_int lvl
 
   let pr_alias_key key =
     try
@@ -288,7 +288,7 @@ let string_of_genarg_arg (ArgumentType arg) =
       let p = pr_tacarg_using_rule pr_gen prods in
       if pp.pptac_level > lev then surround p else p
     with Not_found ->
-      let pr arg = str "_" in
+      let pr _ = str "_" in
       KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
 
   let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg))
@@ -341,14 +341,14 @@ let string_of_genarg_arg (ArgumentType arg) =
       pr_any_arg pr symb arg
     | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
 
-  let pr_raw_extend_rec prc prlc prtac prpat =
+  let pr_raw_extend_rec prtac =
     pr_extend_gen (pr_farg prtac)
-  let pr_glob_extend_rec prc prlc prtac prpat =
+  let pr_glob_extend_rec prtac =
     pr_extend_gen (pr_farg prtac)
 
-  let pr_raw_alias prc prlc prtac prpat lev key args =
+  let pr_raw_alias prtac lev key args =
     pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
-  let pr_glob_alias prc prlc prtac prpat lev key args =
+  let pr_glob_alias prtac lev key args =
     pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
 
   (**********************************************************************)
@@ -743,7 +743,7 @@ let pr_goal_selector ~toplevel s =
       (* Main tactic printer *)
       and pr_atom1 a = tag_atom a (match a with
         (* Basic tactics *)
-        | TacIntroPattern (ev,[]) as t ->
+        | TacIntroPattern (_,[]) as t ->
           pr_atom0 t
         | TacIntroPattern (ev,(_::_ as p)) ->
            hov 1 (primitive (if ev then "eintros" else "intros") ++
@@ -1054,7 +1054,7 @@ let pr_goal_selector ~toplevel s =
               primitive "fresh" ++ pr_fresh_ids l, latom
             | TacArg(_,TacGeneric arg) ->
               pr.pr_generic arg, latom
-            | TacArg(_,TacCall(loc,(f,[]))) ->
+            | TacArg(_,TacCall(_,(f,[]))) ->
               pr.pr_reference f, latom
             | TacArg(_,TacCall(loc,(f,l))) ->
               pr_with_comments ?loc (hov 1 (
@@ -1112,8 +1112,8 @@ let pr_goal_selector ~toplevel s =
       pr_reference = pr_qualid;
       pr_name = pr_lident;
       pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg);
-      pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
-      pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+      pr_extend = pr_raw_extend_rec pr_raw_tactic_level;
+      pr_alias = pr_raw_alias pr_raw_tactic_level;
     } in
     make_pr_tac
       pr raw_printers
@@ -1142,12 +1142,8 @@ let pr_goal_selector ~toplevel s =
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
         pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg);
-        pr_extend = pr_glob_extend_rec
-          (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
-          prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
-        pr_alias = pr_glob_alias
-          (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
-          prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+        pr_extend = pr_glob_extend_rec prtac;
+        pr_alias = pr_glob_alias prtac;
       } in
       make_pr_tac
         pr glob_printers
@@ -1168,8 +1164,8 @@ let pr_goal_selector ~toplevel s =
         | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
-  let pr_atomic_tactic_level env sigma n t =
-    let prtac n (t:atomic_tactic_expr) =
+  let pr_atomic_tactic_level env sigma t =
+    let prtac (t:atomic_tactic_expr) =
       let pr = {
         pr_tactic = (fun _ _ -> str "<tactic>");
         pr_constr = (fun c -> pr_econstr_env env sigma c);
@@ -1188,18 +1184,15 @@ let pr_goal_selector ~toplevel s =
       in
       pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
     in
-    prtac n t
+    prtac t
 
   let pr_raw_generic = Pputils.pr_raw_generic
 
   let pr_glb_generic = Pputils.pr_glb_generic
 
-  let pr_raw_extend env = pr_raw_extend_rec
-    pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
+  let pr_raw_extend _ = pr_raw_extend_rec pr_raw_tactic_level
 
-  let pr_glob_extend env = pr_glob_extend_rec
-    (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
-    (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+  let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env)
 
   let pr_alias pr lev key args =
     pr_alias_gen (fun _ arg -> pr arg) lev key args
@@ -1207,14 +1200,14 @@ let pr_goal_selector ~toplevel s =
   let pr_extend pr lev ml args =
     pr_extend_gen pr lev ml args
 
-  let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma ltop c
+  let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma c
 
 let declare_extra_genarg_pprule wit
   (f : 'a raw_extra_genarg_printer)
   (g : 'b glob_extra_genarg_printer)
   (h : 'c extra_genarg_printer) =
   begin match wit with
-    | ExtraArg s -> ()
+    | ExtraArg _ -> ()
     | _          -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
   end;
   let f x =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 01c52c413c..9f8cd2fc4e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -409,7 +409,7 @@ module TypeGlobal = struct
 
 
   let inverse env (evd,cstrs) car rel = 
-    let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
+    let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible evd in
       app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
 
 end
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 84baea964e..026c00b849 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -165,8 +165,7 @@ let coerce_var_to_ident fresh env sigma v =
 (* Interprets, if possible, a constr to an identifier which may not
    be fresh but suitable to be given to the fresh tactic. Works for
    vars, constants, inductive, constructors and sorts. *)
-let coerce_to_ident_not_fresh env sigma v =
-let g = sigma in
+let coerce_to_ident_not_fresh sigma v =
 let id_of_name = function
   | Name.Anonymous -> Id.of_string "x"
   | Name.Name x -> x in
@@ -183,9 +182,9 @@ let id_of_name = function
     | Some c ->
        match EConstr.kind sigma c with
        | Var id -> id 
-       | Meta m -> id_of_name (Evd.meta_name g m)
+       | Meta m -> id_of_name (Evd.meta_name sigma m)
        | Evar (kn,_) ->
-        begin match Evd.evar_ident kn g with
+        begin match Evd.evar_ident kn sigma with
         | None -> fail ()
         | Some id -> id
         end
@@ -208,7 +207,7 @@ let id_of_name = function
        | _ -> fail()
 
 
-let coerce_to_intro_pattern env sigma v =
+let coerce_to_intro_pattern sigma v =
   if has_type v (topwit wit_intro_pattern) then
     (out_gen (topwit wit_intro_pattern) v).CAst.v
   else if has_type v (topwit wit_var) then
@@ -221,8 +220,8 @@ let coerce_to_intro_pattern env sigma v =
       IntroNaming (IntroIdentifier (destVar sigma c))
   | _ -> raise (CannotCoerceTo "an introduction pattern")
 
-let coerce_to_intro_pattern_naming env sigma v =
-  match coerce_to_intro_pattern env sigma v with
+let coerce_to_intro_pattern_naming sigma v =
+  match coerce_to_intro_pattern sigma v with
   | IntroNaming pat -> pat
   | _ -> raise (CannotCoerceTo "a naming introduction pattern")
 
@@ -255,7 +254,7 @@ let coerce_to_constr env v =
     (try [], constr_of_id env id with Not_found -> fail ())
   else fail ()
 
-let coerce_to_uconstr env v =
+let coerce_to_uconstr v =
   if has_type v (topwit wit_uconstr) then
     out_gen (topwit wit_uconstr) v
   else
@@ -299,11 +298,11 @@ let coerce_to_constr_list env v =
     List.map map l
   | None -> raise (CannotCoerceTo "a term list")
 
-let coerce_to_intro_pattern_list ?loc env sigma v =
+let coerce_to_intro_pattern_list ?loc sigma v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an intro pattern list")
   | Some l ->
-    let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in
+    let map v = CAst.make ?loc @@ coerce_to_intro_pattern sigma v in
     List.map map l
 
 let coerce_to_hyp env sigma v =
@@ -328,7 +327,7 @@ let coerce_to_hyp_list env sigma v =
   | None -> raise (CannotCoerceTo "a variable list")
 
 (* Interprets a qualified name *)
-let coerce_to_reference env sigma v =
+let coerce_to_reference sigma v =
   match Value.to_constr v with
   | Some c ->
     begin
@@ -356,7 +355,7 @@ let coerce_to_quantified_hypothesis sigma v =
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
-let coerce_to_decl_or_quant_hyp env sigma v =
+let coerce_to_decl_or_quant_hyp sigma v =
   if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
   else
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 56f8816840..d2ae92f6ce 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -51,12 +51,12 @@ val coerce_to_constr_context : Value.t -> constr
 
 val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t
 
-val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t
+val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t
 
-val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
+val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
 
 val coerce_to_intro_pattern_naming :
-  Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
+  Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
 
 val coerce_to_hint_base : Value.t -> string
 
@@ -64,7 +64,7 @@ val coerce_to_int : Value.t -> int
 
 val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders
 
-val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr
+val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr
 
 val coerce_to_closed_constr : Environ.env -> Value.t -> constr
 
@@ -74,17 +74,17 @@ val coerce_to_evaluable_ref :
 val coerce_to_constr_list : Environ.env -> Value.t -> constr list
 
 val coerce_to_intro_pattern_list :
-  ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
+  ?loc:Loc.t -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
 
 val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t
 
 val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list
 
-val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> GlobRef.t
+val coerce_to_reference : Evd.evar_map -> Value.t -> GlobRef.t
 
 val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis
 
-val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis
+val coerce_to_decl_or_quant_hyp : Evd.evar_map -> Value.t -> quantified_hypothesis
 
 val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 876e6f3201..fac464a628 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -554,13 +554,18 @@ let () =
   ] in
   register_grammars_by_name "tactic" entries
 
+let get_identifier id =
+  (** Workaround for badly-designed generic arguments lacking a closure *)
+  Names.Id.of_string_soft ("$" ^ id)
+
+
 type _ ty_sig =
 | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
 | TyIdent : string * 'r ty_sig -> 'r ty_sig
 | TyArg :
-  (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+  ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig
 | TyAnonArg :
-  ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+  ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig
 
 type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
@@ -578,10 +583,11 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol
   fun sign -> match sign with
   | TyNil -> []
   | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig'
-  | TyArg ((loc,(a,id)),sig') ->
-    TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
-  | TyAnonArg ((loc,a),sig') ->
-    TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig'
+  | TyArg (a, id, sig') ->
+    let id = get_identifier id in
+    TacNonTerm (None,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
+  | TyAnonArg (a, sig') ->
+    TacNonTerm (None,(untype_user_symbol a,None)) :: clause_of_sign sig'
 
 let clause_of_ty_ml = function
   | TyML (t,_) -> clause_of_sign t
@@ -604,7 +610,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
       | _ :: _ -> assert false
       end
     | TyIdent (s, sig') -> eval_sign sig' tac
-    | TyArg ((_loc,(a,id)), sig') ->
+    | TyArg (a, _, sig') ->
       let f = eval_sign sig' in
       begin fun tac vals ist -> match vals with
       | [] -> assert false
@@ -612,7 +618,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
         let v' = Taccoerce.Value.cast (topwit (prj a)) v in
         f (tac v') vals ist
       end tac
-    | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac
+    | TyAnonArg (a, sig') -> eval_sign sig' tac
 
 let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function
   | TyML (t,tac) -> eval_sign t tac
@@ -624,14 +630,14 @@ let is_constr_entry = function
 let rec only_constr : type a. a ty_sig -> bool = function
 | TyNil -> true
 | TyIdent(_,_) -> false
-| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false
-| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false
+| TyArg (u, _, s) -> if is_constr_entry u then only_constr s else false
+| TyAnonArg (u, s) -> if is_constr_entry u then only_constr s else false
 
 let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function
 | TyNil -> []
 | TyIdent (_,s) -> mk_sign_vars s
-| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s
-| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s
+| TyArg (_, name, s) -> Name (get_identifier name) :: mk_sign_vars s
+| TyAnonArg (_, s) -> Anonymous :: mk_sign_vars s
 
 let dummy_id = Id.of_string "_"
 
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 2bfbbe2e16..9bba9ba71f 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -72,9 +72,9 @@ type _ ty_sig =
 | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
 | TyIdent : string * 'r ty_sig -> 'r ty_sig
 | TyArg :
-  (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+  ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig
 | TyAnonArg :
-  ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+  ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig
 
 type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9d1cc1643c..d9ac96d894 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -312,11 +312,11 @@ let interp_name ist env sigma = function
   | Name id -> Name (interp_ident ist env sigma id)
 
 let interp_intro_pattern_var loc ist env sigma id =
-  try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id)
+  try try_interp_ltac_var (coerce_to_intro_pattern sigma) ist (Some (env,sigma)) (make ?loc id)
   with Not_found -> IntroNaming (IntroIdentifier id)
 
 let interp_intro_pattern_naming_var loc ist env sigma id =
-  try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id)
+  try try_interp_ltac_var (coerce_to_intro_pattern_naming sigma) ist (Some (env,sigma)) (make ?loc id)
   with Not_found -> IntroIdentifier id
 
 let interp_int ist ({loc;v=id} as locid) =
@@ -357,7 +357,7 @@ let interp_hyp_list ist env sigma l =
 let interp_reference ist env sigma = function
   | ArgArg (_,r) -> r
   | ArgVar {loc;v=id} ->
-    try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id)
+    try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
@@ -451,7 +451,7 @@ let default_fresh_id = Id.of_string "H"
 
 let interp_fresh_id ist env sigma l =
   let extract_ident ist env sigma id =
-    try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma)
+    try try_interp_ltac_var (coerce_to_ident_not_fresh sigma)
                             ist (Some (env,sigma)) (make id)
     with Not_found -> id in
   let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in
@@ -474,7 +474,7 @@ let interp_fresh_id ist env sigma l =
 (* Extract the uconstr list from lfun *)
 let extract_ltac_constr_context ist env sigma =
   let add_uconstr id v map =
-    try Id.Map.add id (coerce_to_uconstr env v) map
+    try Id.Map.add id (coerce_to_uconstr v) map
     with CannotCoerceTo _ -> map
   in
   let add_constr id v map =
@@ -799,7 +799,7 @@ and interp_or_and_intro_pattern ist env sigma = function
 
 and interp_intro_pattern_list_as_list ist env sigma = function
   | [{loc;v=IntroNaming (IntroIdentifier id)}] as l ->
-      (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
+      (try sigma, coerce_to_intro_pattern_list ?loc sigma (Id.Map.find id ist.lfun)
        with Not_found | CannotCoerceTo _ ->
          List.fold_left_map (interp_intro_pattern ist env) sigma l)
   | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l
@@ -842,7 +842,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       try try_interp_ltac_var
-            (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id)
+            (coerce_to_decl_or_quant_hyp sigma) ist (Some (env,sigma)) (make id)
       with Not_found -> NamedHyp id
 
 let interp_binding ist env sigma {loc;v=(b,c)} =
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.mlg
index 81140a46a9..21f0414e9c 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.mlg
@@ -16,70 +16,74 @@
 (*                                                                      *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 open Stdarg
 open Tacarg
 
+}
+
 DECLARE PLUGIN "micromega_plugin"
 
 TACTIC EXTEND RED
-| [ "myred"  ] -> [ Tactics.red_in_concl ]
+| [ "myred"  ] -> { Tactics.red_in_concl }
 END
 
 
 
 TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) tactic(t) ] -> [  (Coq_micromega.psatz_Z i
+| [ "psatz_Z" int_or_var(i) tactic(t) ] -> {  (Coq_micromega.psatz_Z i
                                                (Tacinterp.tactic_of_value ist t))
-                                               ]
-| [ "psatz_Z" tactic(t)] -> [  (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) ]
+                                               }
+| [ "psatz_Z" tactic(t)] -> {  (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) }
 END
 
 TACTIC EXTEND Lia
-[ "xlia" tactic(t) ] -> [   (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) ]
+| [ "xlia" tactic(t) ] -> {   (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND Nia
-[ "xnlia" tactic(t) ] -> [  (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) ]
+| [ "xnlia" tactic(t) ] -> {  (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND NRA
-[ "xnra" tactic(t) ] -> [  (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))]
+| [ "xnra" tactic(t) ] -> {  (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))}
 END
 
 TACTIC EXTEND NQA
-[ "xnqa" tactic(t) ] -> [  (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))]
+| [ "xnqa" tactic(t) ] -> {  (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))}
 END
 
 
   
 TACTIC EXTEND Sos_Z
-| [ "sos_Z" tactic(t) ] -> [ (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) ]
+| [ "sos_Z" tactic(t) ] -> { (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) }
    END
 
 TACTIC EXTEND Sos_Q
-| [ "sos_Q" tactic(t) ] -> [   (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) ]
+| [ "sos_Q" tactic(t) ] -> {   (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) }
    END
 
 TACTIC EXTEND Sos_R
-| [ "sos_R" tactic(t) ] -> [   (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) ]
+| [ "sos_R" tactic(t) ] -> {   (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND LRA_Q
-[ "lra_Q"  tactic(t) ] -> [   (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) ]
+| [ "lra_Q"  tactic(t) ] -> {   (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND LRA_R
-[ "lra_R" tactic(t) ] -> [   (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) ]
+| [ "lra_R" tactic(t) ] -> {   (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) tactic(t) ] -> [   (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) ]
-| [ "psatz_R" tactic(t) ] -> [   (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) ]
+| [ "psatz_R" int_or_var(i) tactic(t) ] -> {   (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_R" tactic(t) ] -> {   (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) tactic(t) ] -> [  (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) ]
-| [ "psatz_Q" tactic(t) ] -> [  (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) ]
+| [ "psatz_Q" int_or_var(i) tactic(t) ] -> {  (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_Q" tactic(t) ] -> {  (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) }
 END
 
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.mlg
index 4ac49adb90..16ff512e8d 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.mlg
@@ -8,11 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 open Stdarg
 
+}
+
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute"  constr(lt) ] -> [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ]
+| [ "nsatz_compute"  constr(lt) ] -> { Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) }
 END
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 6f41388284..e14c4e2ec1 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -38,15 +38,9 @@ open OmegaSolver
 
 (* Added by JCF, 09/03/98 *)
 
-let elim_id id =
-  Proofview.Goal.enter begin fun gl ->
-    simplest_elim (mkVar id)
-  end
-let resolve_id id = Proofview.Goal.enter begin fun gl ->
-  apply (mkVar id)
-end
+let elim_id id = simplest_elim (mkVar id)
 
-let timing timer_name f arg = f arg
+let resolve_id id = apply (mkVar id)
 
 let display_time_flag = ref false
 let display_system_flag = ref false
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.mlg
index 170b937c99..c3d063cff8 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.mlg
@@ -18,6 +18,8 @@
 
 DECLARE PLUGIN "omega_plugin"
 
+{
+
 open Ltac_plugin
 open Names
 open Coq_omega
@@ -43,14 +45,15 @@ let omega_tactic l =
     (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs))
     (omega_solver)
 
+}
 
 TACTIC EXTEND omega
-|  [ "omega" ] -> [ omega_tactic [] ]
+|  [ "omega" ] -> { omega_tactic [] }
 END
 
 TACTIC EXTEND omega'
 | [ "omega" "with" ne_ident_list(l) ] ->
-    [ omega_tactic (List.map Names.Id.to_string l) ]
-| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ]
+    { omega_tactic (List.map Names.Id.to_string l) }
+| [ "omega" "with" "*" ] -> { omega_tactic ["nat";"positive";"N";"Z"] }
 END
 
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.mlg
index 09209dc228..749903c3ad 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 open Names
 open Tacexpr
@@ -16,8 +18,12 @@ open Quote
 open Stdarg
 open Tacarg
 
+}
+
 DECLARE PLUGIN "quote_plugin"
 
+{
+
 let cont = Id.of_string "cont"
 let x = Id.of_string "x"
 
@@ -27,12 +33,14 @@ let make_cont (k : Val.t) (c : EConstr.t) =
   let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
   Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac))
 
+}
+
 TACTIC EXTEND quote
-  [ "quote" ident(f) ] -> [ quote f [] ]
-| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
+| [ "quote" ident(f) ] -> { quote f [] }
+| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc }
 | [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] ->
-  [ gen_quote (make_cont k) c f [] ]
+  { gen_quote (make_cont k) c f [] }
 | [ "quote" ident(f) "[" ne_ident_list(lc) "]"
     "in" constr(c) "using" tactic(k) ] ->
-  [ gen_quote (make_cont k) c f lc ]
+  { gen_quote (make_cont k) c f lc }
 END
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.mlg
index 5b77d08dea..c1ce30027e 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.mlg
@@ -9,6 +9,8 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+{
+
 open Ltac_plugin
 open Names
 open Refl_omega
@@ -39,13 +41,15 @@ let romega_tactic unsafe l =
        (Tactics.intros)
        (total_reflexive_omega_tactic unsafe))
 
+}
+
 TACTIC EXTEND romega
-|  [ "romega" ] -> [ romega_tactic false [] ]
-|  [ "unsafe_romega" ] -> [ romega_tactic true [] ]
+|  [ "romega" ] -> { romega_tactic false [] }
+|  [ "unsafe_romega" ] -> { romega_tactic true [] }
 END
 
 TACTIC EXTEND romega'
 | [ "romega" "with" ne_ident_list(l) ] ->
-    [ romega_tactic false (List.map Names.Id.to_string l) ]
-| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ]
+    { romega_tactic false (List.map Names.Id.to_string l) }
+| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] }
 END
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.mlg
index aa67576348..9c9fdcfa2f 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.mlg
@@ -8,12 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
 
 open Ltac_plugin
 
+}
+
 DECLARE PLUGIN "rtauto_plugin"
 
 TACTIC EXTEND rtauto
-  [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ]
+| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) }
 END