diff options
41 files changed, 316 insertions, 126 deletions
diff --git a/.gitignore b/.gitignore index da675309e5..0411247abf 100644 --- a/.gitignore +++ b/.gitignore @@ -165,8 +165,7 @@ user-contrib plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml -# gramlib__pack -gramlib__pack +/gramlib/.pack # ocaml dev files .merlin @@ -178,3 +177,4 @@ theories/*/dune theories/*/*/dune theories/*/*/*/dune *.install +!Makefile.install diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 2444e3982e..65a8a0cb88 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -442,6 +442,9 @@ ci-plugin_tutorial: ci-quickchick: <<: *ci-template-flambda +ci-relation-algebra: + <<: *ci-template + ci-sf: <<: *ci-template diff --git a/.merlin.in b/.merlin.in index a8049361ee..fa3473765d 100644 --- a/.merlin.in +++ b/.merlin.in @@ -40,8 +40,8 @@ S API B API S ide B ide -S gramlib__pack -B gramlib__pack +S gramlib/.pack +B gramlib/.pack S tools B tools diff --git a/CHANGES.md b/CHANGES.md index 7a4af0d7a8..75a29de8e9 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -115,6 +115,9 @@ Standard Library Imported. This should be relevant only when importing files which don't use -noinit into files which do. +- Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an + ordered type (using lexical order). + Universes - Added `Print Universes Subgraph` variant of `Print Universes`. @@ -123,8 +123,11 @@ of the Coq Proof assistant during the indicated time: Sébastien Hinderer (INRIA, 2014) Gérard Huet (INRIA, 1985-1997) Matej Košík (INRIA, 2015-2017) + Leonidas Lampropoulos (University of Pennsylvania, 2018) Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS then IRIF, 2009-now) + Yao Li (ORCID: https://orcid.org/0000-0001-8720-883X, + University of Pennsylvania, 2018) Yishuai Li (ORCID: https://orcid.org/0000-0002-5728-5903 U. Penn, 2018) Patrick Loiseleur (Paris Sud, 1997-1999) diff --git a/META.coq.in b/META.coq.in index b3a96a8303..c2d3f85b9f 100644 --- a/META.coq.in +++ b/META.coq.in @@ -147,7 +147,7 @@ package "gramlib" ( version = "8.10" requires = "coq.lib" - directory = "gramlib__pack" + directory = "gramlib/.pack" archive(byte) = "gramlib.cma" archive(native) = "gramlib.cmxa" @@ -95,9 +95,9 @@ EXISTINGMLI := $(call find, '*.mli') GENMLGFILES:= $(MLGFILES:.mlg=.ml) # GRAMFILES must be in linking order -export GRAMFILES=$(addprefix gramlib__pack/gramlib__,Ploc Plexing Gramext Grammar) +export GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar) export GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) $(addsuffix .mli, $(GRAMFILES)) -export GENGRAMFILES := $(GRAMMLFILES) gramlib__pack/gramlib.ml +export GENGRAMFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) @@ -201,7 +201,7 @@ objclean: archclean indepclean .PHONY: gramlibclean gramlibclean: - rm -rf gramlib__pack/ + rm -rf gramlib/.pack/ cruftclean: mlgclean find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + @@ -291,7 +291,7 @@ KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ $(MLIFILES:.mli=.cmi) \ - gramlib__pack/gramlib.cma gramlib__pack/gramlib.cmxa $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma + gramlib/.pack/gramlib.cma gramlib/.pack/gramlib.cmxa $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) alienclean: diff --git a/Makefile.build b/Makefile.build index 8e4b63c364..ec9b81dba4 100644 --- a/Makefile.build +++ b/Makefile.build @@ -202,7 +202,7 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS) -DEPFLAGS=$(LOCALINCLUDES) -map gramlib__pack/gramlib.ml $(if $(filter plugins/%,$@),, -I ide -I ide/protocol) +DEPFLAGS=$(LOCALINCLUDES) -map gramlib/.pack/gramlib.ml $(if $(filter plugins/%,$@),, -I ide -I ide/protocol) # On MacOS, the binaries are signed, except our private ones ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) @@ -560,38 +560,38 @@ test-suite: world byte $(ALLSTDLIB).v # Default rules for compiling ML code ########################################################################### -gramlib__pack: +gramlib/.pack: mkdir -p $@ # gramlib.ml contents -gramlib__pack/gramlib.ml: | gramlib__pack +gramlib/.pack/gramlib.ml: | gramlib/.pack echo " \ module Ploc = Gramlib__Ploc \ module Plexing = Gramlib__Plexing \ module Gramext = Gramlib__Gramext \ module Grammar = Gramlib__Grammar" > $@ -gramlib__pack/gramlib__P%: gramlib/p% | gramlib__pack +gramlib/.pack/gramlib__P%: gramlib/p% | gramlib/.pack cp -a $< $@ sed -e "1i # 1 \"$<\"" -i $@ -gramlib__pack/gramlib__G%: gramlib/g% | gramlib__pack +gramlib/.pack/gramlib__G%: gramlib/g% | gramlib/.pack cp -a $< $@ sed -e "1i # 1 \"$<\"" -i $@ # Specific rules for gramlib to pack it Dune / OCaml 4.08 style GRAMOBJS=$(addsuffix .cmo, $(GRAMFILES)) -gramlib__pack/%: COND_BYTEFLAGS+=-no-alias-deps -w -49 -gramlib__pack/%: COND_OPTFLAGS+=-no-alias-deps -w -49 +gramlib/.pack/%: COND_BYTEFLAGS+=-no-alias-deps -w -49 +gramlib/.pack/%: COND_OPTFLAGS+=-no-alias-deps -w -49 -gramlib__pack/gramlib.%: COND_OPENFLAGS= -gramlib__pack/gramlib__%: COND_OPENFLAGS=-open Gramlib +gramlib/.pack/gramlib.%: COND_OPENFLAGS= +gramlib/.pack/gramlib__%: COND_OPENFLAGS=-open Gramlib -gramlib__pack/gramlib.cma: $(GRAMOBJS) gramlib__pack/gramlib.cmo +gramlib/.pack/gramlib.cma: $(GRAMOBJS) gramlib/.pack/gramlib.cmo $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $^ -gramlib__pack/gramlib.cmxa: $(GRAMOBJS:.cmo=.cmx) gramlib__pack/gramlib.cmx +gramlib/.pack/gramlib.cmxa: $(GRAMOBJS:.cmo=.cmx) gramlib/.pack/gramlib.cmx $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $^ @@ -748,8 +748,8 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack -MAINMLFILES := $(filter-out gramlib__pack/% checker/% plugins/%, $(MLFILES) $(MLIFILES)) -MAINMLLIBFILES := $(filter-out gramlib__pack/% checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) +MAINMLFILES := $(filter-out gramlib/.pack/% checker/% plugins/%, $(MLFILES) $(MLIFILES)) +MAINMLLIBFILES := $(filter-out gramlib/.pack/% checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) $(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) $(GENGRAMFILES) $(SHOW)'OCAMLDEP MLFILES MLIFILES' diff --git a/Makefile.ci b/Makefile.ci index d0b87fc58b..956e3ee58f 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -39,6 +39,7 @@ CI_TARGETS= \ ci-paramcoq \ ci-plugin_tutorial \ ci-quickchick \ + ci-relation-algebra \ ci-sf \ ci-simple-io \ ci-tlc \ diff --git a/Makefile.common b/Makefile.common index ca2cb8fee6..a59fbe676e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -91,7 +91,7 @@ MKDIR:=install -d CORESRCDIRS:=\ coqpp \ config clib lib kernel kernel/byterun library \ - engine pretyping interp proofs gramlib__pack parsing printing \ + engine pretyping interp proofs gramlib/.pack parsing printing \ tactics vernac stm toplevel PLUGINDIRS:=\ @@ -119,7 +119,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ - gramlib__pack/gramlib.cma \ + gramlib/.pack/gramlib.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma diff --git a/Makefile.install b/Makefile.install index 8233807e03..b6e2ec2aeb 100644 --- a/Makefile.install +++ b/Makefile.install @@ -92,17 +92,20 @@ install-tools: INSTALLCMI = $(sort \ $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ + $(filter %.cmi, $(GRAMMLFILES:.mli=.cmi)) gramlib/.pack/gramlib.cmi \ $(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \ - $(PLUGINS:.cmo=.cmi) gramlib__pack/gramlib.cmi + $(PLUGINS:.cmo=.cmi) INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \ configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \ - $(MLFILES:.ml=.cmx))) + $(filter %.cmx, $(GRAMMLFILES:.ml=.cmx)) $(MLFILES:.ml=.cmx))) + +foo: + @echo $(INSTALLCMX) install-devfiles: $(MKDIR) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) # Regular CMI files $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMX) # To avoid warning 58 "-opaque" $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static linking of plugins diff --git a/checker/values.ml b/checker/values.ml index dcb2bca81a..863f965896 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -93,9 +93,9 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|] (** kernel/univ *) - +let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|] let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) - [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|] + [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|] let v_level = v_tuple "level" [|Int;v_raw_level|] let v_expr = v_tuple "levelexpr" [|v_level;Int|] let v_univ = List v_expr diff --git a/configure.ml b/configure.ml index 6db96244f5..33f76078cf 100644 --- a/configure.ml +++ b/configure.ml @@ -1100,7 +1100,7 @@ let write_configml f = pr_b "native_compiler" !prefs.nativecompiler; let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library"; - "engine"; "pretyping"; "interp"; "gramlib__pack"; "parsing"; "proofs"; + "engine"; "pretyping"; "interp"; "gramlib/.pack"; "parsing"; "proofs"; "tactics"; "toplevel"; "printing"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 9727d42a90..e0f4f50fa9 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -266,3 +266,10 @@ : "${paramcoq_CI_REF:=master}" : "${paramcoq_CI_GITURL:=https://github.com/coq-community/paramcoq}" : "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" + +######################################################################## +# relation-algebra +######################################################################## +: "${relation_algebra_CI_REF:=master}" +: "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" +: "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}" diff --git a/dev/ci/ci-relation-algebra.sh b/dev/ci/ci-relation-algebra.sh new file mode 100755 index 0000000000..84bed5bdfe --- /dev/null +++ b/dev/ci/ci-relation-algebra.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download relation_algebra + +( cd "${CI_BUILD_DIR}/relation_algebra" && make && make install ) diff --git a/dev/core.dbg b/dev/core.dbg index f676b643e4..ec946e2df0 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -1,10 +1,10 @@ load_printer threads.cma load_printer str.cma -load_printer gramlib.cma load_printer config.cma load_printer clib.cma load_printer dynlink.cma load_printer lib.cma +load_printer gramlib.cma load_printer kernel.cma load_printer library.cma load_printer engine.cma diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index c1dcabb743..a11269e059 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -17,7 +17,7 @@ exec $OCAMLDEBUG \ -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ - -I $COQTOP/gramlib__pack \ + -I $COQTOP/gramlib/.pack \ -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ diff --git a/engine/termops.mli b/engine/termops.mli index eef8452e64..7920af8e0e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -290,7 +290,7 @@ val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool val is_Type : Evd.evar_map -> constr -> bool -val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid +val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option (** Combinators on judgments *) diff --git a/engine/uState.ml b/engine/uState.ml index 05bef91f1e..6969d2ba44 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -324,12 +324,14 @@ let constrain_variables diff ctx = let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname) + try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)) with Not_found | Option.IsNone -> UnivNames.qualid_of_level l let pr_uctx_level uctx l = - Libnames.pr_qualid (qualid_of_level uctx l) + match qualid_of_level uctx l with + | Some qid -> Libnames.pr_qualid qid + | None -> Univ.Level.pr l type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) @@ -533,7 +535,7 @@ let emit_side_effects eff u = let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = UnivGen.new_univ_level () in + let u = UnivGen.fresh_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with diff --git a/engine/uState.mli b/engine/uState.mli index ad0cd5c1bb..5170184ef4 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -188,6 +188,6 @@ val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) val pr_uctx_level : t -> Univ.Level.t -> Pp.t -val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid +val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t diff --git a/engine/univGen.ml b/engine/univGen.ml index 130aa06f53..40c4c909fe 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -13,26 +13,25 @@ open Names open Constr open Univ +type univ_unique_id = int (* Generator of levels *) -type universe_id = DirPath.t * int - let new_univ_id, set_remote_new_univ_id = RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> Global.current_dirpath (), n) + ~build:(fun n -> n) -let new_univ_level () = - let dp, id = new_univ_id () in - Univ.Level.make dp id +let new_univ_global () = + Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ()) -let fresh_level () = new_univ_level () +let fresh_level () = + Univ.Level.make (new_univ_global ()) (* TODO: remove *) -let new_univ dp = Univ.Universe.make (new_univ_level dp) -let new_Type dp = mkType (new_univ dp) -let new_Type_sort dp = Type (new_univ dp) +let new_univ () = Univ.Universe.make (fresh_level ()) +let new_Type () = mkType (new_univ ()) +let new_Type_sort () = Type (new_univ ()) let fresh_instance auctx = - let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in + let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in let ctx = Array.fold_right LSet.add inst LSet.empty in let inst = Instance.of_array inst in inst, (ctx, AUContext.instantiate inst auctx) diff --git a/engine/univGen.mli b/engine/univGen.mli index 8af5f8fdb0..b4598e10d0 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -15,14 +15,14 @@ open Univ (** The global universe counter *) -type universe_id = DirPath.t * int - -val set_remote_new_univ_id : universe_id RemoteCounter.installer +type univ_unique_id +val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer +val new_univ_id : unit -> univ_unique_id (** for the stm *) (** Side-effecting functions creating new universe levels. *) -val new_univ_id : unit -> universe_id -val new_univ_level : unit -> Level.t +val new_univ_global : unit -> Level.UGlobal.t +val fresh_level : unit -> Level.t val new_univ : unit -> Universe.t [@@ocaml.deprecated "Use [new_univ_level]"] diff --git a/engine/univNames.ml b/engine/univNames.ml index 39a9a8a3a5..7e6ed5e4c0 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -15,17 +15,15 @@ open Univ let qualid_of_level l = match Level.name l with - | Some (d, n as na) -> - begin - try Nametab.shortest_qualid_of_universe na - with Not_found -> - let name = Id.of_string_soft (string_of_int n) in - Libnames.make_qualid d name - end - | None -> - Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l) + | Some qid -> + (try Some (Nametab.shortest_qualid_of_universe qid) + with Not_found -> None) + | None -> None -let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l) +let pr_with_global_universes l = + match qualid_of_level l with + | Some qid -> Libnames.pr_qualid qid + | None -> Level.pr l (** Global universe information outside the kernel, to handle polymorphic universe names in sections that have to be discharged. *) diff --git a/engine/univNames.mli b/engine/univNames.mli index 6e68153ac2..e9c517babf 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -11,7 +11,7 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t -val qualid_of_level : Level.t -> Libnames.qualid +val qualid_of_level : Level.t -> Libnames.qualid option (** Local universe name <-> level mapping *) diff --git a/interp/declare.ml b/interp/declare.ml index a61078705a..a0ebc3775e 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -467,7 +467,7 @@ type universe_source = | QualifiedUniv of Id.t (* global universe introduced by some global value *) | UnqualifiedUniv (* other global universe *) -type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list +type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list let check_exists sp = if Nametab.exists_universe sp then @@ -538,12 +538,8 @@ let do_universe poly l = user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in - let l = - List.map (fun {CAst.v=id} -> - let lev = UnivGen.new_univ_id () in - (id, lev)) l - in - let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx) + let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in + let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) Univ.LSet.empty l, Univ.Constraint.empty in let () = declare_universe_context poly ctx in diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a4a02791b4..68d44f8782 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -218,7 +218,9 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in let uctx = CumulativityInfo.univ_context cumi in - let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in + let new_levels = Array.init (UContext.size uctx) + (fun i -> Level.make (Level.UGlobal.make DirPath.empty i)) + in let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bbcf07f7e..05c5c0e821 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -593,10 +593,10 @@ let rec ienv_decompose_prod (env,_ as ienv) n c = ienv_decompose_prod ienv' (n-1) b | _ -> assert false +let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0)) +let dummy_implicit_sort = mkType (Universe.make dummy_univ) let lambda_implicit_lift n a = - let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in - let implicit_sort = mkType (Universe.make level) in - let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in + let lambda_implicit a = mkLambda (Anonymous, dummy_implicit_sort, a) in iterate lambda_implicit n (lift n a) (* This removes global parameters of the inductive types in lc (for diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index afdc8f1511..5fc8d0297f 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -921,7 +921,7 @@ let sort_universes g = let types = Array.init (max_lvl + 1) (function | 0 -> Level.prop | 1 -> Level.set - | n -> Level.make mp (n-2)) + | n -> Level.make (Level.UGlobal.make mp (n-2))) in let g = Array.fold_left (fun g u -> let g, u = safe_repr g u in diff --git a/kernel/univ.ml b/kernel/univ.ml index 2b3b4f9486..7b5ed05bda 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -36,10 +36,26 @@ open Util module RawLevel = struct open Names + + module UGlobal = struct + type t = DirPath.t * int + + let make dp i = (DirPath.hcons dp,i) + + let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' + + let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d) + + let compare (d, i) (d', i') = + let c = Int.compare i i' in + if Int.equal c 0 then DirPath.compare d d' + else c + end + type t = | Prop | Set - | Level of int * DirPath.t + | Level of UGlobal.t | Var of int (* Hash-consing *) @@ -49,8 +65,7 @@ struct match x, y with | Prop, Prop -> true | Set, Set -> true - | Level (n,d), Level (n',d') -> - Int.equal n n' && DirPath.equal d d' + | Level l, Level l' -> UGlobal.equal l l' | Var n, Var n' -> Int.equal n n' | _ -> false @@ -62,7 +77,7 @@ struct | Set, Set -> 0 | Set, _ -> -1 | _, Set -> 1 - | Level (i1, dp1), Level (i2, dp2) -> + | Level (dp1, i1), Level (dp2, i2) -> if i1 < i2 then -1 else if i1 > i2 then 1 else DirPath.compare dp1 dp2 @@ -83,9 +98,9 @@ struct let hcons = function | Prop as x -> x | Set as x -> x - | Level (n,d) as x -> + | Level (d,n) as x -> let d' = Names.DirPath.hcons d in - if d' == d then x else Level (n,d') + if d' == d then x else Level (d',n) | Var _n as x -> x open Hashset.Combine @@ -94,18 +109,18 @@ struct | Prop -> combinesmall 1 0 | Set -> combinesmall 1 1 | Var n -> combinesmall 2 n - | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d)) + | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d)) end module Level = struct - open Names + module UGlobal = RawLevel.UGlobal type raw_level = RawLevel.t = | Prop | Set - | Level of int * DirPath.t + | Level of UGlobal.t | Var of int (** Embed levels with their hash value *) @@ -166,7 +181,7 @@ module Level = struct match data x with | Prop -> "Prop" | Set -> "Set" - | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n + | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n | Var n -> "Var(" ^ string_of_int n ^ ")" let pr u = str (to_string u) @@ -185,11 +200,11 @@ module Level = struct match data u with | Var n -> Some n | _ -> None - let make m n = make (Level (n, Names.DirPath.hcons m)) + let make qid = make (Level qid) let name u = match data u with - | Level (n, d) -> Some (d, n) + | Level (d, n) -> Some (d, n) | _ -> None end diff --git a/kernel/univ.mli b/kernel/univ.mli index de7b334ae4..512f38cedd 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -11,9 +11,22 @@ (** Universes. *) module Level : sig + + module UGlobal : sig + type t + + val make : Names.DirPath.t -> int -> t + val equal : t -> t -> bool + val hash : t -> int + val compare : t -> t -> int + + end + (** Qualified global universe level *) + type t (** Type of universe levels. A universe level is essentially a unique name - that will be associated to constraints later on. *) + that will be associated to constraints later on. A level can be local to a + definition or global. *) val set : t val prop : t @@ -34,9 +47,7 @@ sig val hash : t -> int - val make : Names.DirPath.t -> int -> t - (** Create a new universe level from a unique identifier and an associated - module path. *) + val make : UGlobal.t -> t val pr : t -> Pp.t (** Pretty-printing *) @@ -48,7 +59,7 @@ sig val var_index : t -> int option - val name : t -> (Names.DirPath.t * int) option + val name : t -> UGlobal.t option end (** Sets of universe levels *) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 811fcf4063..79f0a806a7 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -112,7 +112,7 @@ let iprint_no_report (e, info) = let _ = register_handler begin function | UserError(s, pps) -> - hov 0 (where s ++ pps) + where s ++ pps | _ -> raise Unhandled end diff --git a/library/nametab.ml b/library/nametab.ml index 503cf515d5..95890b2edf 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -348,12 +348,10 @@ module DirTab = Make(DirPath')(GlobDirRef) type dirtab = DirTab.t let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab) -type universe_id = DirPath.t * int - module UnivIdEqual = struct - type t = universe_id - let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' + type t = Univ.Level.UGlobal.t + let equal = Univ.Level.UGlobal.equal end module UnivTab = Make(FullPath)(UnivIdEqual) type univtab = UnivTab.t @@ -376,12 +374,9 @@ let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevt module UnivIdOrdered = struct - type t = universe_id - let hash (d, i) = i + DirPath.hash d - let compare (d, i) (d', i') = - let c = Int.compare i i' in - if Int.equal c 0 then DirPath.compare d d' - else c + type t = Univ.Level.UGlobal.t + let hash = Univ.Level.UGlobal.hash + let compare = Univ.Level.UGlobal.compare end module UnivIdMap = HMap.Make(UnivIdOrdered) diff --git a/library/nametab.mli b/library/nametab.mli index 78d0f83b6e..fccb8fd918 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -120,11 +120,9 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit -type universe_id = DirPath.t * int +module UnivIdMap : CMap.ExtS with type key = Univ.Level.UGlobal.t -module UnivIdMap : CMap.ExtS with type key = universe_id - -val push_universe : visibility -> full_path -> universe_id -> unit +val push_universe : visibility -> full_path -> Univ.Level.UGlobal.t -> unit (** {6 The following functions perform globalization of qualified names } *) @@ -139,7 +137,7 @@ val locate_modtype : qualid -> ModPath.t val locate_dir : qualid -> GlobDirRef.t val locate_module : qualid -> ModPath.t val locate_section : qualid -> DirPath.t -val locate_universe : qualid -> universe_id +val locate_universe : qualid -> Univ.Level.UGlobal.t (** These functions globalize user-level references into global references, like [locate] and co, but raise a nice error message @@ -198,7 +196,7 @@ val path_of_modtype : ModPath.t -> full_path (** A universe_id might not be registered with a corresponding user name. @raise Not_found if the universe was not introduced by the user. *) -val path_of_universe : universe_id -> full_path +val path_of_universe : Univ.Level.UGlobal.t -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) @@ -220,7 +218,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid -val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid +val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid (** Deprecated synonyms *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0b545dc191..09b3cf167f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -589,8 +589,23 @@ let detype_cofix detype avoid env sigma n (names,tys,bodies) = Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) +(* TODO use some algebraic type with a case for unnamed univs so we + can cleanly detype them. NB: this corresponds to a hack in + Pretyping.interp_universe_level_name to convert Foo.xx strings into + universes. *) +let hack_qualid_of_univ_level sigma l = + match Termops.reference_of_level sigma l with + | Some qid -> qid + | None -> + let path = String.split_on_char '.' (Univ.Level.to_string l) in + let path = List.rev_map Id.of_string_soft path in + Libnames.qualid_of_dirpath (DirPath.make path) + let detype_universe sigma u = - let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in + let fn (l, n) = + let qid = hack_qualid_of_univ_level sigma l in + Some (qid, n) + in Univ.Universe.map fn u let detype_sort sigma = function @@ -611,7 +626,7 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - let l = Termops.reference_of_level sigma l in + let l = hack_qualid_of_univ_level sigma l in GType (UNamed l) let detype_instance sigma l = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 74ef1ddbca..ace2868255 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -120,8 +120,8 @@ let interp_known_universe_level evd qid = if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid else raise Not_found with Not_found -> - let univ, k = Nametab.locate_universe qid in - Univ.Level.make univ k + let qid = Nametab.locate_universe qid in + Univ.Level.make qid let interp_universe_level_name ~anon_rigidity evd qid = try evd, interp_known_universe_level evd qid @@ -140,7 +140,7 @@ let interp_universe_level_name ~anon_rigidity evd qid = user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid)) in - let level = Univ.Level.make dp num in + let level = Univ.Level.(make (UGlobal.make dp num)) in let evd = try Evd.add_global_univ evd level with UGraph.AlreadyDeclared -> evd diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 94e04d1842..51166cf238 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -60,7 +60,7 @@ module Make(T : Task) () = struct type request = Request of T.request type more_data = - | MoreDataUnivLevel of UnivGen.universe_id list + | MoreDataUnivLevel of UnivGen.univ_unique_id list let slave_respond (Request r) = let res = T.perform r in diff --git a/test-suite/Makefile b/test-suite/Makefile index 1db97f43c5..9d2277c37e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -62,6 +62,7 @@ get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_ # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload)) +get_set_impredicativity= $(filter "-impredicative-set",$(call get_coq_prog_args,$(1))) bogomips:= @@ -303,6 +304,8 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v echo " $<...correctly prepared" ; \ fi; \ } > "$@" + @echo "CHK $(shell basename $< .v)" + $(HIDE)$(coqchk) -norec TestSuite.$(shell basename $< .v) > $(shell dirname $<)/$(shell basename $< .v).chk.log 2>&1 ssr: $(wildcard ssr/*.v:%.v=%.v.log) $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @@ -320,6 +323,16 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v $(FAIL); \ fi; \ } > "$@" + @echo "CHK $(shell basename $< .v)" + $(HIDE){ \ + opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \ + $(coqchk) -silent $(call get_set_impredicativity,$<) $$opts 2>&1; R=$$?; \ + if [ $$R != 0 ]; then \ + echo $(log_failure); \ + echo " $<...could not be checked (Error!)" ; \ + $(FAIL); \ + fi; \ + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" stm: $(wildcard stm/*.v:%.v=%.v.log) $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @@ -337,6 +350,15 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v $(FAIL); \ fi; \ } > "$@" + @echo "CHK $(shell basename $< .v)" + $(HIDE){ \ + $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + if [ $$R != 0 ]; then \ + echo $(log_failure); \ + echo " $<...could not be checked (Error!)" ; \ + $(FAIL); \ + fi; \ + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" @@ -352,6 +374,15 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(FAIL); \ fi; \ } > "$@" + @echo "CHK $(shell basename $< .v)" + $(HIDE){ \ + $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + if [ $$R != 0 ]; then \ + echo $(log_failure); \ + echo " $<...could not be checked (Error!)" ; \ + $(FAIL); \ + fi; \ + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" diff --git a/test-suite/output/ErrorInCanonicalStructures.out b/test-suite/output/ErrorInCanonicalStructures.out index 73da4f44f8..b4aa60a2c8 100644 --- a/test-suite/output/ErrorInCanonicalStructures.out +++ b/test-suite/output/ErrorInCanonicalStructures.out @@ -1,5 +1,4 @@ File "stdin", line 3, characters 0-24: -Error: -Could not declare a canonical structure Foo. +Error: Could not declare a canonical structure Foo. Expected an instance of a record or structure. diff --git a/test-suite/output/ErrorInCanonicalStructures2.out b/test-suite/output/ErrorInCanonicalStructures2.out index 63a2871b82..ab64e25030 100644 --- a/test-suite/output/ErrorInCanonicalStructures2.out +++ b/test-suite/output/ErrorInCanonicalStructures2.out @@ -1,5 +1,4 @@ File "stdin", line 3, characters 0-24: -Error: -Could not declare a canonical structure bar. +Error: Could not declare a canonical structure bar. Expected an instance of a record or structure. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index f2a9a56914..1a182de764 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -10,6 +10,8 @@ Require Import OrderedType. Require Import ZArith. +Require Import PeanoNat. +Require Import Ascii String. Require Import Omega. Require Import NArith Ndec. Require Import Compare_dec. @@ -315,3 +317,94 @@ Module PositiveOrderedTypeBits <: UsualOrderedType. Qed. End PositiveOrderedTypeBits. + +(** [String] is an ordered type with respect to the usual lexical order. *) + +Module String_as_OT <: UsualOrderedType. + + Definition t := string. + + Definition eq := @eq string. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. + + Inductive lts : string -> string -> Prop := + | lts_empty : forall a s, lts EmptyString (String a s) + | lts_tail : forall a s1 s2, lts s1 s2 -> lts (String a s1) (String a s2) + | lts_head : forall (a b : ascii) s1 s2, + lt (nat_of_ascii a) (nat_of_ascii b) -> + lts (String a s1) (String b s2). + + Definition lt := lts. + + Lemma nat_of_ascii_inverse a b : nat_of_ascii a = nat_of_ascii b -> a = b. + Proof. + intro H. + rewrite <- (ascii_nat_embedding a). + rewrite <- (ascii_nat_embedding b). + apply f_equal; auto. + Qed. + + Lemma lts_tail_unique a s1 s2 : lt (String a s1) (String a s2) -> + lt s1 s2. + Proof. + intro H; inversion H; subst; auto. + remember (nat_of_ascii a) as x. + apply lt_irrefl in H1; inversion H1. + Qed. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. + induction x; intros y z H1 H2. + - destruct y as [| b y']; inversion H1. + destruct z as [| c z']; inversion H2; constructor. + - destruct y as [| b y']; inversion H1; subst; + destruct z as [| c z']; inversion H2; subst. + + constructor. eapply IHx; eauto. + + constructor; assumption. + + constructor; assumption. + + constructor. eapply lt_trans; eassumption. + Qed. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + induction x; intros y LT. + - inversion LT. intro. inversion H. + - inversion LT; subst; intros EQ. + * specialize (IHx s2 H2). + inversion EQ; subst; auto. + apply IHx; unfold eq; auto. + * inversion EQ; subst; auto. + apply Nat.lt_irrefl in H2; auto. + Qed. + + Definition compare x y : Compare lt eq x y. + Proof. + generalize dependent y. + induction x as [ | a s1]; destruct y as [ | b s2]. + - apply EQ; constructor. + - apply LT; constructor. + - apply GT; constructor. + - destruct ((nat_of_ascii a) ?= (nat_of_ascii b))%nat eqn:ltb. + + assert (a = b). + { + apply Nat.compare_eq in ltb. + assert (ascii_of_nat (nat_of_ascii a) + = ascii_of_nat (nat_of_ascii b)) by auto. + repeat rewrite ascii_nat_embedding in H. + auto. + } + subst. + destruct (IHs1 s2). + * apply LT; constructor; auto. + * apply EQ. unfold eq in e. subst. constructor; auto. + * apply GT; constructor; auto. + + apply nat_compare_lt in ltb. + apply LT; constructor; auto. + + apply nat_compare_gt in ltb. + apply GT; constructor; auto. + Defined. + + Definition eq_dec (x y : string): {x = y} + { ~ (x = y)} := string_dec x y. +End String_as_OT. diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 41057a79e0..9ecd8f19ce 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -109,6 +109,9 @@ module Aux = struct (* Move to Dirmap.update once we require OCaml >= 4.06.0 *) Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map + let replace_ext ~file ~newext = + Filename.(remove_extension file) ^ newext + end open Aux @@ -163,6 +166,11 @@ let pp_rule fmt targets deps action = "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n" ppl targets pp_deps deps pp_print_string action +let gen_coqc_targets vo = + [ vo.target + ; replace_ext ~file:vo.target ~newext:".glob" + ; "." ^ replace_ext ~file:vo.target ~newext:".aux"] + (* Generate the dune rule: *) let pp_vo_dep dir fmt vo = let depth = List.length dir in @@ -174,12 +182,13 @@ let pp_vo_dep dir fmt vo = (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in (* The source file is also corrected as we will call coqtop from the top dir *) - let source = bpath (dir @ [Filename.(remove_extension vo.target) ^ ".v"]) in + let source = bpath (dir @ [replace_ext ~file:vo.target ~newext:".v"]) in (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) let libflag = "-coqlib %{project_root}" in (* The final build rule *) let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in - pp_rule fmt [vo.target] deps action + let all_targets = gen_coqc_targets vo in + pp_rule fmt all_targets deps action let pp_mlg_dep _dir fmt ml = let target = Filename.(remove_extension ml) ^ ".ml" in @@ -192,9 +201,9 @@ let pp_dep dir fmt oo = match oo with let out_install fmt dir ff = let itarget = String.concat "/" dir in - let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in - let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (bpath [itarget;tg]) in - fprintf fmt "(install@\n @[(section lib)@\n(package coq)@\n(files @[%a@])@])@\n" + let ff = List.concat @@ pmap (function | VO vo -> Some (gen_coqc_targets vo) | _ -> None) ff in + let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in + fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n" (pp_list pp_ispec sep) ff (* For each directory, we must record two things, the build rules and |