diff options
Diffstat (limited to 'plugins')
231 files changed, 278 insertions, 404 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/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index 2980274487..23b91507c9 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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 39fb8feeb8..1828213227 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 51e2301fe6..e6abf1ccf0 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 eecb7bc983..a43a167e86 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 4e4d42f869..9f53123db1 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 0f5b806644..4934b0750b 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 43b150c346..6ed4672ce3 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 31cbc8e25f..1524079f42 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 3a7e7b837d..690a7c5083 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 445923e01b..df701ed802 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Stdarg (*i camlp4deps: "grammar/grammar.cma" i*) diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index dfdc498638..8c9ec5b9c2 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v index 78ee460856..6de2a92e81 100644 --- a/plugins/extraction/ExtrOcamlBigIntConv.v +++ b/plugins/extraction/ExtrOcamlBigIntConv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v index fcfea352a7..fe6eb7780f 100644 --- a/plugins/extraction/ExtrOcamlIntConv.v +++ b/plugins/extraction/ExtrOcamlIntConv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index e0837be621..01da8401fc 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 80da72d43f..ef4b2bfca6 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index 64ca6c85d0..a0f4b679c2 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index 66f188c84e..84c0eff5da 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index c93cfb9d46..c4f4664092 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v index ab1416b1d6..1374a91abf 100644 --- a/plugins/extraction/Extraction.v +++ b/plugins/extraction/Extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml index 44b81d762c..2bd70ff4d5 100644 --- a/plugins/extraction/big.ml +++ b/plugins/extraction/big.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index e66bf7e1b7..9772ebd641 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 004019e168..d6342b59c6 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 40ef6601d4..39826d7442 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 4f0ed953c6..e10dcd48b6 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 2b7199a763..3661faadab 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i*) -open API open Util open Names open Term diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 26268fb177..e1d43f3405 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 76b435410b..23452febdc 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 4bd207a982..0f537abece 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ (*s Production of Haskell syntax. *) -open API open Pp open CErrors open Util diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli index 6f49320671..f888e71095 100644 --- a/plugins/extraction/haskell.mli +++ b/plugins/extraction/haskell.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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 ec28f49966..be8282da06 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 3a70a50204..a4c2bcd883 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i*) -open API open Util open Names open Libnames @@ -121,7 +120,6 @@ let rec mgu = function mgu (a, a'); mgu (b, b') | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' -> List.iter mgu (List.combine l l') - | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> () | Tdummy _, Tdummy _ -> () | Tvar i, Tvar j when Int.equal i j -> () | Tvar' i, Tvar' j when Int.equal i j -> () @@ -1053,6 +1051,7 @@ let rec simpl o = function | MLmagic(MLcase(typ,e,br)) -> let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in simpl o (MLcase(typ,e,br')) + | MLmagic(MLdummy _ as e) when lang () == Haskell -> e | MLmagic(MLexn _ as e) -> e | a -> ast_map (simpl o) a diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 6924dc9ffe..42d22a7b45 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 6c38813e4b..1e0c331901 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 9a67baa96d..17a6e8db6f 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 16feaf4d6d..9cbc3fd713 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ (*s Production of Ocaml syntax. *) -open API open Pp open CErrors open Util diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli index f579a54b8b..bc9d1889f8 100644 --- a/plugins/extraction/ocaml.mli +++ b/plugins/extraction/ocaml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 55168cc297..1ccc273704 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ (*s Production of Scheme syntax. *) -open API open Pp open CErrors open Util diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli index 5e1ec0d5e0..51647ef4ad 100644 --- a/plugins/extraction/scheme.mli +++ b/plugins/extraction/scheme.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index b82c5257e1..ca98f07e8d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 cfe75bf4e1..2b3007f025 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 314a2b2f96..db1a46a035 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 a31de5e61f..106c469c62 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 139baaeb31..1e7da3250b 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 a5a81bb166..f660ba7343 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 aaf79ae885..d763fe6355 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 92372fe291..1690736305 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 b0e4b2690b..ec2a056e32 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 72ede1f7dd..d6309b057f 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 682047075b..d8d4c1a38a 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 435ca1986e..5ba98fb584 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 e24eca7cb5..0a2e84bb83 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 e1adebe8dc..a1409edd09 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 7f1fb9bd01..d3e8aeee88 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v index a962547131..6e3defabe9 100644 --- a/plugins/fourier/Fourier.v +++ b/plugins/fourier/Fourier.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v index d4b0e2e107..13e0d4369e 100644 --- a/plugins/fourier/Fourier_util.v +++ b/plugins/fourier/Fourier_util.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml index 4919232c98..418859f7f9 100644 --- a/plugins/fourier/fourier.ml +++ b/plugins/fourier/fourier.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index b44307590e..68af1b3b63 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 1960fa8355..682673e8df 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v index e40aea7764..b8a05e5cc0 100644 --- a/plugins/funind/FunInd.v +++ b/plugins/funind/FunInd.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index 64f43b8335..8b4dbbb45c 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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 e70ef23656..5a7ffe0590 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 1258c92868..16d9f200f3 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 94ef2590c8..8dea6c90f5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 ba88563d3b..52a82b0e5e 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 8e12b239e8..d3eccb58d7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 50013f5583..2769802cf4 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 7ecfa57f6d..4cab6ef336 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 7c734cd9af..122aecd75b 100644 --- a/plugins/ltac/evar_tactics.mli +++ b/plugins/ltac/evar_tactics.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 44f33ab806..6097951330 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 b2b3f8b6bb..acdf67779c 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 36df25cc77..f3f2f27e9e 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 c7ec269677..c423585e5e 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 63451210ca..dd24aa3dbf 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 dceefeaa13..5494369022 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 4bab31b85d..2ea0f60ebc 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 18e62a2111..1a2d895868 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 3e6f420065..c874f8d5a3 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 804f734504..d792d4ff7d 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 84c5d3a44f..2c1b1067ea 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 9261a11c71..048dcc8e92 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 8300a55e3d..327b347ec0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 519283759a..1127c98319 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 020b3048f6..32494a8793 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 09fc549c60..52827cb36b 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 83fb6963b8..2b1106ee21 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 fad181c897..bbd7834d58 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 d7f92fd6e3..35205ac58a 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 2c9bf14be2..1bf9ea4c1d 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 e82cb516c0..6c4f3dd873 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 117a16b0af..9e3a54cc86 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 2c02171d0d..1a67f6f888 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 270225e237..cf676f598f 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 c5223052cc..aa8f4efe65 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 14b5e00c72..13b44f0e2c 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 2295852ce3..958109e5a7 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 67893bd11e..64da097deb 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 bc1dd26d92..0554d43641 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 1841ab42bf..b262473a94 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 0cd3ee2f9c..60a8f75ec7 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 a1841afe36..73e4f3d6ab 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 6d33724f1a..180fb2db40 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 2cfe8fac94..5ac3775676 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 53dc800231..5394b1e116 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 6cfaed3053..ef6362270a 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 6dcef414c2..63b8cc4824 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 53dfe22a9c..fdeab8dc4b 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 2817b54a11..dd91944d48 100644 --- a/plugins/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 71f7082e70..01d3f79c74 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr open Hipattern diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v index 7e3ef89293..f205f4f765 100644 --- a/plugins/micromega/Env.v +++ b/plugins/micromega/Env.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 904ee4dac1..56b3d480eb 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 47b6f7c7f9..3d2712658f 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v index acd2751a04..8482c21857 100644 --- a/plugins/micromega/Lqa.v +++ b/plugins/micromega/Lqa.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v index 5b97d8ed36..409eb663bd 100644 --- a/plugins/micromega/Lra.v +++ b/plugins/micromega/Lra.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 95f135c8f0..e5b5854f0a 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v index 72b4dcb6e3..25e4e3c2f8 100644 --- a/plugins/micromega/OrderedRing.v +++ b/plugins/micromega/OrderedRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 8acf0ff882..cabec8fc9b 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index b13285f537..9a1c842b26 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 30e475b710..6b232b4b58 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v index 32ddb3cf4c..9d041397dd 100644 --- a/plugins/micromega/Refl.v +++ b/plugins/micromega/Refl.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index ed49c3df43..e1f99d5768 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index 391231afd9..1b4e576708 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index bd425e6bbf..697af9873a 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 5aa8d03f99..542bfe2a14 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 459c72f9f6..1df895a01b 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index fba1966df3..a4103634e0 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,7 +16,6 @@ (* *) (************************************************************************) -open API open Pp open Mutils open Goptions diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index 2536005ede..a73c1ddb76 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index d803c75549..b15dd7ae66 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,7 +16,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin open Stdarg open Tacarg diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index b4c6d032bf..d65709a1c3 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 0e6d346a3b..49ccb468c1 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index 90a108a3b7..be7ed7fbd4 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/sos.mli b/plugins/micromega/sos.mli index 1ca27ea20a..196a74ae30 100644 --- a/plugins/micromega/sos.mli +++ b/plugins/micromega/sos.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/sos_types.ml b/plugins/micromega/sos_types.ml index 615ac5a2fb..7cce1f8cc3 100644 --- a/plugins/micromega/sos_types.ml +++ b/plugins/micromega/sos_types.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli index 57c4e50cad..29b839cbd9 100644 --- a/plugins/micromega/sos_types.mli +++ b/plugins/micromega/sos_types.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 403f664e2b..d4c6d0dce8 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 5a6d72036e..01c3d79407 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index a120d4efb2..2f1d576394 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/nsatz/ideal.mli b/plugins/nsatz/ideal.mli index b7ec901afa..a667343f10 100644 --- a/plugins/nsatz/ideal.mli +++ b/plugins/nsatz/ideal.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index dd1d8764ab..72934a15d9 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 c0dad72ad6..d6e3071aa3 100644 --- a/plugins/nsatz/nsatz.mli +++ b/plugins/nsatz/nsatz.mli @@ -1,10 +1,9 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API val nsatz_compute : Term.constr -> unit Proofview.tactic diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index dbd9005cbe..609ca62a04 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/nsatz/polynom.mli b/plugins/nsatz/polynom.mli index 433ab5914d..d08337fe91 100644 --- a/plugins/nsatz/polynom.mli +++ b/plugins/nsatz/polynom.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v index 9988c85886..a53a38d35b 100644 --- a/plugins/omega/Omega.v +++ b/plugins/omega/Omega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v index cd1624984e..ce187892d4 100644 --- a/plugins/omega/OmegaPlugin.v +++ b/plugins/omega/OmegaPlugin.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v index cd1624984e..ce187892d4 100644 --- a/plugins/omega/OmegaTactic.v +++ b/plugins/omega/OmegaTactic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 2780be4aaa..8da45e0ad1 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 440a10bfb9..d07b2e0b45 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 2fcf076f11..735af6babc 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,7 +15,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API DECLARE PLUGIN "omega_plugin" diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 2a018fa3f4..6a1efe85b9 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v index 2d154adc57..3fdae95ff9 100644 --- a/plugins/quote/Quote.v +++ b/plugins/quote/Quote.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index c43d7d0b5b..f7ebd3204a 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 15d0f5f37c..e1e73b1c32 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/Bintree.v b/plugins/rtauto/Bintree.v index 3646018719..da540f29fd 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index 0dc6e31b85..f951df26a3 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index 565308f72e..bfa1e5f393 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 8dd7a5e469..43a4107add 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open CErrors open Util open Goptions diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index 31f8e7b51d..e0c09f394c 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index f84eebadce..9f02388c39 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 801fc46067..bec18f6df8 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (* raises Not_found if no proof is found *) -open API type atom_env= {mutable next:int; diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index 5f5b97925f..447acb9057 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v index d639f6085f..37eb5899a8 100644 --- a/plugins/setoid_ring/BinList.v +++ b/plugins/setoid_ring/BinList.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 17a57e62a7..9bc2f6a3ec 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Field.v b/plugins/setoid_ring/Field.v index 73a131398b..607e4799fc 100644 --- a/plugins/setoid_ring/Field.v +++ b/plugins/setoid_ring/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index babbb86a96..eb93e2c0f5 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 2932d379e0..56b985aa34 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 9c690e2b4a..98ffff4322 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v index 54e2789ba4..843b12ad18 100644 --- a/plugins/setoid_ring/NArithRing.v +++ b/plugins/setoid_ring/NArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v index cd3bef4353..8319e84878 100644 --- a/plugins/setoid_ring/Ncring.v +++ b/plugins/setoid_ring/Ncring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 20022c00ec..6596d80c8b 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 109808ee0f..99c7a42c50 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index 5e30a13000..25afeaa7f5 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index 77576cb933..86051e4589 100644 --- a/plugins/setoid_ring/Ring.v +++ b/plugins/setoid_ring/Ring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v index dc7c10cc5f..8a8b46b601 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/plugins/setoid_ring/Ring_base.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index b69196679f..ac54d862c9 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index f7757a18da..8dda5ecd34 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v index 23784cf33f..73b170a7a6 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/plugins/setoid_ring/ZArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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 da21f64ab1..0f996c65aa 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 796b6f43e6..f6300ab7e1 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 5d1412ba76..af64b1479a 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 a3d13c4077..524a5c5221 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 a734681235..06117de79a 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 dfff8d9dfb..af3df28890 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Pp open CErrors open Util |