diff options
46 files changed, 203 insertions, 76 deletions
diff --git a/appveyor.yml b/appveyor.yml index cd3b88d007..c9c6bc0684 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -1,6 +1,10 @@ version: '{branch}~{build}' clone_depth: 10 +cache: + - C:\cygwin64 -> dev\ci\appveyor.bat + - C:\cygwin64\home\appveyor\.opam -> dev\ci\appveyor.sh + platform: - x64 diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6b22261a15..c03a5fee90 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -120,6 +120,9 @@ type internalization_error = | UnboundFixName of bool * Id.t | NonLinearPattern of Id.t | BadPatternsNumber of int * int + | NotAProjection of qualid + | NotAProjectionOf of qualid * qualid + | ProjectionsOfDifferentRecords of qualid * qualid exception InternalizationError of internalization_error Loc.located @@ -145,6 +148,16 @@ let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 +let explain_field_not_a_projection field_id = + pr_qualid field_id ++ str ": Not a projection" + +let explain_field_not_a_projection_of field_id inductive_id = + pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id + +let explain_projections_of_diff_records inductive1_id inductive2_id = + str "This record contains fields of both " ++ pr_qualid inductive1_id ++ + str " and " ++ pr_qualid inductive2_id + let explain_internalization_error e = let pp = match e with | VariableCapture (id,id') -> explain_variable_capture id id' @@ -153,6 +166,11 @@ let explain_internalization_error e = | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id | NonLinearPattern id -> explain_non_linear_pattern id | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 + | NotAProjection field_id -> explain_field_not_a_projection field_id + | NotAProjectionOf (field_id, inductive_id) -> + explain_field_not_a_projection_of field_id inductive_id + | ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) -> + explain_projections_of_diff_records inductive1_id inductive2_id in pp ++ str "." let error_bad_inductive_type ?loc = @@ -1281,6 +1299,10 @@ let check_duplicate loc fields = user_err ?loc (str "This record defines several times the field " ++ pr_qualid r ++ str ".") +let inductive_of_record loc record = + let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in + Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive + (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] are fields of a record and [e1] are "values" (either terms, when @@ -1303,8 +1325,7 @@ let sort_fields ~complete loc fields completer = let gr = global_reference_of_reference first_field_ref in (gr, Recordops.find_projection gr) with Not_found -> - user_err ?loc ~hdr:"intern" - (pr_qualid first_field_ref ++ str": Not a projection") + raise (InternalizationError(loc, NotAProjection first_field_ref)) in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in @@ -1363,12 +1384,18 @@ let sort_fields ~complete loc fields completer = with Not_found -> user_err ?loc ~hdr:"intern" (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in + let this_field_record = try Recordops.find_projection field_glob_ref + with Not_found -> + let inductive_ref = inductive_of_record loc record in + raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref))) + in let remaining_projs, (field_index, _) = let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in try CList.extract_first the_proj remaining_projs with Not_found -> - user_err ?loc - (str "This record contains fields of different records.") + let ind1 = inductive_of_record loc record in + let ind2 = inductive_of_record loc this_field_record in + raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2))) in index_fields fields remaining_projs ((field_index, field_value) :: acc) | [] -> diff --git a/kernel/names.ml b/kernel/names.ml index 7cd749de1d..18560d5f8d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -872,6 +872,8 @@ struct let equal (c, b) (c', b') = Repr.equal c c' && b == b' + let repr_equal p p' = Repr.equal (repr p) (repr p') + let hash (c, b) = (if b then 0 else 1) + Repr.hash c module SyntacticOrd = struct diff --git a/kernel/names.mli b/kernel/names.mli index 37930c12e2..98995752a2 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -608,6 +608,9 @@ module Projection : sig val hcons : t -> t (** Hashconsing of projections. *) + val repr_equal : t -> t -> bool + (** Ignoring the unfolding boolean. *) + val compare : t -> t -> int val map : (MutInd.t -> MutInd.t) -> t -> t diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index c2bcd73fff..d0b01453a0 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -29,6 +29,7 @@ type project = { v_files : string sourced list; mli_files : string sourced list; ml4_files : string sourced list; + mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; mlpack_files : string sourced list; @@ -66,6 +67,7 @@ let mk_project project_file makefile install_kind use_ocamlopt = { v_files = []; mli_files = []; ml4_files = []; + mlg_files = []; ml_files = []; mllib_files = []; mlpack_files = []; @@ -223,6 +225,7 @@ let process_cmd_line orig_dir proj args = { proj with v_files = proj.v_files @ [sourced f] } | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } + | ".mlg" -> { proj with mlg_files = proj.mlg_files @ [sourced f] } | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] } @@ -249,9 +252,9 @@ let rec find_project_file ~from ~projfile_name = else find_project_file ~from:newdir ~projfile_name ;; -let all_files { v_files; ml_files; mli_files; ml4_files; +let all_files { v_files; ml_files; mli_files; ml4_files; mlg_files; mllib_files; mlpack_files } = - v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files + v_files @ mli_files @ ml4_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files let map_sourced_list f l = List.map (fun x -> f x.thing) l ;; diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 5780bb5d78..2a6a09a9a0 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -23,6 +23,7 @@ type project = { v_files : string sourced list; mli_files : string sourced list; ml4_files : string sourced list; + mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; mlpack_files : string sourced list; diff --git a/library/coqlib.ml b/library/coqlib.ml index a044a9a395..784360dc8a 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -227,8 +227,7 @@ type coq_eq_data = { (* Leibniz equality on Type *) -let build_eqdata_gen lib str = - let _ = check_required_library lib in { +let build_eqdata_gen str = { eq = lib_ref ("core." ^ str ^ ".type"); ind = lib_ref ("core." ^ str ^ ".ind"); refl = lib_ref ("core." ^ str ^ ".refl"); @@ -237,9 +236,9 @@ let build_eqdata_gen lib str = congr = lib_ref ("core." ^ str ^ ".congr"); } -let build_coq_eq_data () = build_eqdata_gen logic_module_name "eq" -let build_coq_jmeq_data () = build_eqdata_gen jmeq_module_name "JMeq" -let build_coq_identity_data () = build_eqdata_gen datatypes_module_name "identity" +let build_coq_eq_data () = build_eqdata_gen "eq" +let build_coq_jmeq_data () = build_eqdata_gen "JMeq" +let build_coq_identity_data () = build_eqdata_gen "identity" (* Inversion data... *) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 70a2a30cd5..a284c3bfc7 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -730,13 +730,10 @@ let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project (** look up a name in the ssreflect internals module *) let ssrdirpath = DirPath.make [Id.of_string "ssreflect"] let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name) -let ssrtopqid name = Libnames.qualid_of_ident (Id.of_string name) -let locate_reference qid = - Smartlocate.global_of_extended_global (Nametab.locate_extended qid) let mkSsrRef name = - try locate_reference (ssrqid name) with Not_found -> - try locate_reference (ssrtopqid name) with Not_found -> - CErrors.user_err (Pp.str "Small scale reflection library not loaded") + let qn = Format.sprintf "plugins.ssreflect.%s" name in + if Coqlib.has_ref qn then Coqlib.lib_ref qn else + CErrors.user_err Pp.(str "Small scale reflection library not loaded (" ++ str name ++ str ")") let mkSsrRRef name = (DAst.make @@ GRef (mkSsrRef name,None)), None let mkSsrConst name env sigma = EConstr.fresh_global env sigma (mkSsrRef name) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 9ba23467e7..566a933522 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -212,8 +212,7 @@ val pf_abs_prod : EConstr.t -> Goal.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option -val mkSsrRef : string -> GlobRef.t -val mkSsrConst : +val mkSsrConst : string -> env -> evar_map -> evar_map * EConstr.t val pf_mkSsrConst : diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 460bdc6d23..e43cab094b 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -159,6 +159,10 @@ Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) := Notation "<hidden n >" := (abstract _ n _). Notation "T (* n *)" := (abstract T n abstract_key). +Register abstract_lock as plugins.ssreflect.abstract_lock. +Register abstract_key as plugins.ssreflect.abstract_key. +Register abstract as plugins.ssreflect.abstract. + (* Constants for tactic-views *) Inductive external_view : Type := tactic_view of Type. @@ -287,6 +291,8 @@ Variant phant (p : Type) := Phant. Definition protect_term (A : Type) (x : A) : A := x. +Register protect_term as plugins.ssreflect.protect_term. + (* The ssreflect idiom for a non-keyed pattern: *) (* - unkeyed t wiil match any subterm that unifies with t, regardless of *) (* whether it displays the same head symbol as t. *) @@ -336,6 +342,9 @@ Notation nosimpl t := (let: tt := tt in t). Lemma master_key : unit. Proof. exact tt. Qed. Definition locked A := let: tt := master_key in fun x : A => x. +Register master_key as plugins.ssreflect.master_key. +Register locked as plugins.ssreflect.locked. + Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed. (* Needed for locked predicates, in particular for eqType's. *) @@ -395,12 +404,18 @@ Definition ssr_have_let Pgoal Plemma step (rest : let x : Plemma := step in Pgoal) : Pgoal := rest. Arguments ssr_have_let [Pgoal]. +Register ssr_have as plugins.ssreflect.ssr_have. +Register ssr_have_let as plugins.ssreflect.ssr_have_let. + Definition ssr_suff Plemma Pgoal step (rest : Plemma) : Pgoal := step rest. Arguments ssr_suff Plemma [Pgoal]. Definition ssr_wlog := ssr_suff. Arguments ssr_wlog Plemma [Pgoal]. +Register ssr_suff as plugins.ssreflect.ssr_suff. +Register ssr_wlog as plugins.ssreflect.ssr_wlog. + (* Internal N-ary congruence lemmas for the congr tactic. *) Fixpoint nary_congruence_statement (n : nat) @@ -425,6 +440,9 @@ Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. Proof. by move->. Qed. Arguments ssr_congr_arrow : clear implicits. +Register nary_congruence as plugins.ssreflect.nary_congruence. +Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow. + (* View lemmas that don't use reflection. *) Section ApplyIff. diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 7f9a9e125e..5067d8af31 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -16,7 +16,6 @@ open Printer open Term open Constr open Termops -open Globnames open Tactypes open Tacmach @@ -98,6 +97,11 @@ let subgoals_tys sigma (relctx, concl) = * generalize the equality in case eqid is not None * 4. build the tactic handle intructions and clears as required in ipats and * by eqid *) + +let get_eq_type gl = + let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in + gl, EConstr.of_constr eq + let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac gl = (* some sanity checks *) let oc, orig_clr, occ, c_gen, gl = match what with @@ -115,8 +119,6 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM=="))); let fire_subst gl t = Reductionops.nf_evar (project gl) t in - let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in - let eq = EConstr.of_constr eq in let is_undef_pat = function | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t) | _ -> false in @@ -322,6 +324,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let k = List.length deps in let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in let gl, t = pfe_type_of gl c in + let gl, eq = get_eq_type gl in let gen_eq_tac, gl = let refl = EConstr.mkApp (eq, [|t; c; c|]) in let new_concl = EConstr.mkArrow refl (EConstr.Vars.lift 1 (pf_concl orig_gl)) in @@ -421,7 +424,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with let is_injection_case c gl = let gl, cty = pfe_type_of gl c in let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in - GlobRef.equal (IndRef mind) Coqlib.(lib_ref "core.eq.type") + Coqlib.check_ind_ref "core.eq.type" mind let perform_injection c gl = let gl, cty = pfe_type_of gl c in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f0ff1aa93b..6a75be352b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -711,8 +711,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in ise_try evd [f1; f2] - | Proj (p, c), Proj (p', c') - when Constant.equal (Projection.constant p) (Projection.constant p') -> + | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' -> let f1 i = ise_and i [(fun i -> evar_conv_x ts env i CONV c c'); diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5dbe95a471..367a48cb5e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -398,8 +398,7 @@ struct match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> Constant.equal c1 c2 && Univ.Instance.equal u1 u2 - | Cst_proj p1, Cst_proj p2 -> - Constant.equal (Projection.constant p1) (Projection.constant p2) + | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2 | _, _ -> false in let rec equal_rec sk1 sk2 = diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject index 53dc963997..ed31a58247 100644 --- a/test-suite/coq-makefile/arg/_CoqProject +++ b/test-suite/coq-makefile/arg/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject index 4f44bde22a..1f914a71b0 100644 --- a/test-suite/coq-makefile/compat-subdirs/_CoqProject +++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc1/_CoqProject b/test-suite/coq-makefile/coqdoc1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/coqdoc1/_CoqProject +++ b/test-suite/coq-makefile/coqdoc1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/coqdoc2/_CoqProject +++ b/test-suite/coq-makefile/coqdoc2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject index 5678a8edbb..3133342f6c 100644 --- a/test-suite/coq-makefile/emptyprefix/_CoqProject +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/extend-subdirs/_CoqProject b/test-suite/coq-makefile/extend-subdirs/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/extend-subdirs/_CoqProject +++ b/test-suite/coq-makefile/extend-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/findlib-package/_CoqProject +++ b/test-suite/coq-makefile/findlib-package/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/latex1/_CoqProject b/test-suite/coq-makefile/latex1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/latex1/_CoqProject +++ b/test-suite/coq-makefile/latex1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/merlin1/_CoqProject +++ b/test-suite/coq-makefile/merlin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/mlpack1/_CoqProject +++ b/test-suite/coq-makefile/mlpack1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject index 51864a87ae..3db54e0a0b 100644 --- a/test-suite/coq-makefile/mlpack2/_CoqProject +++ b/test-suite/coq-makefile/mlpack2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/multiroot/_CoqProject b/test-suite/coq-makefile/multiroot/_CoqProject index b384bb6d97..f53eef99a8 100644 --- a/test-suite/coq-makefile/multiroot/_CoqProject +++ b/test-suite/coq-makefile/multiroot/_CoqProject @@ -4,7 +4,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject index a6fa17348c..847b2c00a9 100644 --- a/test-suite/coq-makefile/native1/_CoqProject +++ b/test-suite/coq-makefile/native1/_CoqProject @@ -4,7 +4,7 @@ -arg -native-compiler src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject index 357384fddf..619a8fa459 100644 --- a/test-suite/coq-makefile/only/_CoqProject +++ b/test-suite/coq-makefile/only/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mlpack -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin1/_CoqProject b/test-suite/coq-makefile/plugin1/_CoqProject index 4eddc9d708..ab7876d868 100644 --- a/test-suite/coq-makefile/plugin1/_CoqProject +++ b/test-suite/coq-makefile/plugin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin2/_CoqProject b/test-suite/coq-makefile/plugin2/_CoqProject index 0bf1e07f25..94eed53130 100644 --- a/test-suite/coq-makefile/plugin2/_CoqProject +++ b/test-suite/coq-makefile/plugin2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin3/_CoqProject b/test-suite/coq-makefile/plugin3/_CoqProject index 2028d49a8b..8e8a7ab074 100644 --- a/test-suite/coq-makefile/plugin3/_CoqProject +++ b/test-suite/coq-makefile/plugin3/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/quick2vo/_CoqProject +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 2e066d30d9..30be5e6456 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -11,7 +11,7 @@ mkdir -p theories/sub cp ../../template/theories/sub/testsub.v theories/sub cp ../../template/theories/test.v theories -cp ../../template/src/test.ml4 src +cp ../../template/src/test.mlg src cp ../../template/src/test_aux.mli src cp ../../template/src/test.mli src cp ../../template/src/test_plugin.mlpack src diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.mlg index 72765abe04..7a166f3b98 100644 --- a/test-suite/coq-makefile/template/src/test.ml4 +++ b/test-suite/coq-makefile/template/src/test.mlg @@ -1,13 +1,17 @@ +{ open Ltac_plugin +} DECLARE PLUGIN "test_plugin" +{ let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; +} VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "TestCommand" ] -> [ () ] + | [ "TestCommand" ] -> { () } END TACTIC EXTEND test -| [ "test_tactic" ] -> [ Test_aux.tac ] +| [ "test_tactic" ] -> { Test_aux.tac } END diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/uninstall1/_CoqProject +++ b/test-suite/coq-makefile/uninstall1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/uninstall2/_CoqProject +++ b/test-suite/coq-makefile/uninstall2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/validate1/_CoqProject b/test-suite/coq-makefile/validate1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/validate1/_CoqProject +++ b/test-suite/coq-makefile/validate1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/vio2vo/_CoqProject +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject index 70ec246062..e5dc3cff56 100644 --- a/test-suite/misc/poly-capture-global-univs/_CoqProject +++ b/test-suite/misc/poly-capture-global-univs/_CoqProject @@ -1,7 +1,7 @@ -Q theories Evil -I src -src/evil.ml4 +src/evil.mlg src/evilImpl.ml src/evilImpl.mli src/evil_plugin.mlpack diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 b/test-suite/misc/poly-capture-global-univs/src/evil.ml4 deleted file mode 100644 index 565e979aaa..0000000000 --- a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 +++ /dev/null @@ -1,9 +0,0 @@ - -open Stdarg -open EvilImpl - -DECLARE PLUGIN "evil_plugin" - -VERNAC COMMAND FUNCTIONAL EXTEND VernacEvil CLASSIFIED AS SIDEFF -| [ "Evil" ident(x) ident(y) ] -> [ fun ~atts ~st -> evil x y; st ] -END diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.mlg b/test-suite/misc/poly-capture-global-univs/src/evil.mlg new file mode 100644 index 0000000000..edd22b1d29 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil.mlg @@ -0,0 +1,10 @@ +{ +open Stdarg +open EvilImpl +} + +DECLARE PLUGIN "evil_plugin" + +VERNAC COMMAND EXTEND VernacEvil CLASSIFIED AS SIDEFF +| [ "Evil" ident(x) ident(y) ] -> { evil x y } +END diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out new file mode 100644 index 0000000000..5b67f632c9 --- /dev/null +++ b/test-suite/output/RecordFieldErrors.out @@ -0,0 +1,14 @@ +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record contains fields of both t and t'. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record defines several times the field foo. +The command has indeed failed with message: +This record defines several times the field unit. +The command has indeed failed with message: +unit: Not a projection of inductive t. diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v new file mode 100644 index 0000000000..27aa07822b --- /dev/null +++ b/test-suite/output/RecordFieldErrors.v @@ -0,0 +1,38 @@ +(** Check that various errors in record fields are reported with the correct +underlying issue. *) + +Record t := + { foo: unit }. + +Record t' := + { bar: unit }. + +Fail Check {| unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| unit := tt; + foo := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + bar := tt |}. +(* This record contains fields of both t and t'. *) + +Fail Check {| unit := tt; + unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + foo := tt |}. +(* This record defines several times the field foo. *) + +Fail Check {| foo := tt; + unit := tt; + unit := tt |}. +(* This is slightly wrong (would prefer "unit: Not a projection."), but it's +acceptable and seems an unlikely mistake. *) +(* This record defines several times the field unit. *) + +Fail Check {| foo := tt; + unit := tt |}. +(* unit: Not a projection of inductive t. *) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 403ad61798..e3fa0c24fe 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -21,6 +21,7 @@ VFILES := $(COQMF_VFILES) MLIFILES := $(COQMF_MLIFILES) MLFILES := $(COQMF_MLFILES) ML4FILES := $(COQMF_ML4FILES) +MLGFILES := $(COQMF_MLGFILES) MLPACKFILES := $(COQMF_MLPACKFILES) MLLIBFILES := $(COQMF_MLLIBFILES) CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES) @@ -87,6 +88,7 @@ COQTOP ?= "$(COQBIN)coqtop" COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" COQDOC ?= "$(COQBIN)coqdoc" +COQPP ?= "$(COQBIN)coqpp" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts @@ -241,6 +243,7 @@ VDFILE := .coqdeps ALLSRCFILES := \ $(ML4FILES) \ + $(MLGFILES) \ $(MLFILES) \ $(MLPACKFILES) \ $(MLLIBFILES) \ @@ -262,6 +265,7 @@ TEXFILES = $(VFILES:.v=.tex) GTEXFILES = $(VFILES:.v=.g.tex) CMOFILES = \ $(ML4FILES:.ml4=.cmo) \ + $(MLGFILES:.mlg=.cmo) \ $(MLFILES:.ml=.cmo) \ $(MLPACKFILES:.mlpack=.cmo) CMXFILES = $(CMOFILES:.cmo=.cmx) @@ -277,7 +281,7 @@ CMXSFILES = \ $(MLPACKFILES:.mlpack=.cmxs) \ $(CMXAFILES:.cmxa=.cmxs) \ $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs)) + $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) # files that are packed into a plugin (no extension) PACKEDFILES = \ @@ -555,6 +559,7 @@ clean:: $(HIDE)rm -f $(CMXSFILES) $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(MLGFILES:.mlg=.ml) $(HIDE)rm -f $(ALLDFILES) $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete @@ -602,11 +607,17 @@ $(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< -$(MLFILES:.ml=.cmo): %.cmo: %.ml +$(MLGFILES:.mlg=.ml): %.ml: %.mlg + $(SHOW)'COQPP $<' + $(HIDE)$(COQPP) $< + +# Stupid hack around a deficient syntax: we cannot concatenate two expansions +$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml $(SHOW)'CAMLC -c $<' $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< -$(MLFILES:.ml=.cmx): %.cmx: %.ml +# Same hack +$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< @@ -647,7 +658,7 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ # This rule is for _CoqProject with no .mllib nor .mlpack -$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -o $@ $< @@ -716,6 +727,10 @@ $(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 $(SHOW)'CAMLDEP -pp $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) +$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml $(SHOW)'CAMLDEP $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 7bb1390cad..ca5a232edb 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -218,7 +218,7 @@ let generate_conf_coq_config oc = ;; let generate_conf_files oc - { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; } + { v_files; mli_files; ml4_files; mlg_files; ml_files; mllib_files; mlpack_files; } = let module S = String in let map = map_sourced_list in @@ -227,6 +227,7 @@ let generate_conf_files oc fprintf oc "COQMF_MLIFILES = %s\n" (S.concat " " (map quote mli_files)); fprintf oc "COQMF_MLFILES = %s\n" (S.concat " " (map quote ml_files)); fprintf oc "COQMF_ML4FILES = %s\n" (S.concat " " (map quote ml4_files)); + fprintf oc "COQMF_MLGFILES = %s\n" (S.concat " " (map quote mlg_files)); fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files)); fprintf oc "COQMF_MLLIBFILES = %s\n" (S.concat " " (map quote mllib_files)); let cmdline_vfiles = filter_cmdline v_files in @@ -283,7 +284,7 @@ let generate_conf oc project args = let ensure_root_dir ({ ml_includes; r_includes; q_includes; - v_files; ml_files; mli_files; ml4_files; + v_files; ml_files; mli_files; ml4_files; mlg_files; mllib_files; mlpack_files } as project) = let exists f = List.exists (forget_source > f) in @@ -293,8 +294,8 @@ let ensure_root_dir || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes || (not_tops v_files && - not_tops mli_files && not_tops ml4_files && not_tops ml_files && - not_tops mllib_files && not_tops mlpack_files) + not_tops mli_files && not_tops ml4_files && not_tops mlg_files && + not_tops ml_files && not_tops mllib_files && not_tops mlpack_files) then project else diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 6a913ea894..713b2ad2b6 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -496,9 +496,9 @@ let rec suffixes = function let add_caml_known phys_dir _ f = let basename,suff = - get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in + get_extension f [".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] in match suff with - | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff @@ -584,12 +584,12 @@ let rec treat_file old_dirname old_name = in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> - (match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with + (match get_extension name [".v";".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] with | (base,".v") -> let name = file_name base dirname and absname = absolute_file_name base dirname in addQueue vAccu (name, absname) - | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname) + | (base,(".ml"|".ml4"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname) | (base,".mli") -> addQueue mliAccu (base,dirname) | (base,".mllib") -> addQueue mllibAccu (base,dirname) | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 053a0435ce..155296362f 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -145,9 +145,9 @@ let mllibAccu = ref ([] : (string * dir) list) let mlpackAccu = ref ([] : (string * dir) list) let add_caml_known phys_dir f = - let basename,suff = get_extension f [".ml";".ml4";".mlpack"] in + let basename,suff = get_extension f [".ml";".ml4";".mlg";".mlpack"] in match suff with - | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () |