diff options
Diffstat (limited to 'plugins')
157 files changed, 96 insertions, 222 deletions
diff --git a/plugins/.merlin b/plugins/.merlin new file mode 100644 index 0000000000..dd6678ba09 --- /dev/null +++ b/plugins/.merlin @@ -0,0 +1,2 @@ +REC +FLG -open API diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 00e80d041f..6281b2675e 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,5 +1,3 @@ -open API - let contrib_name = "btauto" let init_constant dir s = diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 3e4febf47c..1828213227 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -10,7 +10,6 @@ (* Downey,Sethi and Tarjan. *) (* Plus some e-matching and constructor handling by P. Corbineau *) -open API open CErrors open Util open Pp diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 1441e13fb3..e6abf1ccf0 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Term open Names diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 4c9ebcfc4d..a43a167e86 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,7 +9,6 @@ (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) -open API open CErrors open Term open Ccalgo diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 0488a5db7c..9f53123db1 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ccalgo open Term diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 4c5d85a5fd..4934b0750b 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -8,7 +8,6 @@ (* This file is the interface between the c-c algorithm and Coq *) -open API open Evd open Names open Inductiveops diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index ef32d2b83e..b4bb62be8e 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -7,7 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open EConstr val proof_tac: Ccproof.proof -> unit Proofview.tactic diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index add3f90b1b..6ed4672ce3 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin open Cctac open Stdarg diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 19d23c0e43..1524079f42 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Context.Named.Declaration let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 7ea64a5288..690a7c5083 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API - (** [start_deriving f suchthat lemma] starts a proof of [suchthat] (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index ce9129bcfe..df701ed802 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Stdarg (*i camlp4deps: "grammar/grammar.cma" i*) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 19ba31fbbd..9772ebd641 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Pp open Util open Names diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 28a7c4d457..d6342b59c6 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Globnames open Miniml diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 79d602dbe8..39826d7442 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Miniml open Term open Declarations @@ -176,26 +175,32 @@ let factor_fix env l cb msb = (hack proposed by Elie) *) -let expand_mexpr env mp me = +let expand_mexpr env mpo me = let inl = Some (Flags.get_inline_level()) in - Mod_typing.translate_mse env (Some mp) inl me + Mod_typing.translate_mse env mpo inl me -(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. - To check with Elie. *) - -let rec mp_of_mexpr = function - | MEident mp -> mp - | MEwith (seb,_) -> mp_of_mexpr seb - | _ -> assert false +let expand_modtype env mp me = + let inl = Some (Flags.get_inline_level()) in + Mod_typing.translate_modtype env mp inl ([],me) let no_delta = Mod_subst.empty_delta_resolver -let env_for_mtb_with_def env mp me idl = +let flatten_modtype env mp me_alg struc_opt = + match struc_opt with + | Some me -> me, no_delta + | None -> + let mtb = expand_modtype env mp me_alg in + mtb.mod_type, mtb.mod_delta + +(** Ad-hoc update of environment, inspired by [Mod_typing.check_with_aux_def]. +*) + +let env_for_mtb_with_def env mp me reso idl = let struc = Modops.destr_nofunctor me in let l = Label.of_id (List.hd idl) in let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in let before = fst (List.split_when spot struc) in - Modops.add_structure mp before no_delta env + Modops.add_structure mp before reso env let make_cst resolver mp l = Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l) @@ -235,20 +240,24 @@ let rec extract_structure_spec env mp reso = function [extract_mexpression_spec] should come from a [mod_type_alg] field. This way, any encountered [MEident] should be a true module type. *) -and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with +and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with | MEident mp -> Visit.add_mp_all mp; MTident mp | MEwith(me',WithDef(idl,(c,ctx)))-> - let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in - let mt = extract_mexpr_spec env mp1 (me_struct,me') in + let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in + let env' = env_for_mtb_with_def env mp1 me_struct delta idl in + let mt = extract_mexpr_spec env mp1 (None,me') in (match extract_with_type env' c with (* cb may contain some kn *) | None -> mt - | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ))) + | Some (vl,typ) -> + type_iter_references Visit.add_ref typ; + MTwith(mt,ML_With_type(idl,vl,typ))) | MEwith(me',WithMod(idl,mp))-> Visit.add_mp_all mp; - MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp)) + MTwith(extract_mexpr_spec env mp1 (None,me'), ML_With_module(idl,mp)) | MEapply _ -> (* No higher-order module type in OCaml : we use the expanded version *) - extract_msignature_spec env mp1 no_delta (*TODO*) me_struct + let me_struct,delta = flatten_modtype env mp1 me_alg me_struct_o in + extract_msignature_spec env mp1 delta me_struct and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with | MoreFunctor (mbid, mtb, me_alg') -> @@ -259,8 +268,8 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with let mp = MPbound mbid in let env' = Modops.add_module_type mp mtb env in MTfunsig (mbid, extract_mbody_spec env mp mtb, - extract_mexpression_spec env' mp1 (me_struct',me_alg')) - | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m) + extract_mexpression_spec env' mp1 (me_struct',me_alg')) + | NoFunctor m -> extract_mexpr_spec env mp1 (Some me_struct,m) and extract_msignature_spec env mp1 reso = function | NoFunctor struc -> @@ -336,7 +345,7 @@ and extract_mexpr env mp = function (* In Haskell/Scheme, we expand everything. For now, we also extract everything, dead code will be removed later (see [Modutil.optimize_struct]. *) - let sign,_,delta,_ = expand_mexpr env mp me in + let sign,_,delta,_ = expand_mexpr env (Some mp) me in extract_msignature env mp delta ~all:true sign | MEident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; @@ -686,3 +695,35 @@ let structure_for_compute c = let struc = optimize_struct (refs,[]) (mono_environment refs []) in let flatstruc = List.map snd (List.flatten (List.map snd struc)) in flatstruc, ast, mlt + +(* For the test-suite : + extraction to a temporary file + run ocamlc on it *) + +let compile f = + try + let args = ["ocamlc";"-I";Filename.dirname f;"-c";f^"i";f] in + let res = CUnix.sys_command (Envars.ocamlfind ()) args in + match res with + | Unix.WEXITED 0 -> () + | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n -> + CErrors.user_err + Pp.(str "Compilation of file " ++ str f ++ + str " failed with exit code " ++ int n) + with Unix.Unix_error (e,_,_) -> + CErrors.user_err + Pp.(str "Compilation of file " ++ str f ++ + str " failed with error " ++ str (Unix.error_message e)) + +let remove f = + if Sys.file_exists f then Sys.remove f + +let extract_and_compile l = + if lang () != Ocaml then + CErrors.user_err (Pp.str "This command only works with OCaml extraction"); + let f = Filename.temp_file "testextraction" ".ml" in + let () = full_extraction (Some f) l in + let () = compile f in + let () = remove f; remove (f^"i") in + let base = Filename.chop_suffix f ".ml" in + let () = remove (base^".cmo"); remove (base^".cmi") in + Feedback.msg_notice (str "Extracted code successfully compiled") diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 0629a84a03..e10dcd48b6 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -8,7 +8,6 @@ (*s This module declares the extraction commands. *) -open API open Names open Libnames open Globnames @@ -18,6 +17,10 @@ val full_extraction : string option -> reference list -> unit val separate_extraction : reference list -> unit val extraction_library : bool -> Id.t -> unit +(* For the test-suite : extraction to a temporary file + ocamlc on it *) + +val extract_and_compile : reference list -> unit + (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index d638c232bb..3661faadab 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -7,7 +7,6 @@ (************************************************************************) (*i*) -open API open Util open Names open Term diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 5ee34103c5..e1d43f3405 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -8,7 +8,6 @@ (*s Extraction from Coq terms to Miniml. *) -open API open Names open Term open Declarations diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 2fa453e533..23452febdc 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,8 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API -open Grammar_API.Pcoq.Prim +open Pcoq.Prim DECLARE PLUGIN "extraction_plugin" @@ -66,6 +65,10 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY (* Monolithic extraction to a file *) | [ "Extraction" string(f) ne_global_list(l) ] -> [ full_extraction (Some f) l ] + +(* Extraction to a temporary file and OCaml compilation *) +| [ "Extraction" "TestCompile" ne_global_list(l) ] + -> [ extract_and_compile l ] END VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 6146f32bbe..0f537abece 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -8,7 +8,6 @@ (*s Production of Haskell syntax. *) -open API open Pp open CErrors open Util diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index 1bf19f186b..e43c47d050 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -1,4 +1,3 @@ -open API open Pp open Util open Names diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index ea966baee6..be8282da06 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -8,7 +8,6 @@ (*s Target language for extraction: a core ML called MiniML. *) -open API open Pp open Names open Globnames diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index f8c846725e..f1bcde2f3f 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -7,7 +7,6 @@ (************************************************************************) (*i*) -open API open Util open Names open Libnames diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 1db96413a8..42d22a7b45 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Globnames open Miniml diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 365dc191ab..1e0c331901 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open ModPath open Globnames @@ -18,10 +17,15 @@ open Mlutil (*S Functions upon ML modules. *) +(** Note: a syntax like [(F M) with ...] is actually legal, see for instance + bug #4720. Hence the code below tries to handle [MTsig], maybe not in + a perfect way, but that should be enough for the use of [se_iter] below. *) + let rec msid_of_mt = function | MTident mp -> mp + | MTsig(mp,_) -> mp | MTwith(mt,_)-> msid_of_mt mt - | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name.") + | MTfunsig _ -> assert false (* A functor cannot be inside a MTwith *) (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) @@ -37,7 +41,7 @@ let se_iter do_decl do_spec do_mp = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in - mt_iter mt; do_decl (Dtype(r,l,t)) + mt_iter mt; do_spec (Stype(r,l,Some t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in let mp_w = diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 1d9db3a5fc..17a6e8db6f 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Globnames open Miniml @@ -18,6 +17,7 @@ val struct_type_search : (ml_type -> bool) -> ml_structure -> bool type do_ref = global_reference -> unit +val type_iter_references : do_ref -> ml_type -> unit val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 2ac411d06f..9cbc3fd713 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -8,7 +8,6 @@ (*s Production of Ocaml syntax. *) -open API open Pp open CErrors open Util diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index bb96489ab0..1ccc273704 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -8,7 +8,6 @@ (*s Production of Scheme syntax. *) -open API open Pp open CErrors open Util diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2642aeefa4..ca98f07e8d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open ModPath open Term @@ -445,9 +444,10 @@ let error_MPfile_as_mod mp b = "Please "^s2^"use (Recursive) Extraction Library instead.\n")) let argnames_of_global r = - let typ = Global.type_of_global_unsafe r in + let env = Global.env () in + let typ, _ = Global.type_of_global_in_context env r in let rels,_ = - decompose_prod (Reduction.whd_all (Global.env ()) typ) in + decompose_prod (Reduction.whd_all env typ) in List.rev_map fst rels let msg_of_implicit = function @@ -878,7 +878,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = Global.type_of_global_unsafe (ConstRef kn) in + let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 0215aa8e48..2b3007f025 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Libnames open Globnames diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 4319fa71cc..db1a46a035 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Hipattern open Names open Term diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 535d757350..106c469c62 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr open Globnames diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 81d714aa26..1e7da3250b 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API -open Grammar_API open Ltac_plugin open Formula open Sequent diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index bd420546ff..f660ba7343 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ltac_plugin open Formula open Sequent diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index e15af1f23c..d763fe6355 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API val ground_tac: unit Proofview.tactic -> ((Sequent.t -> unit Proofview.tactic) -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 4c8b96be1d..1690736305 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Unify open Rules open CErrors diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index c2eb1d68c5..ec2a056e32 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Globnames open Rules diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b0fcd98ccd..d6309b057f 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open CErrors open Util open Names diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 05f60eccc9..d8d4c1a38a 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr open Names diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 6fddaafa32..5ba98fb584 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open EConstr open CErrors open Util diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 2488ffded2..0a2e84bb83 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open EConstr open Formula open Globnames diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 2da3dc768c..a1409edd09 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Term open EConstr diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index cf2ef8ba61..d3e8aeee88 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index a6299c3c49..68af1b3b63 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -12,7 +12,6 @@ des inéquations et équations sont entiers. En attendant la tactique Field. *) -open API open Term open Tactics open Names diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ba46f78aa8..15ab396e31 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,4 +1,3 @@ -open API open Printer open CErrors open Util @@ -957,7 +956,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) let f_def = Global.lookup_constant (fst (destConst evd f)) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in - let f_body = Option.get (Global.body_of_constant_body f_def) in + let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in let f_body = EConstr.of_constr f_body in let params,f_body_with_params = decompose_lam_n evd nb_params f_body in let (_,num),(_,_,bodies) = destFix evd f_body_with_params in @@ -1091,7 +1090,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in let get_body const = match Global.body_of_constant const with - | Some body -> + | Some (body, _) -> Tacred.cbv_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) @@ -1382,7 +1381,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (* Proof of principles of general functions *) -(* let hrec_id = +(* let hrec_id = Recdef.hrec_id *) (* and acc_inv_id = Recdef.acc_inv_id *) (* and ltof_ref = Recdef.ltof_ref *) (* and acc_rel = Recdef.acc_rel *) diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index d03fc475e0..64fbfaeedf 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -1,4 +1,3 @@ -open API open Names val prove_princ_for_struct : diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8ffd15f9fb..513fce2484 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,4 +1,3 @@ -open API open Printer open CErrors open Util @@ -407,7 +406,7 @@ let get_funs_constant mp dp = function const -> let find_constant_body const = match Global.body_of_constant const with - | Some body -> + | Some (body, _) -> let body = Tacred.cbv_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) @@ -651,7 +650,7 @@ let build_case_scheme fa = (* in *) let funs = let (_,f,_) = fa in - try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) + try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index d6ad7ef0d2..5a7ffe0590 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Term open Misctypes diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 56048f92e4..16d9f200f3 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) -open API -open Grammar_API open Ltac_plugin open Util open Pp diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index db2af2be53..379c83b245 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1,4 +1,3 @@ -open API open Printer open Pp open Names diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 7ad7de0792..0cab5a6d35 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -1,4 +1,3 @@ -open API open Names (* diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 726a8203d7..7cb35838c7 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,4 +1,3 @@ -open API open Pp open Glob_term open CErrors diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index b6d2c45437..99a258de98 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,4 +1,3 @@ -open API open Names open Glob_term open Misctypes diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2c5dae1cde..863c9dc8d5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,4 +1,3 @@ -open API open CErrors open Util open Names @@ -851,7 +850,7 @@ let make_graph (f_ref:global_reference) = in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" - | Some body -> + | Some (body, _) -> let env = Global.env () in let sigma = Evd.from_env env in let extern_body,extern_type = diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index fc7da6a338..7a60da44fb 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,4 +1,3 @@ -open API open Misctypes val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6fe6888f3d..f4f9ba2bbb 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -1,4 +1,3 @@ -open API open Names open Pp open Libnames @@ -342,7 +341,7 @@ let pr_info f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr - (Global.type_of_global_unsafe (ConstRef f_info.function_constant)) + (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index f7a9cedd73..5e425cd18a 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -1,4 +1,3 @@ -open API open Names open Pp diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e6f10a880c..8dea6c90f5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ltac_plugin open Declarations open CErrors diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 63662a4437..52a82b0e5e 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -8,7 +8,6 @@ (* Merging of induction principles. *) -open API open Globnames open Tactics open Indfun_common diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1705cac789..d3eccb58d7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API module CVars = Vars @@ -90,7 +89,7 @@ let type_of_const sigma t = |_ -> assert false let constr_of_global x = - fst (Universes.unsafe_constr_of_global x) + fst (Global.constr_of_global_in_context (Global.env ()) x) let constant sl s = constr_of_global (find_reference sl s) diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index f3d5e73320..63bbdbe7e3 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -1,4 +1,3 @@ -open API (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 47fd324f97..2769802cf4 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Util open Locus open Misctypes diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 4342f5b5e1..4cab6ef336 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open Term diff --git a/plugins/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli index 0658008c00..122aecd75b 100644 --- a/plugins/ltac/evar_tactics.mli +++ b/plugins/ltac/evar_tactics.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Tacexpr open Locus diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index af1d349db2..6097951330 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index e5a2d003a5..acdf67779c 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API -open Grammar_API open Tacexpr open Names open Constrexpr diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index e56b510be0..f3f2f27e9e 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index fe90f633f2..c423585e5e 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API val discrHyp : Names.Id.t -> unit Proofview.tactic val injHyp : Names.Id.t -> unit Proofview.tactic diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 6145e373b1..301943a509 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 946b99f6c0..dd24aa3dbf 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Class_tactics open Stdarg open Tacarg diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index a7c05664f5..5494369022 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -14,7 +14,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Eqdecide DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index cf6bd98b38..2ea0f60ebc 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -8,9 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API -open Grammar_API - DECLARE PLUGIN "ltac_plugin" open Util @@ -433,7 +430,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false VERNAC tactic_mode EXTEND VernacSolve | [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => [ classify_as_proofstep ] -> [ - let g = Option.default (Proof_global.get_default_goal_selector ()) g in + let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in vernac_solve g n t def ] | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index a2e8fc270d..1a2d895868 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,8 +12,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -open API -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 8956e21b93..c874f8d5a3 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -10,8 +10,6 @@ (* Syntax for rewriting with strategies *) -open API -open Grammar_API open Names open Misctypes open Locus diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 49af905d89..d792d4ff7d 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API -open Grammar_API open Pp open CErrors open Util diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 898c1d1c31..2c1b1067ea 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API -open Grammar_API open Pcoq (* Main entry for extensions *) diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 782d13a38d..048dcc8e92 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -8,8 +8,6 @@ (** Ltac parsing entries *) -open API -open Grammar_API open Loc open Names open Pcoq diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 8d8e82c7ce..327b347ec0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Pp open Names open Namegen diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index c15225ebfc..1127c98319 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -9,7 +9,6 @@ (** This module implements pretty-printers for tactic_expr syntactic objects and their subcomponents. *) -open API open Pp open Genarg open Geninterp diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index e25f1926d5..32494a8793 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Unicode open Pp open Printer diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index eb4146cfc1..52827cb36b 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (** Ltac profiling primitives *) diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 9f171cee66..2b1106ee21 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -10,7 +10,6 @@ (** Ltac profiling entrypoints *) -open API open Profile_ltac open Stdarg diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3a77f34a1c..bbd7834d58 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Pp open CErrors diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 73e309cc21..35205ac58a 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Environ open EConstr diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 610a722fb1..1bf9ea4c1d 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -8,7 +8,6 @@ (** Generic arguments based on Ltac. *) -open API open Genarg open Geninterp open Tacexpr diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 4c3687ec75..6c4f3dd873 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Genarg open Tacexpr open Constrexpr diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index bdfa6d9896..9e3a54cc86 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open Term diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index ab46455c82..1a67f6f888 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open EConstr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index c6b4feba1c..cf676f598f 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API -open Grammar_API open Pp open CErrors open Util diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 9980e0961a..aa8f4efe65 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -8,8 +8,6 @@ (** Ltac toplevel command entries. *) -open API -open Grammar_API open Vernacexpr open Tacexpr diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 58d1766ff7..13b44f0e2c 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Pp open Names diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 23e12bfc0d..958109e5a7 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Tacexpr open Geninterp diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 471320684d..64da097deb 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Loc open Names open Constrexpr diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index c3e39ec11a..0554d43641 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API -open Grammar_API open Pattern open Pp open Genredexpr diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 4749017e16..b262473a94 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API -open Grammar_API open Pp open Names open Tacexpr diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index bad3e774de..60a8f75ec7 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API -open Grammar_API open Constrintern open Patternops open Pp diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index ab94e21f0a..73e4f3d6ab 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Tactic_debug open EConstr diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 750843c9d0..180fb2db40 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API -open Grammar_API open Util open Tacexpr open Mod_subst diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index c401e67f11..5ac3775676 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Tacexpr open Mod_subst open Genarg diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 9113b620f0..5394b1e116 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open Pp diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 469c6bdbca..ef6362270a 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Environ open Pattern open Names diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 3e96680729..63b8cc4824 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -9,7 +9,6 @@ (** This file extends Matching with the main logic for Ltac's (lazy)match and (lazy)match goal. *) -open API open Names open Tacexpr open Context.Named.Declaration diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 304eec463e..01334d36c9 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (** This file extends Matching with the main logic for Ltac's (lazy)match and (lazy)match goal. *) diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index 5b95e9c778..fdeab8dc4b 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Libobject open Pp diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli index dc3bbf7d69..dd91944d48 100644 --- a/plugins/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Tacexpr open Vernacexpr diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index e809d87dc7..01d3f79c74 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr open Hipattern diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a662f8bad4..a4103634e0 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -16,7 +16,6 @@ (* *) (************************************************************************) -open API open Pp open Mutils open Goptions diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 37a21cd592..b15dd7ae66 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,7 +16,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin open Stdarg open Tacarg diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 261f3dab40..01c3d79407 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 7e63b916d3..72934a15d9 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open CErrors open Util open Term diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli index b692522f2f..d6e3071aa3 100644 --- a/plugins/nsatz/nsatz.mli +++ b/plugins/nsatz/nsatz.mli @@ -6,5 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API val nsatz_compute : Term.constr -> unit Proofview.tactic diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 3badb92f59..d07b2e0b45 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -13,7 +13,6 @@ (* *) (**************************************************************************) -open API open CErrors open Util open Names diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 8d24027d88..735af6babc 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -15,7 +15,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API DECLARE PLUGIN "omega_plugin" diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 88076dca9e..f7ebd3204a 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin open Names open Misctypes diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 8ee5ce8b1e..e1e73b1c32 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -101,7 +101,6 @@ (*i*) -open API open CErrors open Util open Names diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 06c80a8256..4ffbd5aa8b 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -6,7 +6,6 @@ *************************************************************************) -open API open Names let module_refl_name = "ReflOmegaCore" diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index 6dc5d9f7e5..a452b1a917 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -6,7 +6,6 @@ *************************************************************************) -open API (** Coq objects used in romega *) diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 53f6f42c8e..5fd9c94194 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API DECLARE PLUGIN "romega_plugin" diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 60e6e7de79..517df41d93 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -6,7 +6,6 @@ *************************************************************************) -open API open Pp open Util open Const_omega diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index 69a2043f64..bfa1e5f393 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (*i camlp4deps: "grammar/grammar.cma" i*) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 1158817d62..43a4107add 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open CErrors open Util open Goptions diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 944e0ac5e7..9f02388c39 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API module Search = Explore.Make(Proof_search) diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 080dcdac27..bec18f6df8 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -7,7 +7,6 @@ (************************************************************************) (* raises Not_found if no proof is found *) -open API type atom_env= {mutable next:int; diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index ada41274fa..05ab8ab326 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API -open Grammar_API open Ltac_plugin open Pp open Util diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 955cc767c7..0f996c65aa 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ltac_plugin open Pp open Util diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 7f685063c4..d9d32c681d 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open EConstr open Libnames diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index b7afd2effc..d37582bd79 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open Libnames open Constrexpr diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 94eaa1d6aa..cdd4ee6459 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Ltac_plugin diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index 3988f00bad..cc0e86684e 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Printer open Pretyping open Globnames diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index 20a1263d24..af9f7491ad 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 411ce6853c..799e969ae2 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API -open Grammar_API open Util open Names open Evd diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index f611685769..4b045e989a 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Tacmach open Names open Environ diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index bd9a05891a..832044909c 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Util open Names open Printer diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index 825b4758e3..66e202b48f 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrmatching_plugin val ssrelim : diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index b0fe898975..ab6a60f4ee 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ltac_plugin open Util open Names diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index f9ab5d74fe..a3366887fb 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrmatching_plugin open Ssrast diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 660c2e776c..8e6329a15e 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Tacmach diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 7f254074c7..e5b5b58fff 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Ltac_plugin diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 06bbd749e6..023778fdbf 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Pp open Term diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index aefdc8e111..6c36e67e83 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrmatching_plugin open Ssrast open Ssrcommon diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 09917339a7..ce23bb2b30 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API -open Grammar_API open Names open Pp open Pcoq diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 1548206666..bf6f44f11d 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -8,9 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API -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/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 427109c1b2..e865ef706d 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Pp open Names open Printer diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 8da9bc72bc..5c68872b75 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrast val pp_term : diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index b586d05e1c..5e43c83749 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Termops open Tacmach diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index 297cfdfdc0..c1f65a31e9 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API val tclSEQAT : Ltac_plugin.Tacinterp.interp_sign -> diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 4c8827bf84..9c59d83d4e 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API -open Grammar_API open Names open Term open Termops @@ -337,7 +335,8 @@ let coerce_search_pattern_to_sort hpat = Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = - Reductionops.splay_prod env sigma (EConstr.of_constr (Universes.unsafe_type_of_global hr)) in + let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in + Reductionops.splay_prod env sigma (EConstr.of_constr hr) in let np = List.length dc in if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index cc142e091c..338ecccc2d 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Util open Names open Term diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index 8a7bd5d6e7..6fd906ff4f 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrast open Ssrcommon diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 7674a8dde6..f6300ab7e1 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -8,9 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API -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 1853bc35dc..65ea76d161 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,8 +1,6 @@ (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -open API -open Grammar_API open Goal open Genarg open Tacexpr diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 6bf5b8cfca..c41ec39cb4 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "ascii_syntax_plugin" diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index fe1eef866c..af64b1479a 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "int31_syntax_plugin" diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index c6ee899ed7..524a5c5221 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "nat_syntax_plugin" diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 9cfa50071e..06117de79a 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open Globnames diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index a4335a508b..b7f13b0400 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open API open Globnames open Ascii_syntax_plugin.Ascii_syntax open Glob_term diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 719d8b1ccb..af3df28890 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Pp open CErrors open Util |