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/setoid_ring/newring_ast.ml | 67 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)
 create mode 100644 plugins/setoid_ring/newring_ast.ml

(limited to 'plugins/setoid_ring/newring_ast.ml')

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