diff options
58 files changed, 419 insertions, 325 deletions
diff --git a/.gitignore b/.gitignore index 05869e2a0c..538124b8e5 100644 --- a/.gitignore +++ b/.gitignore @@ -50,7 +50,6 @@ TAGS bin/ _build_ci _build -myocamlbuild_config.ml config/Makefile config/coq_config.ml config/coq_config.py @@ -69,6 +68,7 @@ time-of-build-after.log .csdp.cache test-suite/.lia.cache test-suite/.nra.cache +test-suite/.nia.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt @@ -136,7 +136,6 @@ coqpp/coqpp_parse.mli g_*.ml lib/coqProject_file.ml -parsing/cLexer.ml plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml plugins/ltac/extraargs.ml @@ -167,8 +166,6 @@ checker/esubst.mli user-contrib .*.sw* .#* -test-suite/.lia.cache -test-suite/.nra.cache plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1669145d9b..bb1aa81a73 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-10-04-V1" + CACHEKEY: "bionic_coq-V2018-10-22-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -261,7 +261,7 @@ cacheclean: find theories plugins test-suite -name '.*.aux' -exec rm -f {} + cleanconfig: - rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist distclean: clean cleanconfig cacheclean timingclean diff --git a/Makefile.build b/Makefile.build index 4d19f9a2e1..77fcfc0abf 100644 --- a/Makefile.build +++ b/Makefile.build @@ -406,7 +406,7 @@ grammar/%.cmi: grammar/%.mli .PHONY: coqbinaries coqbyte -coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) $(GRAMMARCMA) coqbyte: $(TOPBYTE) $(CHICKENBYTE) # Special rule for coqtop, we imitate `ocamlopt` can delete the target diff --git a/checker/reduction.ml b/checker/reduction.ml index d36c0ef2c9..58a3f4e410 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -280,17 +280,26 @@ let get_strategy { var_opacity; cst_opacity } = function with Not_found -> default_level) | RelKey _ -> Expand +let dep_order l2r k1 k2 = match k1, k2 with +| RelKey _, RelKey _ -> l2r +| RelKey _, (VarKey _ | ConstKey _) -> true +| VarKey _, RelKey _ -> false +| VarKey _, VarKey _ -> l2r +| VarKey _, ConstKey _ -> true +| ConstKey _, (RelKey _ | VarKey _) -> false +| ConstKey _, ConstKey _ -> l2r + let oracle_order infos l2r k1 k2 = let o = Closure.oracle_of_infos infos in match get_strategy o k1, get_strategy o k2 with - | Expand, Expand -> l2r + | Expand, Expand -> dep_order l2r k1 k2 | Expand, (Opaque | Level _) -> true | (Opaque | Level _), Expand -> false - | Opaque, Opaque -> l2r + | Opaque, Opaque -> dep_order l2r k1 k2 | Level _, Opaque -> true | Opaque, Level _ -> false | Level n1, Level n2 -> - if Int.equal n1 n2 then l2r + if Int.equal n1 n2 then dep_order l2r k1 k2 else n1 < n2 let eq_table_key univ = diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index d2176e326c..84fec71f7a 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -12,4 +12,4 @@ opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $A eval "$(opam config env)" opam install -y num ocamlfind camlp5 ounit -cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 50d4d21637..f422030b53 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -238,7 +238,7 @@ ######################################################################## # plugin_tutorial ######################################################################## -: "${plugin_tutorial_CI_REF:=master}" +: "${plugin_tutorial_CI_REF:=14b2976cdf67db788b79d9421ce1e89bd15c7313}" : "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" : "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index f257c62dd3..41e1d1a937 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-04-V2" +# CACHEKEY: "bionic_coq-V2018-10-22-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index fd3101613a..8cefe699cc 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -140,11 +140,9 @@ New files For a new file, in most cases, you just have to add it to the proper file list(s): - For .ml, in the corresponding .mllib (e.g. kernel/kernel.mllib) - These files are also used by the experimental ocamlbuild plugin, - which is quite touchy about them : be careful with order, - duplicated entries, whitespace errors, and do not mention .mli there. - If module B depends on module A, then B should be after A in the .mllib - file. + Be careful with order, duplicated entries, whitespace errors, and + do not mention .mli there. If module B depends on module A, then B + should be after A in the .mllib file. - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) - The definitions in Makefile.common might have to be adapted too. - If your file needs a specific rule, add it to Makefile.build diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt deleted file mode 100644 index efedbc506e..0000000000 --- a/dev/doc/ocamlbuild.txt +++ /dev/null @@ -1,30 +0,0 @@ -Ocamlbuild & Coq ----------------- - -A quick note in case someone else gets interested someday in compiling -Coq via ocamlbuild : such an experimental build system has existed -in the past (more or less maintained from 2009 to 2013), in addition -to the official build system via gnu make. But this build via -ocamlbuild has been severly broken since early 2014 (and don't work -in 8.5, for instance). This experiment has attracted very limited -interest from other developers over the years, and has been quite -cumbersome to maintain, so it is now officially discontinued. -If you want to have a look at the files of this build system -(especially myocamlbuild.ml), you can fetch : - - my last effort at repairing this build system (up to coqtop.native) : - https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair - - coq official v8.5 branch (recent but broken) - - coq v8.4 branch(less up-to-date, but works). - -For the record, the three main drawbacks of this experiments were: - - recurrent issues with circularities reported by ocamlbuild - (even though make was happy) during the evolution of Coq sources - - no proper support of parallel build - - quite slow re-traversal of already built things -See the two corresponding bug reports on Mantis, or -https://github.com/ocaml/ocamlbuild/issues/52 - -As an interesting feature, I successfully used this to cross-compile -Coq 8.4 from linux to win32 via mingw. - -Pierre Letouzey, june 2016 diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 381f8bb661..835d6dcaa6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -533,10 +533,10 @@ Convertibility Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the relation :math:`t` reduces to :math:`u` in the global environment :math:`E` and local context :math:`Γ` with one of the previous -reductions β, ι, δ or ζ. +reductions β, δ, ι or ζ. We say that two terms :math:`t_1` and :math:`t_2` are -*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the +*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 8c82526f0c..1a33a9a46e 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1112,6 +1112,59 @@ co-inductive definitions are also allowed. object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite objects in Section :ref:`cofixpoint`. +Caveat +++++++ + +The ability to define co-inductive types by constructors, hereafter called +*positive co-inductive types*, is known to break subject reduction. The story is +a bit long: this is due to dependent pattern-matching which implies +propositional η-equality, which itself would require full η-conversion for +subject reduction to hold, but full η-conversion is not acceptable as it would +make type-checking undecidable. + +Since the introduction of primitive records in Coq 8.5, an alternative +presentation is available, called *negative co-inductive types*. This consists +in defining a co-inductive type as a primitive record type through its +projections. Such a technique is akin to the *co-pattern* style that can be +found in e.g. Agda, and preserves subject reduction. + +The above example can be rewritten in the following way. + +.. coqtop:: all + + Set Primitive Projections. + CoInductive Stream : Set := Seq { hd : nat; tl : Stream }. + CoInductive EqSt (s1 s2: Stream) : Prop := eqst { + eqst_hd : hd s1 = hd s2; + eqst_tl : EqSt (tl s1) (tl s2); + }. + +Some properties that hold over positive streams are lost when going to the +negative presentation, typically when they imply equality over streams. +For instance, propositional η-equality is lost when going to the negative +presentation. It is nonetheless logically consistent to recover it through an +axiom. + +.. coqtop:: all + + Axiom Stream_eta : forall s: Stream, s = cons (hs s) (tl s). + +More generally, as in the case of positive coinductive types, it is consistent +to further identify extensional equality of coinductive types with propositional +equality: + +.. coqtop:: all + + Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. + +As of Coq 8.9, it is now advised to use negative co-inductive types rather than +their positive counterparts. + +.. seealso:: + :ref:`primitive_projections` for more information about negative + records and primitive projections. + + Definition of recursive functions --------------------------------- diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index c802f44ac1..741f9fe5b0 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -144,8 +144,9 @@ list of assertion commands is given in :ref:`Assertions`. The command the proof is a subset of the declared one. The set of declared variables is closed under type dependency. For - example if ``T`` is variable and a is a variable of type ``T``, the commands - ``Proof using a`` and ``Proof using T a`` are actually equivalent. + example, if ``T`` is a variable and ``a`` is a variable of type + ``T``, then the commands ``Proof using a`` and ``Proof using T a`` + are equivalent. .. cmdv:: Proof using {+ @ident } with @tactic diff --git a/engine/namegen.ml b/engine/namegen.ml index 7ce759a3fb..db72dc8ec3 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -21,7 +21,6 @@ open Constr open Environ open EConstr open Vars -open Nametab open Nameops open Libnames open Globnames @@ -82,14 +81,14 @@ let is_imported_ref = function let is_global id = try - let ref = locate (qualid_of_ident id) in + let ref = Nametab.locate (qualid_of_ident id) in not (is_imported_ref ref) with Not_found -> false let is_constructor id = try - match locate (qualid_of_ident id) with + match Nametab.locate (qualid_of_ident id) with | ConstructRef _ -> true | _ -> false with Not_found -> @@ -116,7 +115,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *) | Cast (c,_,_) | App (c,_) -> hdrec c | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn))) | Const _ | Ind _ | Construct _ | Var _ as c -> - Some (basename_of_global (global_of_constr c)) + Some (Nametab.basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i) with Name id -> id | _ -> assert false) | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None @@ -148,8 +147,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn)) - | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") - | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> @@ -267,7 +266,7 @@ let visible_ids sigma (nenv, c) = begin try let gseen = GlobRef.Set_env.add g gseen in - let short = shortest_qualid_of_global Id.Set.empty g in + let short = Nametab.shortest_qualid_of_global Id.Set.empty g in let dir, id = repr_qualid short in let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in accu := (gseen, vseen, ids) diff --git a/engine/univGen.ml b/engine/univGen.ml index 23ab30eb75..130aa06f53 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -77,17 +77,14 @@ let fresh_global_instance ?loc ?names env gr = let u, ctx = fresh_global_instance ?loc ?names env gr in mkRef (gr, u), ctx -let constr_of_global gr = - let c, ctx = fresh_global_instance (Global.env ()) gr in - if not (Univ.ContextSet.is_empty ctx) then - if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then - (* Should be an error as we might forget constraints, allow for now - to make firstorder work with "using" clauses *) - c - else CErrors.user_err ~hdr:"constr_of_global" - Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ - str " would forget universes.") - else c +let constr_of_monomorphic_global gr = + if not (Global.is_polymorphic gr) then + fst (fresh_global_instance (Global.env ()) gr) + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") + +let constr_of_global gr = constr_of_monomorphic_global gr let constr_of_global_univ = mkRef diff --git a/engine/univGen.mli b/engine/univGen.mli index c2e9d0c696..42756701dc 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -74,11 +74,16 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> [@@ocaml.deprecated "Use [Univ.extend_in_context_set]"] (** Create a fresh global in the global environment, without side effects. - BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for - the proper way to get a fresh copy of a global reference. *) + the proper way to get a fresh copy of a polymorphic global reference. *) +val constr_of_monomorphic_global : GlobRef.t -> constr + val constr_of_global : GlobRef.t -> constr +[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\ + use [constr_of_monomorphic_global] if the reference is guaranteed to\ + be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"] (** Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. (side-effect on the diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 98e1f6dd36..601099c6ff 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -26,7 +26,6 @@ open Notation_ops open Glob_term open Glob_ops open Pattern -open Nametab open Notation open Detyping open Decl_kinds @@ -213,7 +212,7 @@ let is_record indsp = with Not_found -> false let encode_record r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in if not (is_record indsp) then user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); @@ -279,7 +278,7 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - shortest_qualid_of_global ?loc vars r + Nametab.shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -481,7 +480,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> - let qid = shortest_qualid_of_syndef ?loc vars kn in + let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(subentry,(scopt,scl))) -> extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) @@ -1136,7 +1135,7 @@ and extern_notation (custom,scopes as allscopes) vars t = function List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in - let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in + let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d7497d4e8e..6b22261a15 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -28,7 +28,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Nametab open Notation open Inductiveops open Decl_kinds @@ -633,7 +632,7 @@ let terms_of_binders bl = | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in + let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in @@ -721,7 +720,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = try let gc = intern nenv c in Id.Map.add id (gc, Some c) map - with GlobalizationError _ -> map + with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -986,7 +985,7 @@ let intern_extended_global_of_qualid qid = let intern_reference qid = let r = try intern_extended_global_of_qualid qid - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in Smartlocate.global_of_extended_global r @@ -1058,11 +1057,11 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qi (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (gvar (loc,qualid_basename qid) us, [], [], []), args - else error_global_not_found qid + else Nametab.error_global_not_found qid else let r,projapp,args2 = try intern_qualid qid intern env ntnvars us args - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 @@ -1312,7 +1311,7 @@ let sort_fields ~complete loc fields completer = (* the reference constructor of the record *) let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in - try shortest_qualid_of_global ?loc Id.Set.empty global_record_id + try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1493,7 +1492,7 @@ let drop_notations_pattern looked_for genv = in let rec drop_syndef top scopes qid pats = try - match locate_extended qid with + match Nametab.locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1550,7 +1549,7 @@ let drop_notations_pattern looked_for genv = | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (qid, Some expl_pl, pl) -> - let g = try locate qid + let g = try Nametab.locate qid with Not_found -> raise (InternalizationError (loc,NotAConstructor qid)) in if expl_pl == [] then diff --git a/interp/declare.ml b/interp/declare.ml index 07a0066ea8..7a32018c0e 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -60,14 +60,7 @@ let open_constant i ((sp,kn), obj) = if obj.cst_locl then () else let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con); - match (Global.lookup_constant con).const_body with - | (Def _ | Undef _) -> () - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with - | Some f when Future.is_val f -> - Global.push_context_set false (Future.force f) - | _ -> () + Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = variable_exists id || Global.exists_objlabel (Label.of_id id) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index e3d490a1ad..b73d238c22 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -15,7 +15,6 @@ open Names open Libnames open Libobject open Lib -open Nametab open Notation_term (* Syntactic definitions. *) @@ -38,7 +37,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = let is_alias_of_already_visible_name sp = function | _,NRef ref -> - let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in + let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in DirPath.is_empty dir && Id.equal id (basename sp) | _ -> false @@ -83,11 +82,11 @@ let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) let pr_compat_warning (kn, def, v) = let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r + | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r | _ -> strbrk " is a compatibility notation" in pr_syndef kn ++ pp_def diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index c74f2ab318..ac78064235 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -83,18 +83,27 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu = let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate) +let dep_order l2r k1 k2 = match k1, k2 with +| RelKey _, RelKey _ -> l2r +| RelKey _, (VarKey _ | ConstKey _) -> true +| VarKey _, RelKey _ -> false +| VarKey _, VarKey _ -> l2r +| VarKey _, ConstKey _ -> true +| ConstKey _, (RelKey _ | VarKey _) -> false +| ConstKey _, ConstKey _ -> l2r + (* Unfold the first constant only if it is "more transparent" than the second one. In case of tie, use the recommended default. *) let oracle_order f o l2r k1 k2 = match get_strategy o f k1, get_strategy o f k2 with - | Expand, Expand -> l2r + | Expand, Expand -> dep_order l2r k1 k2 | Expand, (Opaque | Level _) -> true | (Opaque | Level _), Expand -> false - | Opaque, Opaque -> l2r + | Opaque, Opaque -> dep_order l2r k1 k2 | Level _, Opaque -> true | Opaque, Level _ -> false | Level n1, Level n2 -> - if Int.equal n1 n2 then l2r + if Int.equal n1 n2 then dep_order l2r k1 k2 else n1 < n2 let get_strategy o = get_strategy o (fun x -> x) diff --git a/library/coqlib.ml b/library/coqlib.ml index 677515981a..a044a9a395 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -14,7 +14,6 @@ open Pp open Names open Libnames open Globnames -open Nametab let make_dir l = DirPath.make (List.rev_map Id.of_string l) @@ -79,7 +78,7 @@ let register_ref s c = (* Generic functions to find Coq objects *) let has_suffix_in_dirs dirs ref = - let dir = dirpath (path_of_global ref) in + let dir = dirpath (Nametab.path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs let gen_reference_in_modules locstr dirs s = diff --git a/man/coq-interface.1 b/man/coq-interface.1 deleted file mode 100644 index ee013d952e..0000000000 --- a/man/coq-interface.1 +++ /dev/null @@ -1,37 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coq\-interface \- Customized Coq toplevel to make user interfaces - - -.SH SYNOPSIS -.B coq-interface -[ -.B options -] - -.SH DESCRIPTION - -.B coq-interface -is a Coq customized toplevel system for Coq containing some modules -useful for the graphical interface. This program is not for the casual -user. - -.SH OPTIONS - -.TP -.B \-h -Help. Will give you the complete list of options accepted by -coq-interface (the same as coqtop). - -.SH SEE ALSO - -.BR coqc (1), -.BR coqdep (1), -.BR coqtop (1), -.BR coq\-parser (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr diff --git a/man/coq-parser.1 b/man/coq-parser.1 deleted file mode 100644 index 23dc820193..0000000000 --- a/man/coq-parser.1 +++ /dev/null @@ -1,30 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coq\-parser \- Coq parser - - -.SH SYNOPSIS -.B coq\-parser -[ -.B options -] - -.SH DESCRIPTION - -.B parser -is a program reading Coq proof developments and outputing them in the -structured format given in the INRIA technical report RT154. This -program is not for the casual user. - -.SH SEE ALSO - -.BR coq\-interface (1), -.BR coqc (1), -.BR coqtop (1), -.BR coqdep (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr diff --git a/man/dune b/man/dune new file mode 100644 index 0000000000..359e780545 --- /dev/null +++ b/man/dune @@ -0,0 +1,10 @@ +(install + (section man) + (package coq) + (files coqc.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqchk.1 coqdep.1 coqdoc.1 coq_makefile.1 coq-tex.1 coqwc.1)) + +(install + (section man) + (package coqide) + (files coqide.1)) + diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml index 9c421f5b76..2230dfc47c 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml @@ -229,9 +229,11 @@ let unlocated f x = f x (* try f x with Loc.Exc_located (_, exc) -> raise exc *) let check_keyword str = - let rec loop_symb = parser - | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str - | [< s >] -> + let rec loop_symb s = match Stream.peek s with + | Some (' ' | '\n' | '\r' | '\t' | '"') -> + Stream.junk s; + bad_token str + | _ -> match unlocated lookup_utf8 Ploc.dummy s with | Utf8Token (_,n) -> njunk n s; loop_symb s | AsciiChar -> Stream.junk s; loop_symb s @@ -240,12 +242,14 @@ let check_keyword str = loop_symb (Stream.of_string str) let check_ident str = - let rec loop_id intail = parser - | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] -> + let rec loop_id intail s = match Stream.peek s with + | Some ('a'..'z' | 'A'..'Z' | '_') -> + Stream.junk s; loop_id true s - | [< ' ('0'..'9' | ''') when intail; s >] -> + | Some ('0'..'9' | '\'') when intail -> + Stream.junk s; loop_id true s - | [< s >] -> + | _ -> match unlocated lookup_utf8 Ploc.dummy s with | Utf8Token (st, n) when not intail && Unicode.is_valid_ident_initial st -> njunk n s; loop_id true s | Utf8Token (st, n) when intail && Unicode.is_valid_ident_trailing st -> @@ -308,10 +312,11 @@ let warn_unrecognized_unicode = strbrk (Printf.sprintf "Not considering unicode character \"%s\" of unknown \ lexical status as part of identifier \"%s\"." u id)) -let rec ident_tail loc len = parser - | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] -> +let rec ident_tail loc len s = match Stream.peek s with + | Some ('a'..'z' | 'A'..'Z' | '0'..'9' | '\'' | '_' as c) -> + Stream.junk s; ident_tail loc (store len c) s - | [< s >] -> + | _ -> match lookup_utf8 loc s with | Utf8Token (st, n) when Unicode.is_valid_ident_trailing st -> ident_tail loc (nstore n len s) s @@ -321,9 +326,9 @@ let rec ident_tail loc len = parser warn_unrecognized_unicode ~loc:!@loc (u,id); len | _ -> len -let rec number len = parser - | [< ' ('0'..'9' as c); s >] -> number (store len c) s - | [< >] -> len +let rec number len s = match Stream.peek s with + | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s + | _ -> len let warn_comment_terminator_in_string = CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing" @@ -335,31 +340,43 @@ let warn_comment_terminator_in_string = (* If the string being lexed is in a comment, [comm_level] is Some i with i the current level of comments nesting. Otherwise, [comm_level] is None. *) -let rec string loc ~comm_level bp len = parser - | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> +let rec string loc ~comm_level bp len s = match Stream.peek s with + | Some '"' -> + Stream.junk s; + let esc = + match Stream.peek s with + Some '"' -> Stream.junk s; true + | _ -> false + in if esc then string loc ~comm_level bp (store len '"') s else (loc, len) - | [< ''('; s >] -> - (parser - | [< ''*'; s >] -> + | Some '(' -> + Stream.junk s; + (fun s -> match Stream.peek s with + | Some '*' -> + Stream.junk s; let comm_level = Option.map succ comm_level in string loc ~comm_level bp (store (store len '(') '*') s - | [< >] -> + | _ -> string loc ~comm_level bp (store len '(') s) s - | [< ''*'; s >] -> - (parser - | [< '')'; s >] -> + | Some '*' -> + Stream.junk s; + (fun s -> match Stream.peek s with + | Some ')' -> + Stream.junk s; let () = match comm_level with | Some 0 -> - warn_comment_terminator_in_string ~loc:!@loc () + warn_comment_terminator_in_string ~loc:!@loc () | _ -> () in let comm_level = Option.map pred comm_level in string loc ~comm_level bp (store (store len '*') ')') s - | [< >] -> + | _ -> string loc ~comm_level bp (store len '*') s) s - | [< ''\n' as c; s >] ep -> + | Some ('\n' as c) -> + Stream.junk s; + let ep = Stream.count s in (* If we are parsing a comment, the string if not part of a token so we update the first line of the location. Otherwise, we update the last line. *) @@ -368,8 +385,12 @@ let rec string loc ~comm_level bp len = parser else bump_loc_line_last loc ep in string loc ~comm_level bp (store len c) s - | [< 'c; s >] -> string loc ~comm_level bp (store len c) s - | [< _ = Stream.empty >] ep -> + | Some c -> + Stream.junk s; + string loc ~comm_level bp (store len c) s + | _ -> + let _ = Stream.empty s in + let ep = Stream.count s in let loc = set_loc_pos loc bp ep in err loc Unterminated_string @@ -441,25 +462,50 @@ let comment_stop ep = comment_begin := None; between_commands := false -let rec comment loc bp = parser bp2 - | [< ''('; - loc = (parser - | [< ''*'; s >] -> push_string "(*"; comment loc bp s - | [< >] -> push_string "("; loc ); - s >] -> comment loc bp s - | [< ''*'; - loc = parser - | [< '')' >] -> push_string "*)"; loc - | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc - | [< ''"'; s >] -> +let rec comment loc bp s = + let bp2 = Stream.count s in + match Stream.peek s with + Some '(' -> + Stream.junk s; + let loc = + try + match Stream.peek s with + Some '*' -> + Stream.junk s; + push_string "(*"; comment loc bp s + | _ -> push_string "("; loc + with Stream.Failure -> raise (Stream.Error "") + in + comment loc bp s + | Some '*' -> + Stream.junk s; + begin try + match Stream.peek s with + Some ')' -> Stream.junk s; push_string "*)"; loc + | _ -> real_push_char '*'; comment loc bp s + with Stream.Failure -> raise (Stream.Error "") + end + | Some '"' -> + Stream.junk s; let loc, len = string loc ~comm_level:(Some 0) bp2 0 s in push_string "\""; push_string (get_buff len); push_string "\""; comment loc bp s - | [< _ = Stream.empty >] ep -> + | _ -> + match try Some (Stream.empty s) with Stream.Failure -> None with + | Some _ -> + let ep = Stream.count s in let loc = set_loc_pos loc bp ep in err loc Unterminated_comment - | [< ''\n' as z; s >] ep -> real_push_char z; comment (bump_loc_line loc ep) bp s - | [< 'z; s >] -> real_push_char z; comment loc bp s + | _ -> + match Stream.peek s with + Some ('\n' as z) -> + Stream.junk s; + let ep = Stream.count s in + real_push_char z; comment (bump_loc_line loc ep) bp s + | Some z -> + Stream.junk s; + real_push_char z; comment loc bp s + | _ -> raise Stream.Failure (* Parse a special token, using the [token_tree] *) @@ -526,12 +572,16 @@ let process_chars loc bp c cs = (* Parse what follows a dot *) -let parse_after_dot loc c bp = - parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d); s >] -> +let parse_after_dot loc c bp s = match Stream.peek s with + | Some ('a'..'z' | 'A'..'Z' | '_' as d) -> + Stream.junk s; + let len = + try ident_tail loc (store 0 d) s with + Stream.Failure -> raise (Stream.Error "") + in let field = get_buff len in (try find_keyword loc ("."^field) s with Not_found -> FIELD field) - | [< s >] -> + | _ -> match lookup_utf8 loc s with | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in @@ -559,12 +609,23 @@ let blank_or_eof cs = (* Parse a token in a char stream *) -let rec next_token loc = parser bp - | [< ''\n' as c; s >] ep -> +let rec next_token loc s = + let bp = Stream.count s in + match Stream.peek s with + | Some ('\n' as c) -> + Stream.junk s; + let ep = Stream.count s in comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s - | [< '' ' | '\t' | '\r' as c; s >] -> + | Some (' ' | '\t' | '\r' as c) -> + Stream.junk s; comm_loc bp; push_char c; next_token loc s - | [< ''.' as c; t = parse_after_dot loc c bp; s >] ep -> + | Some ('.' as c) -> + Stream.junk s; + let t = + try parse_after_dot loc c bp s with + Stream.Failure -> raise (Stream.Error "") + in + let ep = Stream.count s in comment_stop bp; (* We enforce that "." should either be part of a larger keyword, for instance ".(", or followed by a blank or eof. *) @@ -575,42 +636,68 @@ let rec next_token loc = parser bp between_commands := true; | _ -> () in - (t, set_loc_pos loc bp ep) - | [< ' ('-'|'+'|'*' as c); s >] -> + t, set_loc_pos loc bp ep + | Some ('-' | '+' | '*' as c) -> + Stream.junk s; let t,new_between_commands = if !between_commands then process_sequence loc bp c s, true else process_chars loc bp c s,false in comment_stop bp; between_commands := new_between_commands; t - | [< ''?'; s >] ep -> + | Some '?' -> + Stream.junk s; + let ep = Stream.count s in let t = parse_after_qmark loc bp s in comment_stop bp; (t, set_loc_pos loc bp ep) - | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); - len = ident_tail loc (store 0 c); s >] ep -> + | Some ('a'..'z' | 'A'..'Z' | '_' as c) -> + Stream.junk s; + let len = + try ident_tail loc (store 0 c) s with + Stream.Failure -> raise (Stream.Error "") + in + let ep = Stream.count s in let id = get_buff len in comment_stop bp; (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep - | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> + | Some ('0'..'9' as c) -> + Stream.junk s; + let len = + try number (store 0 c) s with + Stream.Failure -> raise (Stream.Error "") + in + let ep = Stream.count s in comment_stop bp; (INT (get_buff len), set_loc_pos loc bp ep) - | [< ''\"'; (loc,len) = string loc ~comm_level:None bp 0 >] ep -> + | Some '\"' -> + Stream.junk s; + let (loc, len) = + try string loc ~comm_level:None bp 0 s with + Stream.Failure -> raise (Stream.Error "") + in + let ep = Stream.count s in comment_stop bp; (STRING (get_buff len), set_loc_pos loc bp ep) - | [< ' ('(' as c); - t = parser - | [< ''*'; s >] -> + | Some ('(' as c) -> + Stream.junk s; + begin try + match Stream.peek s with + | Some '*' -> + Stream.junk s; comm_loc bp; push_string "(*"; let loc = comment loc bp s in next_token loc s - | [< t = process_chars loc bp c >] -> comment_stop bp; t >] -> - t - | [< ' ('{' | '}' as c); s >] ep -> + | _ -> let t = process_chars loc bp c s in comment_stop bp; t + with Stream.Failure -> raise (Stream.Error "") + end + | Some ('{' | '}' as c) -> + Stream.junk s; + let ep = Stream.count s in let t,new_between_commands = if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true else process_chars loc bp c s, false in comment_stop bp; between_commands := new_between_commands; t - | [< s >] -> + | _ -> match lookup_utf8 loc s with | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in diff --git a/parsing/dune b/parsing/dune index b70612a52b..f931321358 100644 --- a/parsing/dune +++ b/parsing/dune @@ -5,11 +5,6 @@ (libraries proofs)) (rule - (targets cLexer.ml) - (deps (:ml4-file cLexer.ml4)) - (action (run camlp5o -loc loc -impl %{ml4-file} -o %{targets}))) - -(rule (targets g_prim.ml) (deps (:mlg-file g_prim.mlg)) (action (run coqpp %{mlg-file}))) diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index b9ad1ff6d8..07f50f6cd5 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -10,7 +10,7 @@ open Constr -let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n) +let bt_lib_constr n = lazy (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref n) let decomp_term sigma (c : Constr.t) = Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 8fa676de44..b0c4785d7a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -233,12 +233,11 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) -let constant str = UnivGen.constr_of_global - @@ Coqlib.lib_ref str +let constant str = Coqlib.lib_ref str let defined_connectives = lazy - [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type"))); - AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))] + [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type")); + AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 98d68d3db7..ad1114b733 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in - let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in - let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in + let coq_False = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type") in + let coq_True = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.type") in + let coq_I = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in @@ -1605,7 +1605,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 03a64988e4..a385a61ae0 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -116,7 +116,7 @@ let def_of_const t = [@@@ocaml.warning "-3"] let coq_constant s = - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -441,7 +441,7 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) @@ -449,7 +449,7 @@ let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) @@ -463,7 +463,7 @@ let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") [@@@ocaml.warning "-3"] -let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ +let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" [@@@ocaml.warning "+3"] diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b8973a18dc..b0842c3721 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")) + EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) with _ -> assert false (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] @@ -511,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ca3160f4c4..f9df3aed45 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -51,7 +51,7 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) [@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "RecursiveDefinition" m s let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] @@ -63,7 +63,7 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) [@@@ocaml.warning "+3"] @@ -97,7 +97,7 @@ let type_of_const sigma t = Typeops.type_of_constant_in (Global.env()) (sp, u) |_ -> assert false -let constant sl s = constr_of_global (find_reference sl s) +let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s) let const_of_ref = function ConstRef kn -> kn @@ -1241,7 +1241,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in + let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 1f2c722b34..a88285c9ee 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -115,7 +115,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = (* Summary and Object declaration *) -open Nametab open Libobject type ltac_entry = { @@ -153,19 +152,19 @@ let tac_deprecation kn = let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Until i) sp kn in + let () = if not local then push_tactic (Nametab.Until i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Exactly i) sp kn in + let () = if not local then push_tactic (Nametab.Exactly i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with | None -> - let () = push_tactic (Until 1) sp kn in + let () = push_tactic (Nametab.Until 1) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 5501cf92a5..55412c74bb 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -19,7 +19,6 @@ open Util open Names open Libnames open Globnames -open Nametab open Smartlocate open Constrexpr open Termops @@ -98,7 +97,7 @@ let intern_global_reference ist qid = ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) else try ArgArg (qid.CAst.loc,locate_global_with_alias qid) - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid let intern_ltac_variable ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then @@ -150,7 +149,7 @@ let intern_isolated_tactic_reference strict ist qid = try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Internalize an applied tactic reference *) @@ -169,7 +168,7 @@ let intern_applied_tactic_reference ist qid = try intern_applied_global_tactic_reference qid with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Intern a reference parsed in a non-tactic entry *) @@ -190,7 +189,7 @@ let intern_non_tactic_reference strict ist qid = TacGeneric ipat else (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -302,7 +301,7 @@ let intern_evaluable_global_reference ist qid = try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) with Not_found -> if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) - else error_global_not_found qid + else Nametab.error_global_not_found qid let intern_evaluable_reference_or_by_notation ist = function | {v=AN r} -> intern_evaluable_global_reference ist r @@ -377,7 +376,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f90e889678..b60b77595b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -23,7 +23,6 @@ open Names open Nameops open Libnames open Globnames -open Nametab open Refiner open Tacmach.New open Tactic_debug @@ -358,7 +357,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -374,14 +373,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (qualid_of_ident ?loc id) + | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -640,7 +639,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found (qualid_of_ident ?loc id)) + Nametab.error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/plugin_base.dune index 0ae0e6855d..c2d396f0f9 100644 --- a/plugins/micromega/plugin_base.dune +++ b/plugins/micromega/plugin_base.dune @@ -5,3 +5,11 @@ (modules (:standard \ csdpcert)) (synopsis "Coq's micromega plugin") (libraries num coq.plugins.ltac)) + +(executable + (name csdpcert) + (public_name csdpcert) + (package coq) + (modules csdpcert) + (flags :standard -open Micromega_plugin) + (libraries coq.plugins.micromega)) diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 11d0a4a44d..ef60a23e80 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -135,7 +135,7 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) let tpexpr = gen_constant "plugins.setoid_ring.pexpr" let ttconst = gen_constant "plugins.setoid_ring.const" @@ -540,7 +540,7 @@ let nsatz lpol = let return_term t = let a = - mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in + mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 09bd4cd352..d8adb17710 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -186,7 +186,8 @@ let reset_all () = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_global |> EConstr.of_constr) +let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global + |> EConstr.of_constr) (* Zarith *) diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 79418da27c..840a05e02b 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -26,11 +26,11 @@ let step_count = ref 0 let node_count = ref 0 -let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -let li_and = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type")) -let li_or = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type")) +let li_False = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) +let li_and = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type")) +let li_or = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.or.type")) -let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) let l_xI = gen_constant "num.pos.xI" let l_xO = gen_constant "num.pos.xO" diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9585826109..8dbef47fe1 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -206,7 +206,7 @@ let exec_tactic env evd n f args = let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd -let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n))) +let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))) let gen_reference n = lazy (Coqlib.lib_ref n) let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory" @@ -251,7 +251,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) [@@ocaml.warning "-3"] let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) @@ -901,7 +901,7 @@ let ftheory_to_obj : field_info -> obj = let field_equality evd r inv req = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in + let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 1492cfb4e4..6746eff223 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1220,7 +1220,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) + (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b026397abf..73141191cf 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -15,7 +15,6 @@ open Names open Constr open Libnames open Globnames -open Nametab open Libobject open Mod_subst @@ -228,14 +227,14 @@ let string_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" | CL_CONST sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_PROJ sp -> let sp = Projection.Repr.constant sp in - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_IND sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp)) | CL_SECVAR sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp)) let pr_class x = str (string_of_class x) @@ -520,7 +519,7 @@ module CoercionPrinting = let compare = GlobRef.Ordered.compare let encode = coercion_of_reference let subst = subst_coe_typ - let printer x = pr_global_env Id.Set.empty x + let printer x = Nametab.pr_global_env Id.Set.empty x let key = ["Printing";"Coercion"] let title = "Explicitly printed coercions: " let member_message x b = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 592057ab41..072ac9deed 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -25,7 +25,6 @@ open Termops open Namegen open Libnames open Globnames -open Nametab open Mod_subst open Decl_kinds open Context.Named.Declaration @@ -58,7 +57,7 @@ let add_name_opt na b t (nenv, env) = (* Tools for printing of Cases *) let encode_inductive r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in let constr_lengths = constructors_nrealargs indsp in (indsp,constr_lengths) @@ -97,7 +96,7 @@ module PrintingInductiveMake = let compare = ind_ord let encode = Test.encode let subst subst obj = subst_ind subst obj - let printer ind = pr_global_env Id.Set.empty (IndRef ind) + let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) let key = ["Printing";Test.field] let title = Test.title let member_message x = Test.member_message (printer x) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index e49ba75b3f..89f64d328a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -29,7 +29,6 @@ open Inductive open Inductiveops open Environ open Reductionops -open Nametab open Context.Rel.Declaration type dep_flag = bool @@ -618,6 +617,6 @@ let lookup_eliminator ind_sp s = user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ Id.print id ++ strbrk ", the elimination of the inductive definition " ++ - pr_global_env Id.Set.empty (IndRef ind_sp) ++ + Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++ strbrk " on sort " ++ Termops.pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f8dc5ba4d6..5d74b59b27 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -20,7 +20,6 @@ open Util open Pp open Names open Globnames -open Nametab open Constr open Libobject open Mod_subst @@ -330,7 +329,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let error_not_structure ref description = user_err ~hdr:"object_declare" (str"Could not declare a canonical structure " ++ - (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ + (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++ description)) let check_and_decompose_canonical_structure ref = diff --git a/printing/printer.ml b/printing/printer.ml index 990bdaad7d..3cf995a005 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -15,7 +15,6 @@ open Names open Constr open Environ open Globnames -open Nametab open Evd open Refiner open Constrextern @@ -242,7 +241,7 @@ let pr_abstract_cumulativity_info sigma cumi = (**********************************************************************) (* Global references *) -let pr_global_env = pr_global_env +let pr_global_env = Nametab.pr_global_env let pr_global = pr_global_env Id.Set.empty let pr_universe_instance evd inst = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5d1faf1465..388bf8efb5 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -68,7 +68,10 @@ let pf_ids_set_of_hyps gls = let pf_get_new_id id gls = next_ident_away id (pf_ids_set_of_hyps gls) -let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) +let pf_global gls id = + let env = pf_env gls in + let sigma = project gls in + Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 3432ad4afa..f302960870 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,7 +34,7 @@ val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list -val pf_global : goal sigma -> Id.t -> constr +val pf_global : goal sigma -> Id.t -> evar_map * constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v new file mode 100644 index 0000000000..b10569499e --- /dev/null +++ b/test-suite/bugs/closed/bug_8785.v @@ -0,0 +1,44 @@ +Universe u v w. +Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := . + +Inductive FiniteT : Type -> Prop := + | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T) + | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X -> + invertible f -> FiniteT Y. + +Set Printing Universes. + +Axiom a : False. +(* +Constraint v <= u. +Constraint v <= w. +*) +Lemma finite_subtype: forall (X:Type) (P:X->Prop), + FiniteT X -> (forall x:X, P x \/ ~ P x) -> + FiniteT {x:X | P x}. +Proof. +intros. +induction H. + +destruct (H0 None). +elim a. + +pose (g := fun (x:{x:T | P (Some x)}) => + match x return {x:option T | P x} with + | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +pose (g := fun (x:{x:X | P (f x)}) => + match x with + | exist _ x0 i => exist (fun x:Y => P x) (f x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +Qed. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index d91c4f0b34..7bb1390cad 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -46,7 +46,7 @@ let usage_coq_makefile () = \n\ \n[file.v]: Coq file to be compiled\ \n[file.ml[i4]?]: Objective Caml file to be compiled\ -\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ +\n[file.ml{lib,pack}]: ocamlbuild-style file that describes a Objective Caml\ \n library/module\ \n[any] : subdirectory that should be \"made\" and has a Makefile itself\ \n to do so. Very fragile and discouraged.\ diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 148d4437fa..9f71def8fc 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -63,20 +63,20 @@ exception ConstructorWithNonParametricInductiveType of inductive exception DecidabilityIndicesNotSupported (* Some pre declaration of constant we are going to use *) -let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb_prop") +let andb_prop = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb_prop") let andb_true_intro = fun _ -> - UnivGen.constr_of_global + UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb_true_intro") (* We avoid to use lazy as the binding of constants can change *) -let bb () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.type") -let tt () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.true") -let ff () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.false") -let eq () = UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type") +let bb () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.type") +let tt () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.true") +let ff () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.false") +let eq () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type") -let sumbool () = UnivGen.constr_of_global (Coqlib.lib_ref "core.sumbool.type") -let andb = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb") +let sumbool () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.sumbool.type") +let andb = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb") let induct_on c = induction false None c None None let destruct_on c = destruct false None c None None @@ -873,7 +873,7 @@ let compute_dec_goal ind lnamesparrec nparrec = create_input ( mkNamedProd n (mkFullInd ind (2*nparrec)) ( mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( - mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) ) ) ) diff --git a/vernac/class.ml b/vernac/class.ml index 614b2181d9..526acd40b5 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -21,7 +21,6 @@ open Environ open Classops open Declare open Globnames -open Nametab open Decl_kinds let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL @@ -310,7 +309,7 @@ let add_coercion_hook poly local ref = | Global -> false in let () = try_add_new_coercion ref ~local poly in - let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in + let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) diff --git a/vernac/classes.ml b/vernac/classes.ml index 3cf5e9bfdf..52c1e1cf98 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -12,7 +12,6 @@ module CVars = Vars open Names open EConstr -open Nametab open CErrors open Util open Typeclasses_errors @@ -67,7 +66,7 @@ let intern_info {hint_priority;hint_pattern} = (** TODO: add subinstances *) let existing_instance glob g info = - let c = global g in + let c = Nametab.global g in let info = Option.default Hints.empty_hint_info info in let info = intern_info info in let instance, _ = Global.type_of_global_in_context (Global.env ()) c in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 7b28895814..885a22b209 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -22,7 +22,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Nametab open Impargs open Reductionops open Indtypes @@ -575,6 +574,6 @@ let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite = (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 5f2818c12b..4efbb968fb 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -33,7 +33,6 @@ open Globnames open Goptions open Nameops open Termops -open Nametab open Smartlocate open Vernacexpr open Ind_tables @@ -369,7 +368,7 @@ requested | InSet -> recs ^ "_nodep" | InType -> recs ^ "t_nodep") ) in - let newid = add_suffix (basename_of_global (IndRef ind)) suffix in + let newid = add_suffix (Nametab.basename_of_global (IndRef ind)) suffix in let newref = CAst.make newid in ((newref,isdep,ind,z)::l1),l2 in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 0ac97a74e4..fbf552e649 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -266,7 +266,7 @@ let eterm_obligations env name evm fs ?status t ty = let hide_obligation () = Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - UnivGen.constr_of_global (Coqlib.lib_ref "program.tactics.obligation") + UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation") let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) diff --git a/vernac/search.ml b/vernac/search.ml index 04dcb7d565..2273130668 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -18,7 +18,6 @@ open Environ open Pattern open Libnames open Globnames -open Nametab module NamedDecl = Context.Named.Declaration @@ -192,7 +191,7 @@ let rec head_filter pat ref env sigma typ = | _ -> false let full_name_of_reference ref = - let (dir,id) = repr_path (path_of_global ref) in + let (dir,id) = repr_path (Nametab.path_of_global ref) in DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) @@ -204,14 +203,14 @@ let blacklist_filter_aux () = List.for_all is_not_bl l let module_filter (mods, outside) ref env typ = - let sp = path_of_global ref in + let sp = Nametab.path_of_global ref in let sl = dirpath sp in let is_outside md = not (is_dirpath_prefix_of md sl) in let is_inside md = is_dirpath_prefix_of md sl in if outside then List.for_all is_outside mods else List.is_empty mods || List.exists is_inside mods -let name_of_reference ref = Id.to_string (basename_of_global ref) +let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) let search_about_filter query gr env typ = match query with | GlobSearchSubPattern pat -> |