diff options
| author | Maxime Dénès | 2017-03-24 16:15:32 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-24 16:15:32 +0100 |
| commit | af291869bb7d1184d8e655906572d75937ca829b (patch) | |
| tree | 62a5ccf9ee7b115b7d1118cbc3db92c553261713 /plugins/decl_mode | |
| parent | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff) | |
| parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) | |
Merge branch 'trunk' into pr379
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 1 |
4 files changed, 4 insertions, 0 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 828d634d0c..3aa5725295 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open CErrors open Util open Names diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 4fe59d755e..2ea4538c31 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open CErrors open Util open Pp diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 18a35c6cfb..a71d20f0dc 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -10,6 +10,7 @@ DECLARE PLUGIN "decl_mode_plugin" +open Ltac_plugin open Compat open Pp open Decl_expr diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 93b98263e6..92045e775b 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open CErrors open Pp open Decl_expr |