diff options
64 files changed, 162 insertions, 157 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f418df3d75..7c9a5c9a31 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -10,7 +10,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-07-05-V33" + CACHEKEY: "bionic_coq-V2019-07-06-V22" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -9,7 +9,7 @@ WHAT DO YOU NEED ? - OCaml (version >= 4.05.0) (available at https://ocaml.org/) - (This version of Coq has been tested up to OCaml 4.07.0) + (This version of Coq has been tested up to OCaml 4.08.0) - The Num package, which used to be part of the OCaml standard library, if you are using an OCaml version >= 4.06.0 diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 54d6b4b7c8..fd99dc6d18 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -52,9 +52,14 @@ jobs: - script: | set -e brew update + (cd $(brew --repository)/Library/Taps/homebrew/homebrew-core/ && git fetch --shallow-since=${HBCORE_DATE} && git checkout ${HBCORE_REF}) brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme pip3 install macpack displayName: 'Install system dependencies' + env: + HOMEBREW_NO_AUTO_UPDATE: "1" + HBCORE_DATE: "2019-06-18" + HBCORE_REF: "944a5b7d83e4b81c749d93831b514607bdd2b6a1" - script: | set -e @@ -67,7 +72,7 @@ jobs: opam list displayName: 'Install OCaml dependencies' env: - COMPILER: "4.07.1" + COMPILER: "4.08.0" FINDLIB_VER: ".1.8.0" OPAMYES: "true" diff --git a/checker/analyze.ml b/checker/analyze.ml index 77e70318dd..e145988b4f 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -395,8 +395,8 @@ end module IChannel = struct type t = in_channel - let input_byte = Pervasives.input_byte - let input_binary_int = Pervasives.input_binary_int + let input_byte = input_byte + let input_binary_int = input_binary_int end module IString = diff --git a/checker/check.ml b/checker/check.ml index 2840fc9ad6..ecf84fda9c 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -66,7 +66,7 @@ module LibraryOrdered = struct type t = DirPath.t let compare d1 d2 = - Pervasives.compare + compare (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) end @@ -377,7 +377,7 @@ let intern_from_file ~intern_mode (dir, f) = let get_deps (dir, f) = try LibraryMap.find dir !depgraph with Not_found -> - let _ = intern_from_file (dir,f) in + let _ = intern_from_file ~intern_mode:Dep (dir,f) in LibraryMap.find dir !depgraph (* Read a compiled library and all dependencies, in reverse order. diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 9448a03f4f..34d748e1cc 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c +OPAM_VARIANT=ocaml-variants.4.08.0+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8b4af9b63f..011c7fbdec 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-07-05-V33" +# CACHEKEY: "bionic_coq-V2019-07-06-V22" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # We need to install OPAM 2.0 manually for now. -RUN wget https://github.com/ocaml/opam/releases/download/2.0.3/opam-2.0.3-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam +RUN wget https://github.com/ocaml/opam/releases/download/2.0.4/opam-2.0.4-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam # Basic OPAM setup ENV NJOBS="2" \ @@ -37,8 +37,9 @@ 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.6.2 ounit.2.0.8 odoc.1.4.0" \ - CI_OPAM="menhir.20190626 elpi.1.4.0 ocamlgraph.1.8.8" +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.10.0 ounit.2.0.8 odoc.1.4.0" \ + CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ + BASE_ONLY_OPAM="elpi.1.4.0" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" @@ -48,16 +49,16 @@ ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" # base switch RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ - opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM + opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM # base+32bit switch RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.07.1" \ - COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" \ - BASE_OPAM_EDGE="dune-release.1.1.0" +ENV COMPILER_EDGE="4.08.0" \ + COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta6" \ + BASE_OPAM_EDGE="dune-release.1.3.1" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index cf95941de5..c7f36ee964 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -3,5 +3,5 @@ ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.07.1))) -(context (opam (switch 4.07.1+flambda))) +(context (opam (switch 4.08.0))) +(context (opam (switch 4.08.0+flambda))) diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 425f21de70..c0a3eeb11c 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -209,7 +209,8 @@ has_state() { [ "$(jq -rc 'map(select(.user.login == "'"$1"'") | .state) | any(. == "'"$2"'")' <<< "$reviews")" = true ] } -for reviewer in $(jq -rc 'map(.user.login) | unique | join(" ")' <<< "$reviews" ); do +author=$(echo "$PRDATA" | jq -rc '.user.login') +for reviewer in $(jq -rc 'map(.user.login | select(. != "'"$author"'")) | unique | join(" ")' <<< "$reviews" ); do if has_state "$reviewer" APPROVED; then msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Reviewed-by="$reviewer") elif has_state "$reviewer" COMMENTED; then diff --git a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst new file mode 100644 index 0000000000..8bfd01d7a0 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst @@ -0,0 +1,5 @@ +- Coq now officially supports OCaml 4.08. + + see INSTALL files for details + (`#10471 <https://github.com/coq/coq/pull/10471>`_, + by Emilio Jesús Gallego Arias). diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 911b189deb..ea71be8e43 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -331,11 +331,16 @@ let push_rel_decl_to_named_context let map_decl f d = NamedDecl.map_constr f d in - let replace_var_named_declaration id0 id decl = - let id' = NamedDecl.get_id decl in - let id' = if Id.equal id0 id' then id else id' in - let vsubst = [id0 , mkVar id] in - decl |> NamedDecl.set_id id' |> map_decl (replace_vars vsubst) + let rec replace_var_named_declaration id0 id = function + | [] -> [] + | decl :: nc -> + if Id.equal id0 (NamedDecl.get_id decl) then + (* Stop here, the variable cannot occur before its definition *) + (NamedDecl.set_id id decl) :: nc + else + let nc = replace_var_named_declaration id0 id nc in + let vsubst = [id0 , mkVar id] in + map_decl (fun c -> replace_vars vsubst c) decl :: nc in let extract_if_neq id = function | Anonymous -> None @@ -366,7 +371,7 @@ let push_rel_decl_to_named_context context. Unless [id] is a section variable. *) let subst = update_var id0 id subst in let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in - let nc = List.map (replace_var_named_declaration id0 id) nc in + let nc = replace_var_named_declaration id0 id nc in (push_var id0 subst, Id.Set.add id avoid, d :: nc) | Some id0 when hypnaming = FailIfConflict -> user_err Pp.(Id.print id0 ++ str " is already used.") diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 2354d2c5e8..7c06bb59f1 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -41,7 +41,7 @@ let _ = CErrors.register_handler begin function | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!") | Exception e -> CErrors.print e | TacticFailure e -> CErrors.print e - | _ -> Pervasives.raise CErrors.Unhandled + | _ -> raise CErrors.Unhandled end (** {6 Non-logical layer} *) @@ -70,11 +70,11 @@ struct let map f a = (); fun () -> f (a ()) end) - type 'a ref = 'a Pervasives.ref + type 'a ref = 'a Util.pervasives_ref let ignore a = (); fun () -> ignore (a ()) - let ref a = (); fun () -> Pervasives.ref a + let ref a = (); fun () -> ref a (** [Pervasives.(:=)] *) let (:=) r a = (); fun () -> r := a @@ -93,7 +93,7 @@ struct let (src, info) = CErrors.push src in h (e, info) () - let read_line = fun () -> try Pervasives.read_line () with e -> + let read_line = fun () -> try read_line () with e -> let (e, info) = CErrors.push e in raise ~info e () let print_char = fun c -> (); fun () -> print_char c diff --git a/engine/proofview.ml b/engine/proofview.ml index c4a624e462..8b5bd4cd80 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -542,7 +542,7 @@ let tclDISPATCHGEN join tacs = let tacs = CList.map branch tacs in InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs) -let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs +let tclDISPATCH tacs = tclDISPATCHGEN ignore tacs let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs @@ -910,7 +910,7 @@ let tclPROGRESS t = exception Timeout let _ = CErrors.register_handler begin function | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") - | _ -> Pervasives.raise CErrors.Unhandled + | _ -> raise CErrors.Unhandled end let tclTIMEOUT n t = diff --git a/ide/idetop.ml b/ide/idetop.ml index 02682e2ee9..7c6fa8951b 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -392,7 +392,7 @@ let handle_exn (e, info) = let loc_of e = match Loc.get_loc e with | Some loc -> Some (Loc.unloc loc) | _ -> None in - let mk_msg () = CErrors.print ~info e in + let mk_msg () = CErrors.iprint (e,info) in match e with | e -> match Stateid.get info with diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml index 507b985d2f..463d93af0d 100644 --- a/ide/protocol/richpp.ml +++ b/ide/protocol/richpp.ml @@ -94,7 +94,7 @@ let rich_pp width ppcmds = print_close_tag = ignore; } in - pp_set_formatter_tag_functions ft tag_functions; + pp_set_formatter_tag_functions ft tag_functions [@warning "-3"]; pp_set_mark_tags ft true; (* Setting the formatter *) @@ -107,9 +107,9 @@ let rich_pp width ppcmds = (* The whole output must be a valid document. To that end, we nest the document inside <pp> tags. *) pp_open_box ft 0; - pp_open_tag ft "pp"; + pp_open_tag ft "pp" [@warning "-3"]; Pp.(pp_with ft ppcmds); - pp_close_tag ft (); + pp_close_tag ft () [@warning "-3"]; pp_close_box ft (); (* Get the resulting XML tree. *) diff --git a/ide/session.ml b/ide/session.ml index 3792730455..a9c106a765 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -275,9 +275,9 @@ let make_table_widget ?sort cd cb = let make_sorting i (_, c) = let sort (store : GTree.model) it1 it2 = match c with | `IntC c -> - Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) | `StringC c -> - Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) in store#set_sort_func i sort in diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 7758d89ed8..98390e810f 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -15,7 +15,7 @@ struct (* we use first size, then usual comparison *) let d = String.length s1 - String.length s2 in if d <> 0 then d - else Pervasives.compare s1 s2 + else compare s1 s2 end module Proposals = Set.Make(StringOrd) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8573dccdf9..e32ef3fe38 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -69,7 +69,7 @@ let print_no_symbol = ref false (* Turning notations and scopes on and off for printing *) module IRuleSet = Set.Make(struct type t = interp_rule - let compare x y = Pervasives.compare x y + let compare x y = compare x y end) let inactive_notations_table = diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index dc6a1ae180..0ec8b1e0c8 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -12,13 +12,13 @@ open Util (* Dump of globalization (to be used by coqdoc) *) -let glob_file = ref Pervasives.stdout +let glob_file = ref stdout let open_glob_file f = - glob_file := Pervasives.open_out f + glob_file := open_out f let close_glob_file () = - Pervasives.close_out !glob_file + close_out !glob_file type glob_output_t = | NoGlob @@ -37,7 +37,7 @@ let dump_to_dotglob () = glob_output := MultFiles let dump_into_file f = if String.equal f "stdout" then - (glob_output := StdOut; glob_file := Pervasives.stdout) + (glob_output := StdOut; glob_file := stdout) else (glob_output := File f; open_glob_file f) @@ -45,7 +45,7 @@ let feedback_glob () = glob_output := Feedback let dump_string s = if dump () && !glob_output != Feedback then - Pervasives.output_string !glob_file s + output_string !glob_file s let start_dump_glob ~vfile ~vofile = match !glob_output with diff --git a/interp/notation.ml b/interp/notation.ml index d58125e29b..ec3fad7f7d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -57,7 +57,7 @@ let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLev module NotationOrd = struct type t = notation - let compare = Pervasives.compare + let compare = pervasives_compare end module NotationSet = Set.Make(NotationOrd) @@ -593,7 +593,7 @@ let rec rawnum_compare s s' = try for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; for i = d to l-1 do - let c = Pervasives.compare s.[i] s'.[i-d] in + let c = pervasives_compare s.[i] s'.[i-d] in if c != 0 then raise (Comp c) done; 0 @@ -1242,7 +1242,7 @@ type entry_coercion = notation list module EntryCoercionOrd = struct type t = notation_entry * notation_entry - let compare = Pervasives.compare + let compare = pervasives_compare end module EntryCoercionMap = Map.Make(EntryCoercionOrd) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index a6b5fc9a41..1a5455cf3a 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -145,7 +145,7 @@ let dummy_symb = SymbValue (dummy_value ()) let eq_symbol sy1 sy2 = match sy1, sy2 with - | SymbValue v1, SymbValue v2 -> Pervasives.(=) v1 v2 (** FIXME: how is this even valid? *) + | SymbValue v1, SymbValue v2 -> (=) v1 v2 (** FIXME: how is this even valid? *) | SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2 | SymbName n1, SymbName n2 -> Name.equal n1 n2 | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2 diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 3e1ba9107c..b9735d0579 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -25,20 +25,13 @@ let _ = in Printexc.register_printer pr -let make_anomaly ?label pp = - Anomaly (label, pp) - let anomaly ?loc ?label pp = Loc.raise ?loc (Anomaly (label, pp)) exception UserError of string option * Pp.t (* User errors *) -let todo s = prerr_string ("TODO: "^s^"\n") - let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) -let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) - exception Timeout (** Only anomalies should reach the bottom of the handler stack. @@ -123,17 +116,17 @@ let print_gen ~anomaly (e, info) = print_gen ~anomaly ~extra_msg !handle_stack (e,info) (** The standard exception printer *) -let print ?info e = - let info = Option.default Exninfo.(info e) info in +let iprint (e, info) = print_gen ~anomaly:true (e,info) ++ print_backtrace info -let iprint (e, info) = print ~info e +let print e = + iprint (e, Exninfo.info e) (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) -let print_no_report e = print_gen ~anomaly:false (e, Exninfo.info e) let iprint_no_report (e, info) = print_gen ~anomaly:false (e,info) ++ print_backtrace info +let print_no_report e = iprint_no_report (e, Exninfo.info e) (** Predefined handlers **) diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 100dcd0b22..02eaf6bd0b 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -21,9 +21,6 @@ val push : exn -> Exninfo.iexn [Anomaly] is used for system errors and [UserError] for the user's ones. *) -val make_anomaly : ?label:string -> Pp.t -> exn -(** Create an anomaly. *) - val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a (** Raise an anomaly, with an optional location and an optional label identifying the anomaly. *) @@ -41,14 +38,6 @@ val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a (** Main error raising primitive. [user_err ?loc ?hdr pp] signals an error [pp] with optional header and location [hdr] [loc] *) -val invalid_arg : ?loc:Loc.t -> string -> 'a - -(** [todo] is for running of an incomplete code its implementation is - "do nothing" (or print a message), but this function should not be - used in a released code *) - -val todo : string -> unit - exception Timeout (** [register_handler h] registers [h] as a handler. @@ -72,7 +61,7 @@ exception Unhandled val register_handler : (exn -> Pp.t) -> unit (** The standard exception printer *) -val print : ?info:Exninfo.info -> exn -> Pp.t +val print : exn -> Pp.t val iprint : Exninfo.iexn -> Pp.t (** Same as [print], except that the "Please report" part of an anomaly diff --git a/lib/future.ml b/lib/future.ml index f6e9cee140..01fb7d0297 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -68,7 +68,7 @@ and 'a computation = 'a comput ref let unnamed = "unnamed" let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = - ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x))) + ref (Ongoing (name, CEphemeron.create (uuid, f, ref x))) let get x = match !x with | Finished v -> unnamed, UUID.invalid, id, ref (Val v) @@ -197,9 +197,9 @@ let pp_with ft pp = | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms - | Ppcmd_tag(tag, s) -> pp_open_tag ft tag; + | Ppcmd_tag(tag, s) -> pp_open_tag ft tag [@warning "-3"]; pp_cmd s; - pp_close_tag ft () + pp_close_tag ft () [@warning "-3"] in try pp_cmd pp with reraise -> diff --git a/lib/util.ml b/lib/util.ml index bac06b5701..61678f7669 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -8,6 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +type 'a pervasives_ref = 'a ref +let pervasives_ref = ref +let pervasives_compare = compare +let (!) = (!) +let (+) = (+) +let (-) = (-) + (* Mapping under pairs *) let on_fst f (a,b) = (f a,b) diff --git a/lib/util.mli b/lib/util.mli index 8ccb4b3f08..b6347126e0 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -8,6 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +type 'a pervasives_ref = 'a ref +val pervasives_ref : 'a -> 'a ref +val pervasives_compare : 'a -> 'a -> int +val (!) : 'a ref -> 'a +val (+) : int -> int -> int +val (-) : int -> int -> int + (** This module contains numerous utility functions on strings, lists, arrays, etc. *) diff --git a/library/summary.ml b/library/summary.ml index b3ec4c2db2..d3ae42694a 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -153,7 +153,7 @@ let (!) r = CEphemeron.get (fst !r) let ref ?(freeze=fun x -> x) ~name init = - let r = Pervasives.ref (CEphemeron.create init, name) in + let r = pervasives_ref (CEphemeron.create init, name) in declare_summary name { freeze_function = (fun ~marshallable -> freeze !r); unfreeze_function = ((:=) r); diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9abf212443..109125702c 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -125,7 +125,7 @@ module KOrd = struct type t = kind * string let compare (k1, s1) (k2, s2) = - let c = Pervasives.compare k1 k2 (* OK *) in + let c = pervasives_compare k1 k2 (* OK *) in if c = 0 then String.compare s1 s2 else c end diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f4edbda04a..cab82f7067 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1413,7 +1413,6 @@ let com_terminate let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(IsProof Lemma) () in let lemma = Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) - ~sign:(Environ.named_context_val env) ~info ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in @@ -1451,7 +1450,7 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t) Array.of_list (List.map mkVar x))))); observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x)]) g;; -let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type = +let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type = let open CVars in let opacity = match terminate_ref with @@ -1461,7 +1460,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~sign evd + let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false evd (EConstr.of_constr equation_lemma_type) in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (start_equation f_ref terminate_ref @@ -1553,9 +1552,8 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type (* message "start second proof"; *) let stop = (* XXX: What is the correct way to get sign at hook time *) - let sign = Environ.named_context_val Global.(env ()) in try - com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); + com_eqn uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); false with e when CErrors.noncritical e -> begin diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 243e0e945c..9d46bbc74e 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -376,7 +376,7 @@ let get_local_profiling_results () = List.hd Local.(!stack) own. *) module DData = struct type t = Feedback.doc_id * Stateid.t - let compare x y = Pervasives.compare x y + let compare x y = compare x y end module SM = Map.Make(DData) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 9e735e0680..539536911c 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -156,7 +156,7 @@ let rec prompt level = begin let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> - if Pervasives.(!batch) then return (DebugOn (level+1)) else + if Util.(!batch) then return (DebugOn (level+1)) else let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 2e32b00c25..24039c93c6 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -93,7 +93,7 @@ let dev_form n_spec p = let rec fixpoint f x = let y' = f x in - if Pervasives.(=) y' x then y' + if (=) y' x then y' else fixpoint f y' let rec_simpl_cone n_spec e = diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f0435126aa..5cc2c2e061 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1585,7 +1585,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) = let hyps_idx = prover.hyps prf in let hyps = selecti hyps_idx old_cl in - is_sublist Pervasives.(=) hyps new_cl in + is_sublist (=) hyps new_cl in @@ -1953,7 +1953,7 @@ open Persistent_cache module Cache = PHashtable(struct type t = (provername * micromega_polys) - let equal = Pervasives.(=) + let equal = (=) let hash = Hashtbl.hash end) diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index d8f71cda0c..cf5f60fb55 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -136,7 +136,7 @@ let pure_sos l = I should nonetheless be able to try something - over Z > is equivalent to -1 >= *) try let l = List.combine l (CList.interval 0 (List.length l -1)) in - let (lt,i) = try (List.find (fun (x,_) -> Pervasives.(=) (snd x) Mc.Strict) l) + let (lt,i) = try (List.find (fun (x,_) -> (=) (snd x) Mc.Strict) l) with Not_found -> List.hd l in let plt = poly_neg (poly_of_term (expr_to_term (fst lt))) in let (n,polys) = sumofsquares plt in (* n * (ci * pi^2) *) diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 34fb32c270..943bcb384b 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -15,7 +15,7 @@ open Vect let debug = false -let compare_float (p : float) q = Pervasives.compare p q +let compare_float (p : float) q = pervasives_compare p q (** Implementation of intervals *) open Itv @@ -587,7 +587,7 @@ struct let optimise vect l = (* We add a dummy (fresh) variable for vector *) let fresh = - List.fold_left (fun fr c -> Pervasives.max fr (Vect.fresh c.coeffs)) 0 l in + List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in let cstr = { coeffs = Vect.set fresh (Int (-1)) vect ; op = Eq ; diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 97cf23ac1f..537b6175b4 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -21,7 +21,7 @@ module Int = struct type t = int - let compare : int -> int -> int = Pervasives.compare + let compare : int -> int -> int = compare let equal : int -> int -> bool = (=) end @@ -354,7 +354,7 @@ struct let from i = i let next i = i + 1 - let max : int -> int -> int = Pervasives.max + let max : int -> int -> int = max let pp o i = output_string o (string_of_int i) let compare : int -> int -> int = Int.compare let to_int x = x diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index f909b4ecda..1a31a36732 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -278,7 +278,7 @@ and op = |Eq | Ge | Gt exception Strict -let is_strict c = Pervasives.(=) c.op Gt +let is_strict c = (=) c.op Gt let eval_op = function | Eq -> (=/) @@ -422,7 +422,7 @@ module LinPoly = struct let min_list (l:int list) = match l with | [] -> None - | e::l -> Some (List.fold_left Pervasives.min e l) + | e::l -> Some (List.fold_left min e l) let search_linear p l = min_list (search_all_linear p l) @@ -656,9 +656,9 @@ module ProofFormat = struct let rec compare p1 p2 = match p1, p2 with | Annot(s1,p1) , Annot(s2,p2) -> if s1 = s2 then compare p1 p2 - else Pervasives.compare s1 s2 - | Hyp i , Hyp j -> Pervasives.compare i j - | Def i , Def j -> Pervasives.compare i j + else Util.pervasives_compare s1 s2 + | Hyp i , Hyp j -> Util.pervasives_compare i j + | Def i , Def j -> Util.pervasives_compare i j | Cst n , Cst m -> Num.compare_num n m | Zero , Zero -> 0 | Square v1 , Square v2 -> Vect.compare v1 v2 @@ -667,7 +667,7 @@ module ProofFormat = struct | MulPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2) | AddPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2) | CutPrf p , CutPrf p' -> compare p p' - | _ , _ -> Pervasives.compare (id_of_constr p1) (id_of_constr p2) + | _ , _ -> Util.pervasives_compare (id_of_constr p1) (id_of_constr p2) end @@ -785,7 +785,7 @@ module ProofFormat = struct let rec xid_of_hyp i l' = match l' with | [] -> failwith (Printf.sprintf "id_of_hyp %i %s" hyp (string_of_int_list l)) - | hyp'::l' -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l' in + | hyp'::l' -> if (=) hyp hyp' then i else xid_of_hyp (i+1) l' in xid_of_hyp 0 l end @@ -873,7 +873,7 @@ module ProofFormat = struct let (p,o) = eval_prf_rule (fun i -> IMap.find i env) prf in if is_unsat (p,o) then true else - if Pervasives.(=) rst Done + if (=) rst Done then begin Printf.fprintf stdout "Last inference %a %s\n" LinPoly.pp p (string_of_op o); diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index 15fb55c007..4c95e6da75 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -587,7 +587,7 @@ let cut env rmin sol vm (rst:Restricted.t) tbl (x,v) = Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x; Printf.printf " %a\n" WithProof.output (v,prf); end; - if Pervasives.(=) (snd v) Eq + if (=) (snd v) Eq then (* Unsat *) Some (x,(v,prf)) else let vl = (Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol)) in @@ -651,7 +651,7 @@ let integer_solver lp = match find_cut (!nb mod 2) env cr (*x*) sol vm rst tbl with | None -> None | Some(cr,((v,op),cut)) -> - if Pervasives.(=) op Eq + if (=) op Eq then (* This is a contradiction *) Some(Step(vr,CutPrf cut, Done)) else diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index e3a9f6f60f..58d5d7ecf1 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -13,7 +13,7 @@ open Num (* Comparisons that are reflexive on NaN and also short-circuiting. *) (* ------------------------------------------------------------------------- *) -let cmp = Pervasives.compare (** FIXME *) +let cmp = compare (** FIXME *) let (=?) = fun x y -> cmp x y = 0;; let (<?) = fun x y -> cmp x y < 0;; @@ -491,21 +491,21 @@ let temp_path = Filename.get_temp_dir_name ();; (* ------------------------------------------------------------------------- *) let strings_of_file filename = - let fd = try Pervasives.open_in filename + let fd = try open_in filename with Sys_error _ -> failwith("strings_of_file: can't open "^filename) in let rec suck_lines acc = - try let l = Pervasives.input_line fd in + try let l = input_line fd in suck_lines (l::acc) with End_of_file -> List.rev acc in let data = suck_lines [] in - (Pervasives.close_in fd; data);; + (close_in fd; data);; let string_of_file filename = String.concat "\n" (strings_of_file filename);; let file_of_string filename s = - let fd = Pervasives.open_out filename in + let fd = open_out filename in output_string fd s; close_out fd;; diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 4b2bc66eb7..a5f3b83c48 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -148,7 +148,7 @@ let rec add (ve1:t) (ve2:t) = match ve1 , ve2 with | [] , v | v , [] -> v | (v1,c1)::l1 , (v2,c2)::l2 -> - let cmp = Pervasives.compare v1 v2 in + let cmp = Util.pervasives_compare v1 v2 in if cmp == 0 then let s = add_num c1 c2 in if eq_num (Int 0) s @@ -163,7 +163,7 @@ let rec xmul_add (n1:num) (ve1:t) (n2:num) (ve2:t) = | [] , _ -> mul n2 ve2 | _ , [] -> mul n1 ve1 | (v1,c1)::l1 , (v2,c2)::l2 -> - let cmp = Pervasives.compare v1 v2 in + let cmp = Util.pervasives_compare v1 v2 in if cmp == 0 then let s = ( n1 */ c1) +/ (n2 */ c2) in if eq_num (Int 0) s diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 6aec83318c..776bd0a829 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -500,7 +500,7 @@ let context sigma operation path (t : constr) = | (p, Fix ((_,n as ln),(tys,lna,v))) -> let l = Array.length v in let v' = Array.copy v in - v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) + v'.(n)<- loop (Util.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) | ((P_TYPE :: p), Prod (n,t,c)) -> (mkProd (n,loop i p t,c)) | ((P_TYPE :: p), Lambda (n,t,c)) -> @@ -684,7 +684,7 @@ let simpl_coeffs path_init path_k = | _ -> assert false) | _ -> assert false in - let n = Pervasives.(-) (List.length path_k) (List.length path_init) in + let n = Util.(-) (List.length path_k) (List.length path_init) in let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) in convert_concl ~check:false newc DEFAULTcast @@ -1000,7 +1000,7 @@ let shrink_pair p f1 f2 = | t1,t2 -> begin oprint t1; print_newline (); oprint t2; print_newline (); - flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1") + flush stdout; CErrors.user_err Pp.(str "shrink.1") end let reduce_factor p = function diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index cec87221f0..05c31062fc 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -242,7 +242,7 @@ let add_event, history, clear_history = (fun () -> !accu), (fun () -> accu := []) -let nf_linear = List.sort (fun x y -> Pervasives.(-) y.v x.v) +let nf_linear = List.sort (fun x y -> Util.(-) y.v x.v) let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 34f13b1096..f91b5e7aa2 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -26,7 +26,7 @@ module AdaptorDb = struct module AdaptorKind = struct type t = kind - let compare = Pervasives.compare + let compare = pervasives_compare end module AdaptorMap = Map.Make(AdaptorKind) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index afb546b2d2..496a02f07d 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -58,7 +58,7 @@ let cl_typ_ord t1 t2 = match t1, t2 with | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2 | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2 | CL_IND i1, CL_IND i2 -> ind_ord i1 i2 - | _ -> Pervasives.compare t1 t2 (** OK *) + | _ -> pervasives_compare t1 t2 (** OK *) module ClTyp = struct type t = cl_typ diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9b1acddef1..64fddd04a3 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -114,7 +114,7 @@ let print_impargs_by_name max = function let print_one_impargs_list l = let imps = List.filter is_status_implicit l in let maximps = List.filter Impargs.maximal_insertion_of imps in - let nonmaximps = List.subtract Pervasives.(=) imps maximps in (* FIXME *) + let nonmaximps = List.subtract (=) imps maximps in (* FIXME *) print_impargs_by_name false nonmaximps @ print_impargs_by_name true maximps diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index a476381b17..70819e9550 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -29,7 +29,7 @@ type term_label = let compare_term_label t1 t2 = match t1, t2 with | GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2 -| _ -> Pervasives.compare t1 t2 (** OK *) +| _ -> pervasives_compare t1 t2 (** OK *) type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 303ddacb67..849ea7e83f 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -257,7 +257,7 @@ let clenv_of_prods poly nprods (c, clenv) gl = let sigma = Tacmach.New.project gl in let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in let diff = nb_prod sigma ty - nprods in - if Pervasives.(>=) diff 0 then + if (>=) diff 0 then (* Was Some clenv... *) Some (Some diff, mk_clenv_from_n gl (Some diff) (c,ty)) diff --git a/tactics/redops.ml b/tactics/redops.ml index e0473cbefd..86ed8f8899 100644 --- a/tactics/redops.ml +++ b/tactics/redops.ml @@ -10,7 +10,7 @@ open Genredexpr -let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *) +let union_consts l1 l2 = Util.List.union (=) l1 l2 (* FIXME *) let make_red_flag l = let rec add_flag red = function diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 7a07e815ce..6f81be475b 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -297,7 +297,7 @@ module DAG = DAG(struct type t = string let compare = compare end) (** TODO: we should share this code with Coqdep_common *) module VData = struct type t = string list option * string list - let compare = Pervasives.compare + let compare = Util.pervasives_compare end module VCache = Set.Make(VData) diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index d98242ef17..8beb314046 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -357,7 +357,7 @@ let canonize f = module VData = struct type t = string list option * string list - let compare = Pervasives.compare + let compare = compare end module VCache = Set.Make(VData) diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 1c22efa513..3442ebb731 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -396,7 +396,7 @@ let copy src dst = try let cout = open_out dst in try - while true do Pervasives.output_char cout (input_char cin) done + while true do output_char cout (input_char cin) done with End_of_file -> close_out cout; close_in cin diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 9b7da862a8..02f0290802 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -13,9 +13,9 @@ open Index (*s Low level output *) -let output_char c = Pervasives.output_char !out_channel c +let output_char c = output_char !out_channel c -let output_string s = Pervasives.output_string !out_channel s +let output_string s = output_string !out_channel s let printf s = Printf.fprintf !out_channel s @@ -527,13 +527,13 @@ module Html = struct let header () = if !header_trailer then if !header_file_spec then - let cin = Pervasives.open_in !header_file in + let cin = open_in !header_file in try while true do - let s = Pervasives.input_line cin in + let s = input_line cin in printf "%s\n" s done - with End_of_file -> Pervasives.close_in cin + with End_of_file -> close_in cin else begin printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n"; @@ -548,13 +548,13 @@ module Html = struct let trailer () = if !header_trailer && !footer_file_spec then - let cin = Pervasives.open_in !footer_file in + let cin = open_in !footer_file in try while true do - let s = Pervasives.input_line cin in + let s = input_line cin in printf "%s\n" s done - with End_of_file -> Pervasives.close_in cin + with End_of_file -> close_in cin else begin if !index && (get_module false) <> "Index" then diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index bd19d30409..41a4e2a86a 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -35,7 +35,6 @@ rule mllib_list = parse { open Printf -open Unix (* Makefile's escaping rules are awful: $ is escaped by doubling and other special characters are escaped by backslash prefixing while @@ -99,6 +98,7 @@ let file_name s = function type dir = string option let add_directory add_file phys_dir = + let open Unix in Array.iter (fun f -> (* we avoid all files starting by '.' *) if f.[0] <> '.' then @@ -152,7 +152,7 @@ let add_caml_known phys_dir f = | _ -> () let add_caml_dir phys_dir = - handle_unix_error (add_directory add_caml_known) phys_dir + Unix.handle_unix_error (add_directory add_caml_known) phys_dir let traite_fichier_modules md ext = try @@ -192,7 +192,7 @@ let mllib_dependencies () = efullname efullname; printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - flush Pervasives.stdout) + flush stdout) (List.rev !mllibAccu) let mlpack_dependencies () = @@ -209,7 +209,7 @@ let mlpack_dependencies () = efullname efullname; printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - flush Pervasives.stdout) + flush stdout) (List.rev !mlpackAccu) let rec parse = function diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index f6211102e6..e49b1c0c07 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -315,8 +315,8 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in (* Flush in a compatible order with 8.5 *) (* This mimics the semantics of the old Pp.flush_all *) let loop_flush_all () = - Pervasives.flush stderr; - Pervasives.flush stdout; + flush stderr; + flush stdout; Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index c7b8b13282..0c45ff11d7 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -53,7 +53,7 @@ type program_info = ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool - ; prg_sign : named_context_val } + } (* Saving an obligation *) diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 7433888cec..a8dd5040cb 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -48,7 +48,7 @@ type program_info = ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool - ; prg_sign : Environ.named_context_val } + } val declare_obligation : program_info diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 3402e05af8..00316bfadf 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -218,9 +218,11 @@ let initialize_named_context_for_proof () = (* Starting a goal *) let start_lemma ~name ~poly ?(udecl=UState.default_univ_decl) - ?(sign=initialize_named_context_for_proof()) ?(info=Info.make ()) sigma c = + (* We remove the bodies of variables in the named context marked + "opaque", this is a hack tho, see #10446 *) + let sign = initialize_named_context_for_proof () in let goals = [ Global.env_of_context sign , c ] in let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in { proof ; info } diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 17003bed7b..fbf91b3ad4 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -80,7 +80,6 @@ val start_lemma : name:Id.t -> poly:bool -> ?udecl:UState.universe_decl - -> ?sign:Environ.named_context_val -> ?info:Info.t -> Evd.evar_map -> EConstr.types @@ -122,11 +121,6 @@ val start_lemma_com -> Vernacexpr.proof_expr list -> t -(* Prepare global named context for proof session: remove proofs of - opaque section definitions and remove vm-compiled code *) - -val initialize_named_context_for_proof : unit -> Environ.named_context_val - (** {4 Saving proofs} *) val save_lemma_admitted : lemma:t -> unit diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 90892feb13..e754ead5dd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -519,7 +519,7 @@ let read_recursive_format sl fmt = let sl = skip_var_in_recursive_format fmt in try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in let rec get_tail = function - | (loc,a) :: sepfmt, (_,b) :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *) + | (loc,a) :: sepfmt, (_,b) :: fmt when (=) a b -> get_tail (sepfmt, fmt) (* FIXME *) | [], tail -> skip_var_in_recursive_format tail | (loc,_) :: _, ([] | (_,UnpTerminal _) :: _)-> error_not_same ?loc () | _, (loc,_)::_ -> error_not_same ?loc () in @@ -953,7 +953,7 @@ let join_auxiliary_recursive_types recvars etyps = | None, None -> typs | Some _, None -> typs | None, Some ytyp -> (x,ytyp)::typs - | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *) + | Some xtyp, Some ytyp when (=) xtyp ytyp -> typs (* FIXME *) | Some xtyp, Some ytyp -> user_err (strbrk "In " ++ Id.print x ++ str " .. " ++ Id.print y ++ diff --git a/vernac/obligations.ml b/vernac/obligations.ml index eb1e3b74b4..37fe0df0ee 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -298,7 +298,7 @@ let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) -let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind +let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind notations obls impls ~scope ~poly ~kind reduce = let obls', b = match b with @@ -335,7 +335,7 @@ let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind ; prg_reduce = reduce ; prg_hook = hook ; prg_opaque = opaque - ; prg_sign = sign } + } let map_cardinal m = let i = ref 0 in @@ -495,7 +495,7 @@ let rec solve_obligation prg num tac = let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in let poly = prg.prg_poly in - let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in + let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in let lemma = fst @@ Lemmas.by !default_tactic lemma in let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in lemma @@ -634,9 +634,8 @@ let show_term n = let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = - let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print name ++ str " has type-checked" in - let prg = init_prog_info sign ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in + let prg = init_prog_info ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); @@ -654,11 +653,10 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = - let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> - let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind) + let prg = init_prog_info ~opaque n univdecl (Some b) t ctx deps (Some fixkind) notations obls imps ~poly ~scope ~kind reduce ?hook in progmap_add n (CEphemeron.create prg)) l; let _defined = diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 78112d9dc4..e676fe94db 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -371,7 +371,7 @@ open Pputils | (c,(idl,t))::l -> match factorize l with | (xl,((c', t') as r))::l' - when (c : bool) == c' && Pervasives.(=) t t' -> + when (c : bool) == c' && (=) t t' -> (* FIXME: we need equality on constr_expr *) (idl@xl,r)::l' | l' -> (idl,(c,t))::l' diff --git a/vernac/search.ml b/vernac/search.ml index 101a578587..964d01260b 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -148,7 +148,7 @@ module ConstrPriority = struct -(3*(num_symbols t) + size t) let compare (_,_,_,p1) (_,_,_,p2) = - Pervasives.compare p1 p2 + pervasives_compare p1 p2 end module PriorityQueue = Heap.Functional(ConstrPriority) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 7644f4c5b6..046defc26b 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -329,8 +329,8 @@ let init_terminal_output ~color = Format.pp_set_print_tags !std_ft true; Format.pp_set_print_tags !err_ft true end; - Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft); - Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft) + Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft) [@warning "-3"]; + Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft) [@warning "-3"] (* Rules for emacs: - Debug/info: emacs_quote_info |