diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 14:47:40 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 14:47:40 +0200 |
commit | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (patch) | |
tree | c8857eb4007122038c432121fd331c69bc243821 /plugins | |
parent | 777751427cbe02ac8a0384d1173f9ef3cce0c8fd (diff) | |
parent | ae325798c95bd43126e72ce71a7e76e4bee69d3e (diff) |
Merge PR #905: [api] Remove type equalities from API.
Diffstat (limited to 'plugins')
26 files changed, 1 insertions, 29 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index dba1e3444..23452febd 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API.Pcoq.Prim +open Pcoq.Prim DECLARE PLUGIN "extraction_plugin" diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index c001ee382..1e7da3250 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Ltac_plugin open Formula open Sequent diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index c495703ee..16d9f200f 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Ltac_plugin open Util open Pp diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 72c6f9090..609795133 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 419c5e8c4..acdf67779 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Tacexpr open Names open Constrexpr diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 6d80ab549..f3f2f27e9 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 4d13d89a4..301943a50 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index cc052c8a2..2ea0f60eb 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API - DECLARE PLUGIN "ltac_plugin" open Util diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 1935d560a..1a2d89586 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,7 +12,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -open Grammar_API open Libnames open Constrexpr open Constrexpr_ops diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 3c27b2747..c874f8d5a 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -10,7 +10,6 @@ (* Syntax for rewriting with strategies *) -open Grammar_API open Names open Misctypes open Locus diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index e539b5867..d792d4ff7 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pp open CErrors open Util diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 2adcf02e6..2c1b1067e 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pcoq (* Main entry for extensions *) diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 794cb527f..048dcc8e9 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -8,7 +8,6 @@ (** Ltac parsing entries *) -open Grammar_API open Loc open Names open Pcoq diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 791b7f48d..cf676f598 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pp open CErrors open Util diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index ccd44b914..aa8f4efe6 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -8,7 +8,6 @@ (** Ltac toplevel command entries. *) -open Grammar_API open Vernacexpr open Tacexpr diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index df03c7b47..0554d4364 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pattern open Pp open Genredexpr diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index ad2e70908..b262473a9 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pp open Names open Tacexpr diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 7b054947b..60a8f75ec 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Constrintern open Patternops open Pp diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index c1ca85433..180fb2db4 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Util open Tacexpr open Mod_subst diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 6c82346bc..05ab8ab32 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Ltac_plugin open Pp open Util diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 608b778e4..799e969ae 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API open Util open Names open Evd diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 228444b82..ce23bb2b3 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API open Names open Pp open Pcoq diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index c93e10405..bf6f44f11 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API - 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 -> (int * Ppextend.parenRelation -> 'c) -> 'c diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index fbe3cd2b9..9c59d83d4 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API open Names open Term open Termops diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 74519f6c5..f6300ab7e 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API - (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 0c09d7bfb..65ea76d16 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,7 +1,6 @@ (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -open Grammar_API open Goal open Genarg open Tacexpr |