From 99129d2518bd9fe92051aa89138cbb57c839a270 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 28 Feb 2018 09:43:06 +0100
Subject: [ssreflect] Fix module scoping problems due to packing and mli files.

Unfortunately, mli-only files cannot be included in packs, so we have
the weird situation that the scope for `Tacexpr` is wrong. So we
cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the
global namespace instead.

This creates problem when using other modular build/packing strategies
[such as #6857] This could be indeed considered a bug in the OCaml
compiler.

In order to remedy this situation we face two choices:
- leave the module out of the pack (!)
- create an implementation for the module

I chose the second solution as it seems to me like the most sensible
choice.

cc: #6512.
---
 plugins/extraction/extraction_plugin.mlpack |   1 +
 plugins/extraction/miniml.ml                | 222 ++++++++++++++++
 plugins/funind/indfun.ml                    |   2 +-
 plugins/funind/indfun.mli                   |   2 +-
 plugins/ltac/ltac_plugin.mlpack             |   1 +
 plugins/ltac/pptactic.ml                    |   5 +-
 plugins/ltac/pptactic.mli                   |   2 +-
 plugins/ltac/tacexpr.ml                     | 397 ++++++++++++++++++++++++++++
 plugins/setoid_ring/newring_ast.ml          |  67 +++++
 plugins/setoid_ring/newring_ast.mli         |   2 +
 plugins/setoid_ring/newring_plugin.mlpack   |   1 +
 plugins/ssr/ssrparser.mli                   |   2 +
 plugins/ssr/ssrtacticals.mli                |  18 +-
 plugins/ssrmatching/ssrmatching.mli         |   4 +-
 14 files changed, 712 insertions(+), 14 deletions(-)
 create mode 100644 plugins/extraction/miniml.ml
 create mode 100644 plugins/ltac/tacexpr.ml
 create mode 100644 plugins/setoid_ring/newring_ast.ml

(limited to 'plugins')

diff --git a/plugins/extraction/extraction_plugin.mlpack b/plugins/extraction/extraction_plugin.mlpack
index 9184f6501..7f98348e2 100644
--- a/plugins/extraction/extraction_plugin.mlpack
+++ b/plugins/extraction/extraction_plugin.mlpack
@@ -1,3 +1,4 @@
+Miniml
 Table
 Mlutil
 Modutil
diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml
new file mode 100644
index 000000000..e1e49d926
--- /dev/null
+++ b/plugins/extraction/miniml.ml
@@ -0,0 +1,222 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(*s Target language for extraction: a core ML called MiniML. *)
+
+open Names
+open Globnames
+
+(* The [signature] type is used to know how many arguments a CIC
+   object expects, and what these arguments will become in the ML
+   object. *)
+
+(* We eliminate from terms:
+   1) types
+   2) logical parts
+   3) user-declared implicit arguments of a constant of constructor
+*)
+
+type kill_reason =
+  | Ktype
+  | Kprop
+  | Kimplicit of global_reference * int  (* n-th arg of a cst or construct *)
+
+type sign = Keep | Kill of kill_reason
+
+
+(* Convention: outmost lambda/product gives the head of the list. *)
+
+type signature = sign list
+
+(*s ML type expressions. *)
+
+type ml_type =
+  | Tarr    of ml_type * ml_type
+  | Tglob   of global_reference * ml_type list
+  | Tvar    of int
+  | Tvar'   of int (* same as Tvar, used to avoid clash *)
+  | Tmeta   of ml_meta (* used during ML type reconstruction *)
+  | Tdummy  of kill_reason
+  | Tunknown
+  | Taxiom
+
+and ml_meta = { id : int; mutable contents : ml_type option }
+
+(* ML type schema.
+   The integer is the number of variable in the schema. *)
+
+type ml_schema = int * ml_type
+
+(*s ML inductive types. *)
+
+type inductive_kind =
+  | Singleton
+  | Coinductive
+  | Standard
+  | Record of global_reference option list (* None for anonymous field *)
+
+(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
+   If the inductive is logical ([ip_logical = false]), then all other fields
+   are unused. Otherwise,
+   [ip_sign] is a signature concerning the arguments of the inductive,
+   [ip_vars] contains the names of the type variables surviving in ML,
+   [ip_types] contains the ML types of all constructors.
+*)
+
+type ml_ind_packet = {
+  ip_typename : Id.t;
+  ip_consnames : Id.t array;
+  ip_logical : bool;
+  ip_sign : signature;
+  ip_vars : Id.t list;
+  ip_types : (ml_type list) array
+}
+
+(* [ip_nparams] contains the number of parameters. *)
+
+type equiv =
+  | NoEquiv
+  | Equiv of KerName.t
+  | RenEquiv of string
+
+type ml_ind = {
+  ind_kind : inductive_kind;
+  ind_nparams : int;
+  ind_packets : ml_ind_packet array;
+  ind_equiv : equiv
+}
+
+(*s ML terms. *)
+
+type ml_ident =
+  | Dummy
+  | Id of Id.t
+  | Tmp of Id.t
+
+(** We now store some typing information on constructors
+    and cases to avoid type-unsafe optimisations. This will be
+    either the type of the applied constructor or the type
+    of the head of the match.
+*)
+
+(** Nota : the constructor [MLtuple] and the extension of [MLcase]
+    to general patterns have been proposed by P.N. Tollitte for
+    his Relation Extraction plugin. [MLtuple] is currently not
+    used by the main extraction, as well as deep patterns. *)
+
+type ml_branch = ml_ident list * ml_pattern * ml_ast
+
+and ml_ast =
+  | MLrel    of int
+  | MLapp    of ml_ast * ml_ast list
+  | MLlam    of ml_ident * ml_ast
+  | MLletin  of ml_ident * ml_ast * ml_ast
+  | MLglob   of global_reference
+  | MLcons   of ml_type * global_reference * ml_ast list
+  | MLtuple  of ml_ast list
+  | MLcase   of ml_type * ml_ast * ml_branch array
+  | MLfix    of int * Id.t array * ml_ast array
+  | MLexn    of string
+  | MLdummy  of kill_reason
+  | MLaxiom
+  | MLmagic  of ml_ast
+
+and ml_pattern =
+  | Pcons   of global_reference * ml_pattern list
+  | Ptuple  of ml_pattern list
+  | Prel    of int (** Cf. the idents in the branch. [Prel 1] is the last one. *)
+  | Pwild
+  | Pusual  of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
+
+(*s ML declarations. *)
+
+type ml_decl =
+  | Dind  of MutInd.t * ml_ind
+  | Dtype of global_reference * Id.t list * ml_type
+  | Dterm of global_reference * ml_ast * ml_type
+  | Dfix  of global_reference array * ml_ast array * ml_type array
+
+type ml_spec =
+  | Sind  of MutInd.t * ml_ind
+  | Stype of global_reference * Id.t list * ml_type option
+  | Sval  of global_reference * ml_type
+
+type ml_specif =
+  | Spec of ml_spec
+  | Smodule of ml_module_type
+  | Smodtype of ml_module_type
+
+and ml_module_type =
+  | MTident of ModPath.t
+  | MTfunsig of MBId.t * ml_module_type * ml_module_type
+  | MTsig of ModPath.t * ml_module_sig
+  | MTwith of ml_module_type * ml_with_declaration
+
+and ml_with_declaration =
+  | ML_With_type of Id.t list * Id.t list * ml_type
+  | ML_With_module of Id.t list * ModPath.t
+
+and ml_module_sig = (Label.t * ml_specif) list
+
+type ml_structure_elem =
+  | SEdecl of ml_decl
+  | SEmodule of ml_module
+  | SEmodtype of ml_module_type
+
+and ml_module_expr =
+  | MEident of ModPath.t
+  | MEfunctor of MBId.t * ml_module_type * ml_module_expr
+  | MEstruct of ModPath.t * ml_module_structure
+  | MEapply of ml_module_expr * ml_module_expr
+
+and ml_module_structure = (Label.t * ml_structure_elem) list
+
+and ml_module =
+    { ml_mod_expr : ml_module_expr;
+      ml_mod_type : ml_module_type }
+
+(* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp]
+   implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)
+
+type ml_structure = (ModPath.t * ml_module_structure) list
+
+type ml_signature = (ModPath.t * ml_module_sig) list
+
+type unsafe_needs = {
+  mldummy : bool;
+  tdummy : bool;
+  tunknown : bool;
+  magic : bool
+}
+
+type language_descr = {
+  keywords : Id.Set.t;
+
+  (* Concerning the source file *)
+  file_suffix : string;
+  file_naming : ModPath.t -> string;
+  (* the second argument is a comment to add to the preamble *)
+  preamble :
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_struct : ml_structure -> Pp.t;
+
+  (* Concerning a possible interface file *)
+  sig_suffix : string option;
+  (* the second argument is a comment to add to the preamble *)
+  sig_preamble :
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_sig : ml_signature -> Pp.t;
+
+  (* for an isolated declaration print *)
+  pp_decl : ml_decl -> Pp.t;
+
+}
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index b65d9867d..9c350483b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -93,7 +93,7 @@ let functional_induction with_clean c princl pat =
       in
       let encoded_pat_as_patlist =
         List.make (List.length args + List.length c_list - 1) None @ [pat] in
-      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None))
+      List.map2 (fun c pat -> ((None,Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None))
         (args@c_list) encoded_pat_as_patlist
     in
     let princ' = Some (princ,bindings) in
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 93e03852e..dcc1c2ea6 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -14,7 +14,7 @@ val functional_induction :
   bool ->
   EConstr.constr ->
   (EConstr.constr * EConstr.constr bindings) option ->
-  Tacexpr.or_and_intro_pattern option ->
+  Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index 3972b7aac..ec96e1bbd 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -1,3 +1,4 @@
+Tacexpr
 Tacarg
 Tacsubst
 Tacenv
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 5d262ffcb..11bb7a234 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -14,11 +14,9 @@ open Namegen
 open CErrors
 open Util
 open Constrexpr
-open Tacexpr
 open Genarg
 open Geninterp
 open Stdarg
-open Tacarg
 open Libnames
 open Notation_term
 open Misctypes
@@ -29,6 +27,9 @@ open Pputils
 open Ppconstr
 open Printer
 
+open Tacexpr
+open Tacarg
+
 module Tag =
 struct
 
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 7e6c6b20e..5951f2b11 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -17,8 +17,8 @@ open Names
 open Misctypes
 open Environ
 open Constrexpr
-open Tacexpr
 open Notation_term
+open Tacexpr
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
new file mode 100644
index 000000000..8b0c44041
--- /dev/null
+++ b/plugins/ltac/tacexpr.ml
@@ -0,0 +1,397 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Loc
+open Names
+open Constrexpr
+open Libnames
+open Genredexpr
+open Genarg
+open Pattern
+open Misctypes
+open Locus
+
+type ltac_constant = KerName.t
+
+type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
+type lazy_flag =
+  | General (* returns all possible successes *)
+  | Select  (* returns all successes of the first matching branch *)
+  | Once    (* returns the first success in a maching branch
+               (not necessarily the first) *)
+type global_flag = (* [gfail] or [fail] *)
+  | TacGlobal
+  | TacLocal
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
+type rec_flag = bool       (* true = recursive        false = not recursive *)
+type advanced_flag = bool  (* true = advanced         false = basic *)
+type letin_flag = bool     (* true = use local def    false = use Leibniz *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
+type goal_selector = Vernacexpr.goal_selector =
+  | SelectNth of int
+  | SelectList of (int * int) list
+  | SelectId of Id.t
+  | SelectAll
+
+type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
+  | ElimOnConstr of 'a
+  | ElimOnIdent of lident
+  | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+  clear_flag * 'a core_destruction_arg
+
+type inversion_kind = Misctypes.inversion_kind =
+  | SimpleInversion
+  | FullInversion
+  | FullInversionClear
+
+type ('c,'d,'id) inversion_strength =
+  | NonDepInversion of
+      inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
+  | DepInversion of
+      inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option
+  | InversionUsing of 'c * 'id list
+
+type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
+
+type 'id message_token =
+  | MsgString of string
+  | MsgInt of int
+  | MsgIdent of 'id
+
+type ('dconstr,'id) induction_clause =
+    'dconstr with_bindings destruction_arg *
+    (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+    * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
+    * 'id clause_expr option (* in ... *)
+
+type ('constr,'dconstr,'id) induction_clause_list =
+    ('dconstr,'id) induction_clause list
+    * 'constr with_bindings option (* using ... *)
+
+type 'a with_bindings_arg = clear_flag * 'a with_bindings
+
+(* Type of patterns *)
+type 'a match_pattern =
+  | Term of 'a
+  | Subterm of Id.t option * 'a
+
+(* Type of hypotheses for a Match Context rule *)
+type 'a match_context_hyps =
+  | Hyp of lname * 'a match_pattern
+  | Def of lname * 'a match_pattern * 'a match_pattern
+
+(* Type of a Match rule for Match Context and Match *)
+type ('a,'t) match_rule =
+  | Pat of 'a match_context_hyps list * 'a match_pattern * 't
+  | All of 't
+
+(** Extension indentifiers for the TACTIC EXTEND mechanism. *)
+type ml_tactic_name = {
+  (** Name of the plugin where the tactic is defined, typically coming from a
+      DECLARE PLUGIN statement in the source. *)
+  mltac_plugin : string;
+  (** Name of the tactic entry where the tactic is defined, typically found
+      after the TACTIC EXTEND statement in the source. *)
+  mltac_tactic : string;
+}
+
+type ml_tactic_entry = {
+  mltac_name : ml_tactic_name;
+  mltac_index : int;
+}
+
+(** Composite types *)
+
+type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+
+type open_constr_expr = unit * constr_expr
+type open_glob_constr = unit * glob_constr_and_expr
+
+type binding_bound_vars = Constr_matching.binding_bound_vars
+type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern
+
+type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
+
+type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
+
+type delayed_open_constr = EConstr.constr delayed_open
+
+type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
+type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
+type intro_pattern_naming = intro_pattern_naming_expr CAst.t
+
+(** Generic expressions for atomic tactics *)
+
+type 'a gen_atomic_tactic_expr =
+  (* Basic tactics *)
+  | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
+  | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
+      ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+  | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
+  | TacCase of evars_flag * 'trm with_bindings_arg
+  | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
+  | TacMutualCofix of Id.t * (Id.t * 'trm) list
+  | TacAssert of
+      evars_flag * bool * 'tacexpr option option *
+      'dtrm intro_pattern_expr CAst.t option * 'trm
+  | TacGeneralize of ('trm with_occurrences * Name.t) list
+  | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
+      intro_pattern_naming_expr CAst.t option
+
+  (* Derived basic tactics *)
+  | TacInductionDestruct of
+      rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
+
+  (* Conversion *)
+  | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
+  | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+
+  (* Equality and inversion *)
+  | TacRewrite of evars_flag *
+      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+      (* spiwack: using ['dtrm] here is a small hack, may not be
+         stable by a change in the representation of delayed
+         terms. Because, in fact, it is the whole "with_bindings"
+         which is delayed. But because the "t" level for ['dtrm] is
+         uninterpreted, it works fine here too, and avoid more
+         disruption of this file. *)
+      'tacexpr option
+  | TacInversion of ('trm,'dtrm,'nam) inversion_strength * quantified_hypothesis
+
+constraint 'a = <
+    term:'trm;
+    dterm: 'dtrm;
+    pattern:'pat;
+    constant:'cst;
+    reference:'ref;
+    name:'nam;
+    tacexpr:'tacexpr;
+    level:'lev
+>
+
+(** Possible arguments of a tactic definition *)
+
+type 'a gen_tactic_arg =
+  | TacGeneric     of 'lev generic_argument
+  | ConstrMayEval  of ('trm,'cst,'pat) may_eval
+  | Reference      of 'ref
+  | TacCall    of ('ref * 'a gen_tactic_arg list) Loc.located
+  | TacFreshId of string or_var list
+  | Tacexp of 'tacexpr
+  | TacPretype of 'trm
+  | TacNumgoals
+
+constraint 'a = <
+    term:'trm;
+    dterm: 'dtrm;
+    pattern:'pat;
+    constant:'cst;
+    reference:'ref;
+    name:'nam;
+    tacexpr:'tacexpr;
+    level:'lev
+>
+
+(** Generic ltac expressions.
+    't : terms, 'p : patterns, 'c : constants, 'i : inductive,
+    'r : ltac refs, 'n : idents, 'l : levels *)
+
+and 'a gen_tactic_expr =
+  | TacAtom of ('a gen_atomic_tactic_expr) Loc.located
+  | TacThen of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
+  | TacDispatch of
+      'a gen_tactic_expr list
+  | TacExtendTac of
+      'a gen_tactic_expr array *
+      'a gen_tactic_expr *
+      'a gen_tactic_expr array
+  | TacThens of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr list
+  | TacThens3parts of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr array *
+      'a gen_tactic_expr *
+      'a gen_tactic_expr array
+  | TacFirst of 'a gen_tactic_expr list
+  | TacComplete of 'a gen_tactic_expr
+  | TacSolve of 'a gen_tactic_expr list
+  | TacTry of 'a gen_tactic_expr
+  | TacOr of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
+  | TacOnce of
+      'a gen_tactic_expr
+  | TacExactlyOnce of
+      'a gen_tactic_expr
+  | TacIfThenCatch of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
+  | TacOrelse of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
+  | TacDo of int or_var * 'a gen_tactic_expr
+  | TacTimeout of int or_var * 'a gen_tactic_expr
+  | TacTime of string option * 'a gen_tactic_expr
+  | TacRepeat of 'a gen_tactic_expr
+  | TacProgress of 'a gen_tactic_expr
+  | TacShowHyps of 'a gen_tactic_expr
+  | TacAbstract of
+      'a gen_tactic_expr * Id.t option
+  | TacId of 'n message_token list
+  | TacFail of global_flag * int or_var * 'n message_token list
+  | TacInfo of 'a gen_tactic_expr
+  | TacLetIn of rec_flag *
+      (lname * 'a gen_tactic_arg) list *
+      'a gen_tactic_expr
+  | TacMatch of lazy_flag *
+      'a gen_tactic_expr *
+      ('p,'a gen_tactic_expr) match_rule list
+  | TacMatchGoal of lazy_flag * direction_flag *
+      ('p,'a gen_tactic_expr) match_rule list
+  | TacFun of 'a gen_tactic_fun_ast
+  | TacArg of 'a gen_tactic_arg located
+  | TacSelect of goal_selector * 'a gen_tactic_expr
+  (* For ML extensions *)
+  | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
+  (* For syntax extensions *)
+  | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located
+
+constraint 'a = <
+    term:'t;
+    dterm: 'dtrm;
+    pattern:'p;
+    constant:'c;
+    reference:'r;
+    name:'n;
+    tacexpr:'tacexpr;
+    level:'l
+>
+
+and 'a gen_tactic_fun_ast =
+    Name.t list * 'a gen_tactic_expr
+
+constraint 'a = <
+    term:'t;
+    dterm: 'dtrm;
+    pattern:'p;
+    constant:'c;
+    reference:'r;
+    name:'n;
+    tacexpr:'te;
+    level:'l
+>
+
+(** Globalized tactics *)
+
+type g_trm = glob_constr_and_expr
+type g_pat = glob_constr_pattern_and_expr
+type g_cst = evaluable_global_reference and_short_name or_var
+type g_ref = ltac_constant located or_var
+type g_nam = lident
+
+type g_dispatch =  <
+    term:g_trm;
+    dterm:g_trm;
+    pattern:g_pat;
+    constant:g_cst;
+    reference:g_ref;
+    name:g_nam;
+    tacexpr:glob_tactic_expr;
+    level:glevel
+>
+
+and glob_tactic_expr =
+    g_dispatch gen_tactic_expr
+
+type glob_atomic_tactic_expr =
+    g_dispatch gen_atomic_tactic_expr
+
+type glob_tactic_arg =
+    g_dispatch gen_tactic_arg
+
+(** Raw tactics *)
+
+type r_trm = constr_expr
+type r_pat = constr_pattern_expr
+type r_cst = reference or_by_notation
+type r_ref = reference
+type r_nam = lident
+type r_lev = rlevel
+
+type r_dispatch =  <
+    term:r_trm;
+    dterm:r_trm;
+    pattern:r_pat;
+    constant:r_cst;
+    reference:r_ref;
+    name:r_nam;
+    tacexpr:raw_tactic_expr;
+    level:rlevel
+>
+
+and raw_tactic_expr =
+    r_dispatch gen_tactic_expr
+
+type raw_atomic_tactic_expr =
+    r_dispatch gen_atomic_tactic_expr
+
+type raw_tactic_arg =
+    r_dispatch gen_tactic_arg
+
+(** Interpreted tactics *)
+
+type t_trm = EConstr.constr
+type t_pat = constr_pattern
+type t_cst = evaluable_global_reference
+type t_ref = ltac_constant located
+type t_nam = Id.t
+
+type t_dispatch =  <
+    term:t_trm;
+    dterm:g_trm;
+    pattern:t_pat;
+    constant:t_cst;
+    reference:t_ref;
+    name:t_nam;
+    tacexpr:unit;
+    level:tlevel
+>
+
+type atomic_tactic_expr =
+    t_dispatch gen_atomic_tactic_expr
+
+(** Misc *)
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
+type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
+
+(** Traces *)
+
+type ltac_call_kind =
+  | LtacMLCall of glob_tactic_expr
+  | LtacNotationCall of KerName.t
+  | LtacNameCall of ltac_constant
+  | LtacAtomCall of glob_atomic_tactic_expr
+  | LtacVarCall of Id.t * glob_tactic_expr
+  | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map
+
+type ltac_trace = ltac_call_kind Loc.located list
+
+type tacdef_body =
+  | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
+  | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml
new file mode 100644
index 000000000..3eb68b518
--- /dev/null
+++ b/plugins/setoid_ring/newring_ast.ml
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+open Libnames
+open Constrexpr
+
+open Ltac_plugin
+open Tacexpr
+
+type 'constr coeff_spec =
+    Computational of 'constr (* equality test *)
+  | Abstract (* coeffs = Z *)
+  | Morphism of 'constr (* general morphism *)
+
+type cst_tac_spec =
+    CstTac of raw_tactic_expr
+  | Closed of reference list
+
+type 'constr ring_mod =
+    Ring_kind of 'constr coeff_spec
+  | Const_tac of cst_tac_spec
+  | Pre_tac of raw_tactic_expr
+  | Post_tac of raw_tactic_expr
+  | Setoid of constr_expr * constr_expr
+  | Pow_spec of cst_tac_spec * constr_expr
+           (* Syntaxification tactic , correctness lemma *)
+  | Sign_spec of constr_expr
+  | Div_spec of constr_expr
+
+type 'constr field_mod =
+    Ring_mod of 'constr ring_mod
+  | Inject of constr_expr
+
+type ring_info =
+    { ring_carrier : types;
+      ring_req : constr;
+      ring_setoid : constr;
+      ring_ext : constr;
+      ring_morph : constr;
+      ring_th : constr;
+      ring_cst_tac : glob_tactic_expr;
+      ring_pow_tac : glob_tactic_expr;
+      ring_lemma1 : constr;
+      ring_lemma2 : constr;
+      ring_pre_tac : glob_tactic_expr;
+      ring_post_tac : glob_tactic_expr }
+
+type field_info =
+    { field_carrier : types;
+      field_req : constr;
+      field_cst_tac : glob_tactic_expr;
+      field_pow_tac : glob_tactic_expr;
+      field_ok : constr;
+      field_simpl_eq_ok : constr;
+      field_simpl_ok : constr;
+      field_simpl_eq_in_ok : constr;
+      field_cond : constr;
+      field_pre_tac : glob_tactic_expr;
+      field_post_tac : glob_tactic_expr }
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index 226c65125..3eb68b518 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -11,6 +11,8 @@
 open Constr
 open Libnames
 open Constrexpr
+
+open Ltac_plugin
 open Tacexpr
 
 type 'constr coeff_spec =
diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack
index 23663b409..5aa79b586 100644
--- a/plugins/setoid_ring/newring_plugin.mlpack
+++ b/plugins/setoid_ring/newring_plugin.mlpack
@@ -1,2 +1,3 @@
+Newring_ast
 Newring
 G_newring
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 130550388..2ac7c7e26 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -10,6 +10,8 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
+open Ltac_plugin
+
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index 84b184713..a5636ad0f 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -10,21 +10,23 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
+open Ltac_plugin
+open Ssrmatching_plugin
 
 val tclSEQAT :
-  Ltac_plugin.Tacinterp.interp_sign ->
-  Ltac_plugin.Tacinterp.Value.t ->
+  Tacinterp.interp_sign ->
+  Tacinterp.Value.t ->
   Ssrast.ssrdir ->
   int Misctypes.or_var *
-    (('a * Ltac_plugin.Tacinterp.Value.t option list) *
-       Ltac_plugin.Tacinterp.Value.t option) ->
+    (('a * Tacinterp.Value.t option list) *
+       Tacinterp.Value.t option) ->
   Tacmach.tactic
 
 val tclCLAUSES :
   unit Proofview.tactic ->
   (Ssrast.ssrhyps *
      ((Ssrast.ssrhyp_or_id * string) *
-        Ssrmatching_plugin.Ssrmatching.cpattern option)
+        Ssrmatching.cpattern option)
        option)
     list * Ssrast.ssrclseq ->
   unit Proofview.tactic
@@ -34,12 +36,12 @@ val hinttac :
            bool -> bool * Tacinterp.Value.t option list -> Ssrast.v82tac
 
 val ssrdotac :
-  Ltac_plugin.Tacinterp.interp_sign ->
+  Tacinterp.interp_sign ->
   ((int Misctypes.or_var * Ssrast.ssrmmod) *
-     (bool * Ltac_plugin.Tacinterp.Value.t option list)) *
+     (bool * Tacinterp.Value.t option list)) *
     ((Ssrast.ssrhyps *
         ((Ssrast.ssrhyp_or_id * string) *
-           Ssrmatching_plugin.Ssrmatching.cpattern option)
+           Ssrmatching.cpattern option)
           option)
        list * Ssrast.ssrclseq) ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 07d0f9757..c55081e0f 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -3,11 +3,13 @@
 
 open Goal
 open Genarg
-open Tacexpr
 open Environ
 open Evd
 open Constr
 
+open Ltac_plugin
+open Tacexpr
+
 (** ******** Small Scale Reflection pattern matching facilities ************* *)
 
 (** Pattern parsing *)
-- 
cgit v1.2.3