diff options
92 files changed, 1247 insertions, 841 deletions
diff --git a/.travis.yml b/.travis.yml index 481a635581..1699568ca0 100644 --- a/.travis.yml +++ b/.travis.yml @@ -190,7 +190,7 @@ matrix: # Ocaml warnings with two compilers - env: - MAIN_TARGET="coqocaml" - - EXTRA_CONF="-byte-only -coqide byte -warn-error" + - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - EXTRA_OPAM="hevea ${LABLGTK}" # dummy target - BUILD_TARGET="clean" @@ -209,7 +209,7 @@ matrix: - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-byte-only -coqide byte -warn-error" + - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - EXTRA_OPAM="num hevea ${LABLGTK_BE}" # dummy target - BUILD_TARGET="clean" @@ -239,7 +239,7 @@ matrix: - CAMLP5_VER=".6.17" - NATIVE_COMP="no" - COQ_DEST="-prefix ${PWD}/_install" - - EXTRA_CONF="-coqide opt -warn-error" + - EXTRA_CONF="-coqide opt -warn-error yes" - EXTRA_OPAM="${LABLGTK}" before_install: - brew update @@ -63,6 +63,7 @@ Focusing - Focusing bracket `{` now supports single-numbered goal selector, e.g. `2: {` will focus on the second sub-goal. As usual, unfocus with `}` once the sub-goal is fully solved. + The `Focus` and `Unfocus` commands are now deprecated. Vernacular Commands @@ -73,6 +74,7 @@ Vernacular Commands was removed. Use Local as a prefix instead. - For the Extraction Language command, "OCaml" is spelled correctly. The older "Ocaml" is still accepted, but deprecated. +- Using “Require” inside a section is deprecated. Universes @@ -86,6 +88,15 @@ Universes more information. - Fix #5726: Notations that start with `Type` now support universe instances with `@{u}`. +- `with Definition` now understands universe declarations + (like `@{u| Set < u}`). + +Tools + +- Coq can now be run with the option -mangle-names to change the auto-generated + name scheme. This is intended to function as a linter for developments that + want to be robust to changes in auto-generated names. This feature is experimental, + and may change or dissapear without warning. Checker @@ -110,6 +121,8 @@ Standard Library Coq.Numbers.DecimalString providing a type of decimal numbers, some facts about them, and conversions between decimal numbers and nat, positive, N, Z, and string. +- Added [Coq.Strings.String.concat] to concatenate a list of strings + inserting a separator between each item - Some deprecated aliases are now emitting warnings when used. @@ -268,6 +281,7 @@ Standard Library lemmas such as INR_IZR_INZ should be used instead. - Real constants are now represented using IZR rather than R0 and R1; this might cause rewriting rules to fail to apply to constants. +- Added new notation {x & P} for sigT (without a type for x) Plugins diff --git a/Makefile.doc b/Makefile.doc index 894ef9a99a..9fd93651d1 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -387,10 +387,10 @@ install-doc-index-urls: OCAMLDOCDIR=dev/ocamldoc -DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ - ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ - ./parsing/*.mli ./proofs/*.mli \ - ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli) +DOCMLLIBS= $(CORECMA:.cma=_MLLIB_DEPENDENCIES) $(PLUGINSCMO:.cmo=_MLPACK_DEPENDENCIES) +DOCMLS=$(foreach lib,$(DOCMLLIBS),$(addsuffix .ml, $($(lib)))) + +DOCMLIS=$(wildcard $(addsuffix /*.mli, $(SRCDIRS))) # Defining options to generate dependencies graphs DOT=dot @@ -434,7 +434,12 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) - $(OCAMLDOC_MLLIBD) ml-doc: - $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) + $(SHOW)'OCAMLDOC -html' + $(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) \ + $(DOCMLS) -d $(OCAMLDOCDIR)/html/implementation -colorize-code \ + -t "Coq mls documentation" \ + -css-style ../style.css parsing/parsing.dot : | parsing/parsing.mllib.d $(OCAMLDOC_MLLIBD) diff --git a/appveyor.yml b/appveyor.yml index 64c1bedb54..44a93d15d4 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -10,12 +10,12 @@ image: environment: CYGMIRROR: http://ftp.inf.tu-dresden.de/software/windows/cygwin32 matrix: - - USEOPAM: true - ARCH: 64 - USEOPAM: false ARCH: 32 - USEOPAM: false ARCH: 64 + - USEOPAM: true + ARCH: 64 build_script: - cmd: 'call %APPVEYOR_BUILD_FOLDER%\dev\ci\appveyor.bat' diff --git a/checker/univ.mli b/checker/univ.mli index 3876e7bbc9..935f0a2b8d 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -84,7 +84,7 @@ val check_eq : universe check_function val initial_universes : universes (** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) + @raise AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared diff --git a/clib/option.ml b/clib/option.ml index c2e2e70970..21913e8f7a 100644 --- a/clib/option.ml +++ b/clib/option.ml @@ -44,7 +44,7 @@ let hash f = function exception IsNone (** [get x] returns [y] where [x] is [Some y]. - @raise [IsNone] if [x] equals [None]. *) + @raise IsNone if [x] equals [None]. *) let get = function | Some y -> y | _ -> raise IsNone diff --git a/configure.ml b/configure.ml index 69db9407ab..1eae3bd931 100644 --- a/configure.ml +++ b/configure.ml @@ -22,8 +22,10 @@ let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr"; let verbose = ref false (* for debugging this script *) (** * Utility functions *) - -let die msg = eprintf "%s\nConfiguration script failed!\n" msg; exit 1 +let cfprintf oc = kfprintf (fun oc -> fprintf oc "\n%!") oc +let cprintf s = cfprintf stdout s +let ceprintf s = cfprintf stderr s +let die msg = ceprintf "%s\nConfiguration script failed!" msg; exit 1 let s2i = int_of_string let i2s = string_of_int @@ -107,7 +109,7 @@ let run ?(fatal=true) ?(err=StdErr) prog args = let cmd = String.concat " " (prog::args) in let exn = match e with Failure s -> s | _ -> Printexc.to_string e in let msg = sprintf "Error while running '%s' (%s)" cmd exn in - if fatal then die msg else (printf "W: %s\n" msg; "", []) + if fatal then die msg else (cprintf "W: %s" msg; "", []) let tryrun prog args = run ~fatal:false ~err:DevNull prog args @@ -203,7 +205,7 @@ let win_aware_quote_executable str = sprintf "%S" str else let _ = if contains_suspicious_characters str then - printf "*Warning* The string %S contains suspicious characters; ocamlfind might fail\n" str in + cprintf "*Warning* The string %S contains suspicious characters; ocamlfind might fail" str in Str.global_replace (Str.regexp "\\\\") "/" str (** * Date *) @@ -235,6 +237,101 @@ let _ = if not (dir_exists "bin") then Unix.mkdir "bin" 0o755 type ide = Opt | Byte | No +type preferences = { + prefix : string option; + local : bool; + vmbyteflags : string option; + custom : bool option; + bindir : string option; + libdir : string option; + configdir : string option; + datadir : string option; + mandir : string option; + docdir : string option; + emacslib : string option; + coqdocdir : string option; + ocamlfindcmd : string option; + lablgtkdir : string option; + camlp5dir : string option; + arch : string option; + natdynlink : bool; + coqide : ide option; + macintegration : bool; + browser : string option; + withdoc : bool; + byteonly : bool; + flambda_flags : string list; + debug : bool; + profile : bool; + bin_annot : bool; + annot : bool; + bytecodecompiler : bool; + nativecompiler : bool; + coqwebsite : string; + force_caml_version : bool; + force_findlib_version : bool; + warn_error : bool; +} + +module Profiles = struct + +let default = { + prefix = None; + local = false; + vmbyteflags = None; + custom = None; + bindir = None; + libdir = None; + configdir = None; + datadir = None; + mandir = None; + docdir = None; + emacslib = None; + coqdocdir = None; + ocamlfindcmd = None; + lablgtkdir = None; + camlp5dir = None; + arch = None; + natdynlink = true; + coqide = None; + macintegration = true; + browser = None; + withdoc = false; + byteonly = false; + flambda_flags = []; + debug = true; + profile = false; + bin_annot = false; + annot = false; + bytecodecompiler = true; + nativecompiler = not (os_type_win32 || os_type_cygwin); + coqwebsite = "http://coq.inria.fr/"; + force_caml_version = false; + force_findlib_version = false; + warn_error = false; +} + +let devel state = { state with + local = true; + bin_annot = true; + annot = true; + warn_error = true; +} +let devel_doc = "-local -annot -bin-annot -warn-error yes" + +let get = function + | "devel" -> devel + | s -> raise (Arg.Bad ("profile name expected instead of "^s)) + +let doc = + "<profile> Sets a bunch of flags. Supported profiles: + devel = " ^ devel_doc + +end + +let prefs = ref Profiles.default + + let get_bool = function | "true" | "yes" | "y" | "all" -> true | "false" | "no" | "n" -> false @@ -246,123 +343,99 @@ let get_ide = function | "no" -> No | s -> raise (Arg.Bad ("(opt|byte|no) argument expected instead of "^s)) -let arg_bool r = Arg.String (fun s -> r := get_bool s) - -let arg_string_option r = Arg.String (fun s -> r := Some s) - -module Prefs = struct - let prefix = ref (None : string option) - let local = ref false - let vmbyteflags = ref (None : string option) - let custom = ref (None : bool option) - let bindir = ref (None : string option) - let libdir = ref (None : string option) - let configdir = ref (None : string option) - let datadir = ref (None : string option) - let mandir = ref (None : string option) - let docdir = ref (None : string option) - let emacslib = ref (None : string option) - let coqdocdir = ref (None : string option) - let ocamlfindcmd = ref (None : string option) - let lablgtkdir = ref (None : string option) - let camlp5dir = ref (None : string option) - let arch = ref (None : string option) - let natdynlink = ref true - let coqide = ref (None : ide option) - let macintegration = ref true - let browser = ref (None : string option) - let withdoc = ref false - let byteonly = ref false - let flambda_flags = ref [] - let debug = ref true - let profile = ref false - let bin_annot = ref false - let annot = ref false - let bytecodecompiler = ref true - let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) - let coqwebsite = ref "http://coq.inria.fr/" - let force_caml_version = ref false - let force_findlib_version = ref false - let warn_error = ref false -end +let arg_bool f = Arg.String (fun s -> prefs := f !prefs (get_bool s)) + +let arg_string f = Arg.String (fun s -> prefs := f !prefs s) +let arg_string_option f = Arg.String (fun s -> prefs := f !prefs (Some s)) +let arg_string_list c f = Arg.String (fun s -> prefs := f !prefs (string_split c s)) + +let arg_set f = Arg.Unit (fun () -> prefs := f !prefs true) +let arg_clear f = Arg.Unit (fun () -> prefs := f !prefs false) + +let arg_set_option f = Arg.Unit (fun () -> prefs := f !prefs (Some true)) +let arg_clear_option f = Arg.Unit (fun () -> prefs := f !prefs (Some false)) + +let arg_ide f = Arg.String (fun s -> prefs := f !prefs (Some (get_ide s))) + +let arg_profile = Arg.String (fun s -> prefs := Profiles.get s !prefs) (* TODO : earlier any option -foo was also available as --foo *) let args_options = Arg.align [ - "-prefix", arg_string_option Prefs.prefix, + "-prefix", arg_string_option (fun p prefix -> { p with prefix }), "<dir> Set installation directory to <dir>"; - "-local", Arg.Set Prefs.local, + "-local", arg_set (fun p local -> { p with local }), " Set installation directory to the current source tree"; - "-vmbyteflags", arg_string_option Prefs.vmbyteflags, + "-vmbyteflags", arg_string_option (fun p vmbyteflags -> { p with vmbyteflags }), "<flags> Comma-separated link flags for the VM of coqtop.byte"; - "-custom", Arg.Unit (fun () -> Prefs.custom := Some true), + "-custom", arg_set_option (fun p custom -> { p with custom }), " Build bytecode executables with -custom (not recommended)"; - "-no-custom", Arg.Unit (fun () -> Prefs.custom := Some false), + "-no-custom", arg_clear_option (fun p custom -> { p with custom }), " Do not build with -custom on Windows and MacOS"; - "-bindir", arg_string_option Prefs.bindir, + "-bindir", arg_string_option (fun p bindir -> { p with bindir }), "<dir> Where to install bin files"; - "-libdir", arg_string_option Prefs.libdir, + "-libdir", arg_string_option (fun p libdir -> { p with libdir }), "<dir> Where to install lib files"; - "-configdir", arg_string_option Prefs.configdir, + "-configdir", arg_string_option (fun p configdir -> { p with configdir }), "<dir> Where to install config files"; - "-datadir", arg_string_option Prefs.datadir, + "-datadir", arg_string_option (fun p datadir -> { p with datadir }), "<dir> Where to install data files"; - "-mandir", arg_string_option Prefs.mandir, + "-mandir", arg_string_option (fun p mandir -> { p with mandir }), "<dir> Where to install man files"; - "-docdir", arg_string_option Prefs.docdir, + "-docdir", arg_string_option (fun p docdir -> { p with docdir }), "<dir> Where to install doc files"; - "-emacslib", arg_string_option Prefs.emacslib, + "-emacslib", arg_string_option (fun p emacslib -> { p with emacslib }), "<dir> Where to install emacs files"; - "-coqdocdir", arg_string_option Prefs.coqdocdir, + "-coqdocdir", arg_string_option (fun p coqdocdir -> { p with coqdocdir }), "<dir> Where to install Coqdoc style files"; - "-ocamlfind", arg_string_option Prefs.ocamlfindcmd, + "-ocamlfind", arg_string_option (fun p ocamlfindcmd -> { p with ocamlfindcmd }), "<dir> Specifies the ocamlfind command to use"; - "-lablgtkdir", arg_string_option Prefs.lablgtkdir, + "-lablgtkdir", arg_string_option (fun p lablgtkdir -> { p with lablgtkdir }), "<dir> Specifies the path to the Lablgtk library"; - "-camlp5dir", - Arg.String (fun s -> Prefs.camlp5dir:=Some s), + "-camlp5dir", arg_string_option (fun p camlp5dir -> { p with camlp5dir }), "<dir> Specifies where is the Camlp5 library and tells to use it"; - "-flambda-opts", - Arg.String (fun s -> Prefs.flambda_flags := string_split ' ' s), + "-flambda-opts", arg_string_list ' ' (fun p flambda_flags -> { p with flambda_flags }), "<flags> Specifies additional flags to be passed to the flambda optimizing compiler"; - "-arch", arg_string_option Prefs.arch, + "-arch", arg_string_option (fun p arch -> { p with arch }), "<arch> Specifies the architecture"; - "-natdynlink", arg_bool Prefs.natdynlink, + "-natdynlink", arg_bool (fun p natdynlink -> { p with natdynlink }), "(yes|no) Use dynamic loading of native code or not"; - "-coqide", Arg.String (fun s -> Prefs.coqide := Some (get_ide s)), + "-coqide", arg_ide (fun p coqide -> { p with coqide }), "(opt|byte|no) Specifies whether or not to compile CoqIDE"; - "-nomacintegration", Arg.Clear Prefs.macintegration, + "-nomacintegration", arg_clear (fun p macintegration -> { p with macintegration }), " Do not try to build CoqIDE MacOS integration"; - "-browser", arg_string_option Prefs.browser, + "-browser", arg_string_option (fun p browser -> { p with browser }), "<command> Use <command> to open URL %s"; - "-with-doc", arg_bool Prefs.withdoc, + "-with-doc", arg_bool (fun p withdoc -> { p with withdoc }), "(yes|no) Compile the documentation or not"; - "-byte-only", Arg.Set Prefs.byteonly, + "-byte-only", arg_set (fun p byteonly -> { p with byteonly }), " Compiles only bytecode version of Coq"; - "-nodebug", Arg.Clear Prefs.debug, + "-nodebug", arg_clear (fun p debug -> { p with debug }), " Do not add debugging information in the Coq executables"; - "-profile", Arg.Set Prefs.profile, + "-profiling", arg_set (fun p profile -> { p with profile }), " Add profiling information in the Coq executables"; - "-annotate", Arg.Unit (fun () -> printf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead.\n"), + "-annotate", Arg.Unit (fun () -> cprintf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead."), " Deprecated. Please use -annot or -bin-annot instead"; - "-annot", Arg.Set Prefs.annot, + "-annot", arg_set (fun p annot -> { p with annot }), " Dumps ml text annotation files while compiling Coq (e.g. for Tuareg)"; - "-bin-annot", Arg.Set Prefs.bin_annot, + "-bin-annot", arg_set (fun p bin_annot -> { p with bin_annot }), " Dumps ml binary annotation files while compiling Coq (e.g. for Merlin)"; - "-bytecode-compiler", arg_bool Prefs.bytecodecompiler, + "-bytecode-compiler", arg_bool (fun p bytecodecompiler -> { p with bytecodecompiler }), "(yes|no) Enable Coq's bytecode reduction machine (VM)"; - "-native-compiler", arg_bool Prefs.nativecompiler, + "-native-compiler", arg_bool (fun p nativecompiler -> { p with nativecompiler }), "(yes|no) Compilation to native code for conversion and normalization"; - "-coqwebsite", Arg.Set_string Prefs.coqwebsite, + "-coqwebsite", arg_string (fun p coqwebsite -> { p with coqwebsite }), " URL of the coq website"; - "-force-caml-version", Arg.Set Prefs.force_caml_version, + "-force-caml-version", arg_set (fun p force_caml_version -> { p with force_caml_version }), " Force OCaml version"; - "-force-findlib-version", Arg.Set Prefs.force_findlib_version, + "-force-findlib-version", arg_set (fun p force_findlib_version -> { p with force_findlib_version }), " Force findlib version"; - "-warn-error", Arg.Set Prefs.warn_error, - " Make OCaml warnings into errors"; + "-warn-error", arg_bool (fun p warn_error -> { p with warn_error }), + "(yes|no) Make OCaml warnings into errors (default no)"; "-camldir", Arg.String (fun _ -> ()), "<dir> Specifies path to 'ocaml' for running configure script"; + "-profile", arg_profile, + Profiles.doc ] let parse_args () = @@ -370,7 +443,7 @@ let parse_args () = args_options (fun s -> raise (Arg.Bad ("Unknown option: "^s))) "Available options for configure are:"; - if !Prefs.local && !Prefs.prefix <> None then + if !prefs.local && !prefs.prefix <> None then die "Options -prefix and -local are incompatible." let _ = parse_args () @@ -391,10 +464,10 @@ let reset_caml_lex c o = c.lex <- o let reset_caml_top c o = c.top <- o let reset_caml_find c o = c.find <- o -let coq_debug_flag = if !Prefs.debug then "-g" else "" -let coq_profile_flag = if !Prefs.profile then "-p" else "" -let coq_annot_flag = if !Prefs.annot then "-annot" else "" -let coq_bin_annot_flag = if !Prefs.bin_annot then "-bin-annot" else "" +let coq_debug_flag = if !prefs.debug then "-g" else "" +let coq_profile_flag = if !prefs.profile then "-p" else "" +let coq_annot_flag = if !prefs.annot then "-annot" else "" +let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else "" (* This variable can be overriden only for debug purposes, use with care. *) @@ -412,8 +485,8 @@ let arch_progs = ("/usr/ucb/arch", []) ] let query_arch () = - printf "I can not automatically find the name of your architecture.\n"; - printf "Give me a name, please [win32 for Win95, Win98 or WinNT]: %!"; + cprintf "I can not automatically find the name of your architecture."; + cprintf "Give me a name, please [win32 for Win95, Win98 or WinNT]: %!"; read_line () let rec try_archs = function @@ -423,7 +496,7 @@ let rec try_archs = function | _ :: rest -> try_archs rest | [] -> query_arch () -let arch = match !Prefs.arch with +let arch = match !prefs.arch with | Some a -> a | None -> let arch,_ = tryrun "uname" ["-s"] in @@ -455,7 +528,7 @@ let vcs = let _ = let f = ".git/hooks/pre-commit" in if vcs = "git" && dir_exists ".git/hooks" && not (Sys.file_exists f) then begin - printf "Creating pre-commit hook in %s\n" f; + cprintf "Creating pre-commit hook in %s" f; let o = open_out f in let pr s = fprintf o s in pr "#!/bin/sh\n"; @@ -470,7 +543,7 @@ let _ = (** * Browser command *) let browser = - match !Prefs.browser with + match !prefs.browser with | Some b -> b | None when arch_is_win32 -> "start %s" | None when arch = "Darwin" -> "open %s" @@ -479,7 +552,7 @@ let browser = (** * OCaml programs *) let camlbin, caml_version, camllib, findlib_version = - let () = match !Prefs.ocamlfindcmd with + let () = match !prefs.ocamlfindcmd with | Some cmd -> reset_caml_find camlexec cmd | None -> try reset_caml_find camlexec (which camlexec.find) @@ -521,11 +594,11 @@ let caml_version_nums = let check_caml_version () = if caml_version_nums >= [4;2;1] then - printf "You have OCaml %s. Good!\n" caml_version + cprintf "You have OCaml %s. Good!" caml_version else - let () = printf "Your version of OCaml is %s.\n" caml_version in - if !Prefs.force_caml_version then - printf "*Warning* Your version of OCaml is outdated.\n" + let () = cprintf "Your version of OCaml is %s." caml_version in + if !prefs.force_caml_version then + cprintf "*Warning* Your version of OCaml is outdated." else die "You need OCaml 4.02.1 or later." @@ -543,11 +616,11 @@ let findlib_version_nums = let check_findlib_version () = if findlib_version_nums >= [1;4;1] then - printf "You have OCamlfind %s. Good!\n" findlib_version + cprintf "You have OCamlfind %s. Good!" findlib_version else - let () = printf "Your version of OCamlfind is %s.\n" findlib_version in - if !Prefs.force_findlib_version then - printf "*Warning* Your version of OCamlfind is outdated.\n" + let () = cprintf "Your version of OCamlfind is %s." findlib_version in + if !prefs.force_findlib_version then + cprintf "*Warning* Your version of OCamlfind is outdated." else die "You need OCamlfind 1.4.1 or later." @@ -571,7 +644,7 @@ let camltag = match caml_version_list with *) let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50" let coq_warn_error = - if !Prefs.warn_error + if !prefs.warn_error then "-warn-error +a" ^ (if caml_version_nums > [4;2;3] then "-56" @@ -611,7 +684,7 @@ let which_camlp5 base = (* TODO: camlp5dir should rather be the *binary* location, just as camldir *) (* TODO: remove the late attempts at finding gramlib.cma *) -let check_camlp5 testcma = match !Prefs.camlp5dir with +let check_camlp5 testcma = match !prefs.camlp5dir with | Some dir -> if Sys.file_exists (dir/testcma) then let camlp5o = @@ -636,7 +709,7 @@ let check_camlp5_version camlp5o = let version = List.nth (string_split ' ' version_line) 2 in match numeric_prefix_list version with | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) -> - printf "You have Camlp5 %s. Good!\n" version; version + cprintf "You have Camlp5 %s. Good!" version; version | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" let config_camlp5 () = @@ -659,22 +732,22 @@ let camlp5libdir = shorten_camllib fullcamlp5libdir (** * Native compiler *) let msg_byteonly () = - printf "Only the bytecode version of Coq will be available.\n" + cprintf "Only the bytecode version of Coq will be available." let msg_no_ocamlopt () = - printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly () + cprintf "Cannot find the OCaml native-code compiler."; msg_byteonly () let msg_no_camlp5_cmxa () = - printf "Cannot find the native-code library of camlp5.\n"; msg_byteonly () + cprintf "Cannot find the native-code library of camlp5."; msg_byteonly () let msg_no_dynlink_cmxa () = - printf "Cannot find native-code dynlink library.\n"; msg_byteonly (); - printf "For building a native-code Coq, you may try to first\n"; - printf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)\n"; - printf "and then run ./configure -natdynlink no\n" + cprintf "Cannot find native-code dynlink library."; msg_byteonly (); + cprintf "For building a native-code Coq, you may try to first"; + cprintf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)"; + cprintf "and then run ./configure -natdynlink no" let check_native () = - let () = if !Prefs.byteonly then raise Not_found in + let () = if !prefs.byteonly then raise Not_found in let version, _ = tryrun camlexec.find ["opt";"-version"] in if version = "" then let () = msg_no_ocamlopt () in raise Not_found else if not (Sys.file_exists (fullcamlp5libdir/camlp5mod^".cmxa")) @@ -684,16 +757,16 @@ let check_native () = else let () = if version <> caml_version then - printf - "Warning: Native and bytecode compilers do not have the same version!\n" - in printf "You have native-code compilation. Good!\n" + cprintf + "Warning: Native and bytecode compilers do not have the same version!" + in cprintf "You have native-code compilation. Good!" let best_compiler = try check_native (); "opt" with Not_found -> "byte" (** * Native dynlink *) -let hasnatdynlink = !Prefs.natdynlink && best_compiler = "opt" +let hasnatdynlink = !prefs.natdynlink && best_compiler = "opt" let natdynlinkflag = if hasnatdynlink then "true" else "false" @@ -723,7 +796,7 @@ let check_for_numlib () = match numlib with | "" -> die "Num library not installed, required for OCaml 4.06 or later" - | _ -> printf "You have the Num library installed. Good!\n" + | _ -> cprintf "You have the Num library installed. Good!" let numlib = check_for_numlib () @@ -740,7 +813,7 @@ let get_source = function (** Is some location a suitable LablGtk2 installation ? *) let check_lablgtkdir ?(fatal=false) src dir = - let yell msg = if fatal then die msg else (printf "%s\n" msg; false) in + let yell msg = if fatal then die msg else (cprintf "%s" msg; false) in let msg = get_source src in if not (dir_exists dir) then yell (sprintf "No such directory '%s' (%s)." dir msg) @@ -753,7 +826,7 @@ let check_lablgtkdir ?(fatal=false) src dir = (** Detect and/or verify the Lablgtk2 location *) let get_lablgtkdir () = - match !Prefs.lablgtkdir with + match !prefs.lablgtkdir with | Some dir -> let msg = Manual in if check_lablgtkdir ~fatal:true msg dir then dir, msg @@ -776,7 +849,7 @@ let get_lablgtkdir () = let check_lablgtk_version src dir = match src with | Manual | Stdlib -> - printf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.\n"; + cprintf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3."; (true, "an unknown version") | OCamlFind -> let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in @@ -787,7 +860,7 @@ let check_lablgtk_version src dir = match src with else if vi < [2; 18; 3] then begin (* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *) - printf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable.\n" v; + cprintf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable." v; (true, "an unknown version") end else @@ -800,11 +873,11 @@ exception Ide of ide (** If the user asks an impossible coqide, we abort the configuration *) -let set_ide ide msg = match ide, !Prefs.coqide with +let set_ide ide msg = match ide, !prefs.coqide with | No, Some (Byte|Opt) | Byte, Some Opt -> die (msg^":\n=> cannot build requested CoqIde") | _ -> - printf "%s:\n=> %s CoqIde will be built.\n" msg (pr_ide ide); + cprintf "%s:\n=> %s CoqIde will be built." msg (pr_ide ide); raise (Ide ide) let lablgtkdir = ref "" @@ -813,7 +886,7 @@ let lablgtkdir = ref "" This function also sets the lablgtkdir reference in case of success. *) let check_coqide () = - if !Prefs.coqide = Some No then set_ide No "CoqIde manually disabled"; + if !prefs.coqide = Some No then set_ide No "CoqIde manually disabled"; let dir, via = get_lablgtkdir () in if dir = "" then set_ide No "LablGtk2 not found"; let (ok, version) = check_lablgtk_version via dir in @@ -821,7 +894,7 @@ let check_coqide () = if not ok then set_ide No (found^", but too old (required >= 2.18.3, found " ^ version ^ ")"); (* We're now sure to produce at least one kind of coqide *) lablgtkdir := shorten_camllib dir; - if !Prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested"); + if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested"); if best_compiler<>"opt" then set_ide Byte (found^", but no native compiler"); if not (Sys.file_exists (dir/"gtkThread.cmx")) then set_ide Byte (found^", but no native LablGtk2"); @@ -844,7 +917,7 @@ let idearchdef = ref "X11" let coqide_flags () = if !lablgtkdir <> "" then lablgtkincludes := sprintf "-I %S" !lablgtkdir; match coqide, arch with - | "opt", "Darwin" when !Prefs.macintegration -> + | "opt", "Darwin" when !prefs.macintegration -> let osxdir,_ = tryrun camlexec.find ["query";"lablgtkosx"] in if osxdir <> "" then begin lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir; @@ -870,7 +943,7 @@ let strip = if arch = "Darwin" then if hasnatdynlink then "true" else "strip" else - if !Prefs.profile || !Prefs.debug then "true" else begin + if !prefs.profile || !prefs.debug then "true" else begin let _, all = run camlexec.find ["ocamlc";"-config"] in let strip = String.concat "" (List.map (fun l -> match string_split ' ' l with @@ -886,11 +959,11 @@ let strip = let check_doc () = let err s = - printf "%s was not found; documentation will not be available\n" s; + ceprintf "%s was not found; documentation will not be available" s; raise Not_found in try - if not !Prefs.withdoc then raise Not_found; + if not !prefs.withdoc then raise Not_found; if not (program_in_path "latex") then err "latex"; if not (program_in_path "hevea") then err "hevea"; if not (program_in_path "hacha") then err "hacha"; @@ -908,28 +981,28 @@ let coqtop = Sys.getcwd () let unix = os_type_cygwin || not arch_is_win32 -(** Variable name, description, ref in Prefs, default dir, prefix-relative *) +(** Variable name, description, ref in prefs, default dir, prefix-relative *) type path_style = | Absolute of string (* Should start with a "/" *) | Relative of string (* Should not start with a "/" *) let install = [ - "BINDIR", "the Coq binaries", Prefs.bindir, + "BINDIR", "the Coq binaries", !prefs.bindir, Relative "bin", Relative "bin", Relative "bin"; - "COQLIBINSTALL", "the Coq library", Prefs.libdir, + "COQLIBINSTALL", "the Coq library", !prefs.libdir, Relative "lib", Relative "lib/coq", Relative ""; - "CONFIGDIR", "the Coqide configuration files", Prefs.configdir, + "CONFIGDIR", "the Coqide configuration files", !prefs.configdir, Relative "config", Absolute "/etc/xdg/coq", Relative "ide"; - "DATADIR", "the Coqide data files", Prefs.datadir, + "DATADIR", "the Coqide data files", !prefs.datadir, Relative "share", Relative "share/coq", Relative "ide"; - "MANDIR", "the Coq man pages", Prefs.mandir, + "MANDIR", "the Coq man pages", !prefs.mandir, Relative "man", Relative "share/man", Relative "man"; - "DOCDIR", "the Coq documentation", Prefs.docdir, + "DOCDIR", "the Coq documentation", !prefs.docdir, Relative "doc", Relative "share/doc/coq", Relative "doc"; - "EMACSLIB", "the Coq Emacs mode", Prefs.emacslib, + "EMACSLIB", "the Coq Emacs mode", !prefs.emacslib, Relative "emacs", Relative "share/emacs/site-lisp", Relative "tools"; - "COQDOCDIR", "the Coqdoc LaTeX files", Prefs.coqdocdir, + "COQDOCDIR", "the Coqdoc LaTeX files", !prefs.coqdocdir, Relative "latex", Relative "share/texmf/tex/latex/misc", Relative "tools/coqdoc"; ] @@ -959,8 +1032,8 @@ let find_suffix prefix path = match prefix with let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout) = let dir,suffix = - if !Prefs.local then (use_suffix coqtop locallayout,locallayout) - else match !uservalue, !Prefs.prefix with + if !prefs.local then (use_suffix coqtop locallayout,locallayout) + else match uservalue, !prefs.prefix with | Some d, p -> d,find_suffix p d | _, Some p -> let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in @@ -992,7 +1065,7 @@ let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s let custom_os = arch_is_win32 || arch = "Darwin" -let use_custom = match !Prefs.custom with +let use_custom = match !prefs.custom with | Some b -> b | None -> custom_os @@ -1002,10 +1075,10 @@ let build_loadpath = ref "# you might want to set CAML_LD_LIBRARY_PATH by hand!" let config_runtime () = - match !Prefs.vmbyteflags with + match !prefs.vmbyteflags with | Some flags -> string_split ',' flags | _ when use_custom -> [custom_flag] - | _ when !Prefs.local -> + | _ when !prefs.local -> ["-dllib";"-lcoqrun";"-dllpath";coqtop/"kernel/byterun"] | _ -> let ld="CAML_LD_LIBRARY_PATH" in @@ -1029,7 +1102,7 @@ let print_summary () = pr " OCaml version : %s\n" caml_version; pr " OCaml binaries in : %s\n" (esc camlbin); pr " OCaml library in : %s\n" (esc camllib); - pr " OCaml flambda flags : %s\n" (String.concat " " !Prefs.flambda_flags); + pr " OCaml flambda flags : %s\n" (String.concat " " !prefs.flambda_flags); pr " Camlp5 version : %s\n" camlp5_version; pr " Camlp5 binaries in : %s\n" (esc camlp5bindir); pr " Camlp5 library in : %s\n" (esc camlp5libdir); @@ -1043,10 +1116,10 @@ let print_summary () = pr " Documentation : %s\n" (if withdoc then "All" else "None"); pr " Web browser : %s\n" browser; - pr " Coq web site : %s\n" !Prefs.coqwebsite; - pr " Bytecode VM enabled : %B\n" !Prefs.bytecodecompiler; - pr " Native Compiler enabled : %B\n\n" !Prefs.nativecompiler; - if !Prefs.local then + pr " Coq web site : %s\n" !prefs.coqwebsite; + pr " Bytecode VM enabled : %B\n" !prefs.bytecodecompiler; + pr " Native Compiler enabled : %B\n\n" !prefs.nativecompiler; + if !prefs.local then pr " Local build, no installation...\n" else (pr " Paths for true installation:\n"; @@ -1095,7 +1168,7 @@ let write_configml f = pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n"; pr "(* Exact command that generated this file: *)\n"; pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv)); - pr_b "local" !Prefs.local; + pr_b "local" !prefs.local; pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n"; pr_s "coqlib" coqlib; pr_s "configdir" configdir; @@ -1130,17 +1203,17 @@ let write_configml f = pr "let gtk_platform = `%s\n" !idearchdef; pr_b "has_natdynlink" hasnatdynlink; pr_s "natdynlinkflag" natdynlinkflag; - pr_l "flambda_flags" !Prefs.flambda_flags; + pr_l "flambda_flags" !prefs.flambda_flags; pr_i "vo_magic_number" vo_magic; pr_i "state_magic_number" state_magic; pr_s "browser" browser; - pr_s "wwwcoq" !Prefs.coqwebsite; - pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/"); - pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); - pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); + pr_s "wwwcoq" !prefs.coqwebsite; + pr_s "wwwbugtracker" (!prefs.coqwebsite ^ "bugs/"); + pr_s "wwwrefman" (!prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); + pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); - pr_b "bytecode_compiler" !Prefs.bytecodecompiler; - pr_b "native_compiler" !Prefs.nativecompiler; + pr_b "bytecode_compiler" !prefs.bytecodecompiler; + pr_b "native_compiler" !prefs.nativecompiler; let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; @@ -1197,7 +1270,7 @@ let write_makefile f = pr "#Variable used to detect whether ./configure has run successfully.\n"; pr "COQ_CONFIGURED=yes\n\n"; pr "# Local use (no installation)\n"; - pr "LOCAL=%B\n\n" !Prefs.local; + pr "LOCAL=%B\n\n" !prefs.local; pr "# Bytecode link flags : should we use -custom or not ?\n"; pr "CUSTOM=%s\n" custom_flag; pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags); @@ -1226,7 +1299,7 @@ let write_makefile f = pr "# User compilation flag\n"; pr "USERFLAGS=\n\n"; (* XXX make this configurable *) - pr "FLAMBDA_FLAGS=%s\n" (String.concat " " !Prefs.flambda_flags); + pr "FLAMBDA_FLAGS=%s\n" (String.concat " " !prefs.flambda_flags); pr "# Flags for GCC\n"; pr "CFLAGS=%s\n\n" cflags; pr "# Compilation debug flags\n"; @@ -1271,7 +1344,7 @@ let write_makefile f = pr "# Option to control compilation and installation of the documentation\n"; pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no"); pr "# Option to produce precompiled files for native_compute\n"; - pr "NATIVECOMPUTE=%s\n" (if !Prefs.nativecompiler then "-native-compiler" else ""); + pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else ""); close_out o; Unix.chmod f 0o444 diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 665d541761..ccf22cc866 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -78,6 +78,9 @@ SET GTK_FROM_SOURCES=N REM see -threads in ReadMe.txt SET MAKE_THREADS=8 +REM see -addon in ReadMe.txt +SET "COQ_ADDONS= " + REM ========== PARSE COMMAND LINE PARAMETERS ========== SHIFT @@ -233,6 +236,14 @@ IF "%~0" == "-threads" ( GOTO Parse ) +IF "%~0" == "-addon" ( + SET "COQ_ADDONS=%COQ_ADDONS% %~1" + SHIFT + SHIFT + GOTO Parse +) + + IF NOT "%~0" == "" ( ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW ECHO !!! Illegal parameter %~0 @@ -426,6 +437,7 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -coqver ^<Coq version to install^> ECHO -gtksrc ^<Y or N^> build GTK ^(90 min^) or use cygwin version ECHO -threads ^<1..N^> Number of make threads + ECHO -addon ^<name^> Enable building selected addon (can be repeated) ECHO( ECHO See ReadMe.txt for a detailed description of all parameters ECHO( @@ -447,6 +459,7 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -coqver = %COQ_VERSION% ECHO -gtksrc = %GTK_FROM_SOURCES% ECHO -threads = %MAKE_THREADS% + ECHO -addon = %COQ_ADDONS% GOTO :EOF :CheckYN diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index 7e80e33c6d..93851aeb8d 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -61,6 +61,7 @@ The Script MakeCoq_MinGW does: - either installs MinGW GTK via Cygwin or compiles it fom sources - download, compile and install OCaml, CamlP5, Menhir, lablgtk - download, compile and install Coq +- download, compile and install selected addons - create a Windows installer (NSIS based) The parameters are described below. Mostly paths and the HTTP proxy need to be @@ -335,6 +336,10 @@ Possible values: 1..N. Should not be more than 1.5x the number of cores. Should not be more than available RAM/2GB (e.g. 4 for 8GB) +===== -addon ===== + +Enable build and installation of selected Coq package (can be repeated for +selecting more packages) ==================== TODO ==================== diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d8cde39f82..bea30b1a72 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -223,6 +223,12 @@ function get_expand_source_tar { cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" $TARBALLS else wget $1/$2.$3 + if file -i $2.$3 | grep text/html; then + echo Download failed: $1/$2.$3 + echo The file wget downloaded is an html file: + cat $2.$3 + exit 1 + fi if [ ! "$2.$3" == "$name.$3" ] ; then mv $2.$3 $name.$3 fi @@ -1280,7 +1286,8 @@ function make_coq_installer { # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build: # ocaml: ocaml + menhir + camlp5 + findlib - # ocal_coq: as above + coq + # ocaml_coq: as above + coq + # ocaml_coq_addons: as above + lib/user-contrib/* # Create coq file list as ocaml_coq / ocaml diff_files coq ocaml_coq ocaml @@ -1294,11 +1301,17 @@ function make_coq_installer { # Coq objects objects required for plugin development = coq objects except those for pre installed plugins diff_files coq_plugindev coq_objects coq_objects_plugins + # Addons (TODO: including objects that could go to the plugindev thing, but + # then one would have to make that package depend on this one, so not + # implemented yet) + diff_files coq_addons ocaml_coq_addons ocaml_coq + # Coq files, except objects needed only for plugin development diff_files coq_base coq coq_plugindev # Convert section files to NSIS format files_to_nsis coq_base + files_to_nsis coq_addons files_to_nsis coq_plugindev files_to_nsis ocaml @@ -1314,12 +1327,30 @@ function make_coq_installer { cp ../patches/ReplaceInFile.nsh dev/nsis VERSION=`grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r'` cd dev/nsis - logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico coq_new.nsi + logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi build_post fi } +###################### ADDONS ##################### + +function make_addon_bignums { + if build_prep https://github.com/coq/bignums/archive/ master zip 1 bignums-8.8.0; then + # To make command lines shorter :-( + echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local + logn make make all + logn make-install make install + build_post + fi +} + +function make_addons { + for addon in $COQ_ADDONS; do + make_addon_$addon + done +} + ###################### TOP LEVEL BUILD ##################### make_sed @@ -1337,6 +1368,10 @@ fi list_files ocaml_coq +make_addons + +list_files ocaml_coq_addons + if [ "$MAKEINSTALLER" == "Y" ] ; then make_coq_installer fi diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi index 2c2f0fa47c..55fba6d5ab 100644 --- a/dev/build/windows/patches_coq/coq_new.nsi +++ b/dev/build/windows/patches_coq/coq_new.nsi @@ -9,6 +9,7 @@ ; ARCH The target architecture, either x86_64 or i686 ; COQ_SRC_PATH path of Coq installation in Windows or MinGW format (either \\ or /, but with drive letter) ; COQ_ICON path of Coq icon file in Windows or MinGW format +; COQ_ADDONS list of addons that are shipped ; Enable compression after debugging. ; SetCompress off @@ -69,7 +70,8 @@ Var INSTDIR_DBS ; INSTDIR with \\ instead of \ ;Description LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE." - LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development." + LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}" + ;LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development." LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq." LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user." LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users." @@ -150,6 +152,11 @@ SectionEnd ;OCAML !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS" ;OCAML SectionEnd +Section "Coq packages" Sec2 + SetOutPath "$INSTDIR\" + !include "..\..\..\filelists\coq_addons.nsh" +SectionEnd + Section "Coq files for plugin developers" Sec3 SetOutPath "$INSTDIR\" !include "..\..\..\filelists\coq_plugindev.nsh" @@ -176,7 +183,7 @@ SectionEnd !insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1) - ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2) + !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2) !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5) diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index dec6f0d182..85a71baf7f 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -23,6 +23,7 @@ if %USEOPAM% == false ( call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^ -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ + -addon=bignums -make=N ^ -setup %CYGROOT%\%SETUP% || GOTO ErrorExit copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit 7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 0003a2c217..c48c2d5d16 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -41,15 +41,15 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -local + ./configure -profile devel make clean make -j4 coqide printers -The "-annotate" option is essential when one wants to use Merlin. +The "-profile devel" enables all options recommended for developers (like +warnings, support for Merlin, etc). Moreover Coq is configured so that +it can be run without installing it (i.e. from the current directory). -The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install - -Then check if +Once the compilation is over check if - bin/coqtop - bin/coqide behave as expected. diff --git a/dev/header.c b/dev/header.c new file mode 100644 index 0000000000..663c43b3d6 --- /dev/null +++ b/dev/header.c @@ -0,0 +1,9 @@ +/************************************************************************/ +/* * The Coq Proof Assistant / The Coq Development Team */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* <O___,, * (see CREDITS file for the list of authors) */ +/* \VV/ **************************************************************/ +/* // * This file is distributed under the terms of the */ +/* * GNU Lesser General Public License Version 2.1 */ +/* * (see LICENSE file for the text of the license) */ +/************************************************************************/ diff --git a/dev/header b/dev/header.ml index 7c3ee60040..7c3ee60040 100644 --- a/dev/header +++ b/dev/header.ml diff --git a/dev/header.py b/dev/header.py new file mode 100644 index 0000000000..f81c8aa6a2 --- /dev/null +++ b/dev/header.py @@ -0,0 +1,9 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## diff --git a/doc/LICENSE b/doc/LICENSE index ada22e6690..0aa0d629e8 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -25,16 +25,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA distributed under the terms of the Lesser General Public License version 2.1 or later. -The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo -Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All -documents (the LaTeX source and the PostScript, PDF and html outputs) -are copyright (c) INRIA 2004-2006. The material connected to the FAQ -(Coq for the Clueless) may be distributed only subject to the terms -and conditions set forth in the Open Publication License, v1.0 or -later (the latest version is presently available at -http://www.opencontent.org/openpub/). Options A and B are *not* -elected. - The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre Castéran and Eduardo Gimenez. All related documents (the LaTeX and BibTeX sources and the PostScript, PDF and html outputs) are copyright diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 04a8a25c12..5b73ac00a6 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -241,6 +241,20 @@ The following command-line options are recognized by the commands {\tt Collapse the universe hierarchy of {\Coq}. Warning: this makes the logic inconsistent. +\item[{\tt -mangle-names} {\em ident}]\ % + + Experimental: Do not depend on this option. + + Replace Coq's auto-generated name scheme with names of the form + {\tt ident0}, {\tt ident1}, \ldots etc. + The command {\tt Set Mangle Names}\optindex{Mangle Names} turns + the behavior on in a document, and {\tt Set Mangle Names Prefix "ident"} + \optindex{Mangle Names Prefix} changes the used prefix. + + This feature is intended to be used as a linter for developments that want + to be robust to changes in the auto-generated name scheme. The options are + provided to facilitate tracking down problems. + \item[{\tt -compat} {\em version}]\ % Attempt to maintain some backward-compatibility with a previous version. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index c4c0435c5f..0a4d0ef9aa 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1156,16 +1156,6 @@ without having to cut manually the proof in smaller lemmas. It may be useful to generate lemmas minimal w.r.t. the assumptions they depend on. This can be obtained thanks to the option below. -\begin{quote} -\optindex{Shrink Abstract} -{\tt Set Shrink Abstract} -\end{quote} -\emph{Deprecated since 8.7} - -When set (default), all lemmas generated through \texttt{abstract {\tacexpr}} -and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the -variables that appear in the term constructed by \texttt{\tacexpr}. - \begin{Variants} \item \texttt{abstract {\tacexpr} using {\ident}}.\\ Give explicitly the name of the auxiliary lemma. diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 6b24fdde79..bd74a40d7c 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -298,15 +298,19 @@ subgoals which clutter your screen. \begin{Variant} \item {\tt Focus {\num}.}\\ This focuses the attention on the $\num^{th}$ subgoal to prove. - \end{Variant} +\emph{This command is deprecated since 8.8: prefer the use of bullets or + focusing brackets instead, including {\tt {\num}: \{}}. + \subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}} This command restores to focus the goal that were suspended by the last {\tt Focus} command. +\emph{This command is deprecated since 8.8.} + \subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}} -Succeeds in the proof is fully unfocused, fails is there are some +Succeeds in the proof if fully unfocused, fails if there are some goals out of focus. \subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket} diff --git a/engine/evd.mli b/engine/evd.mli index 7957eaa018..49c953f6d3 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -320,8 +320,8 @@ exception UniversesDiffer val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map (** Add the given universe unification constraints to the evar map. - @raises UniversesDiffer in case a first-order unification fails. - @raises UniverseInconsistency + @raise UniversesDiffer in case a first-order unification fails. + @raise UniverseInconsistency . *) (** {5 Extra data} diff --git a/engine/namegen.ml b/engine/namegen.ml index 33570ac73d..d66b77b573 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -192,9 +192,45 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = (**********************************************************************) (* Fresh names *) +(* Introduce a mode where auto-generated names are mangled + to test dependence of scripts on auto-generated names *) + +let mangle_names = ref false + +let _ = Goptions.( + declare_bool_option + { optdepr = false; + optname = "mangle auto-generated names"; + optkey = ["Mangle";"Names"]; + optread = (fun () -> !mangle_names); + optwrite = (:=) mangle_names; }) + +let mangle_names_prefix = ref (Id.of_string "_0") +let set_prefix x = mangle_names_prefix := forget_subscript x + +let set_mangle_names_mode x = begin + set_prefix x; + mangle_names := true + end + +let _ = Goptions.( + declare_string_option + { optdepr = false; + optname = "mangled names prefix"; + optkey = ["Mangle";"Names";"Prefix"]; + optread = (fun () -> Id.to_string !mangle_names_prefix); + optwrite = begin fun x -> + set_prefix + (try Id.of_string x + with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) + end }) + +let mangle_id id = if !mangle_names then !mangle_names_prefix else id + (* Looks for next "good" name by lifting subscript *) let next_ident_away_from id bad = + let id = mangle_id id in let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in name_rec id @@ -293,6 +329,7 @@ let next_global_ident_away id avoid = looks for same name with lower available subscript *) let next_ident_away id avoid = + let id = mangle_id id in if Id.Set.mem id avoid then next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid) else id @@ -423,23 +460,3 @@ let rename_bound_vars_as_displayed sigma avoid env c = | _ -> c in rename avoid env c - -(**********************************************************************) -(* "H"-based naming strategy introduced June 2014 for hypotheses in - Prop produced by case/elim/destruct/induction, in place of the - strategy that was using the first letter of the type, leading to - inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar - types *) - -let h_based_elimination_names = ref false - -let use_h_based_elimination_names () = !h_based_elimination_names - -open Goptions - -let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "use of \"H\"-based proposition names in elimination tactics"; - optkey = ["Standard";"Proposition";"Elimination";"Names"]; - optread = (fun () -> !h_based_elimination_names); - optwrite = (:=) h_based_elimination_names } diff --git a/engine/namegen.mli b/engine/namegen.mli index d266347060..1b70ef68dd 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -116,7 +116,6 @@ val compute_displayed_name_in_gen : (evar_map -> int -> 'a -> bool) -> evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t -(**********************************************************************) -(* Naming strategy for arguments in Prop when eliminating inductive types *) - -val use_h_based_elimination_names : unit -> bool +val set_mangle_names_mode : Id.t -> unit +(** Turn on mangled names mode and with the given prefix. + @raise UserError if the argument is invalid as an identifier. *) diff --git a/engine/proofview.ml b/engine/proofview.ml index 25c8e2d802..8a844bbf54 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -127,7 +127,7 @@ let focus_context (left,right) = (** This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns - [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the + [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the original list. The focused list has lenght [j-i-1] and contains the goals from number [i] to number [j] (both included) the first goal of the list being numbered [1]. [focus_sublist i j l] raises @@ -572,8 +572,8 @@ let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs (** [extend_to_list startxs rx endxs l] builds a list - [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises - [SizeMismatch] if [startxs@endxs] is already longer than [l]. *) + [startxs @ [rx,...,rx] @ endxs] of the same length as [l]. Raises + [SizeMismatch] if [startxs @ endxs] is already longer than [l]. *) let extend_to_list startxs rx endxs l = (* spiwack: I use [l] essentially as a natural number *) let rec duplicate acc = function diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 84162ca89b..918e12e5cb 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1077,7 +1077,7 @@ type 'a raw_cases_pattern_expr_r = | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname | RCPatCstr of Globnames.global_reference * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list - (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) + (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *) | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option | RCPatOr of 'a raw_cases_pattern_expr list and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t diff --git a/interp/modintern.ml b/interp/modintern.ml index 92264fb72b..8876855853 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -62,18 +62,19 @@ let lookup_module lqid = fst (lookup_module_or_modtype Module lqid) let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> WithMod (fqid,lookup_module qid), Univ.ContextSet.empty - | CWith_Definition ((_,fqid),c) -> - let sigma = Evd.from_env env in + | CWith_Definition ((_,fqid),udecl,c) -> + let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in let c, ectx = interp_constr env sigma c in - if Flags.is_universe_polymorphism () then - let ctx = UState.context ectx in - let inst, ctx = Univ.abstract_universes ctx in - let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in - let c = EConstr.to_constr sigma c in - WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty - else - let c = EConstr.to_constr sigma c in - WithDef (fqid,(c, None)), UState.context_set ectx + begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with + | Entries.Polymorphic_const_entry ctx -> + let inst, ctx = Univ.abstract_universes ctx in + let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in + let c = EConstr.to_constr sigma c in + WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty + | Entries.Monomorphic_const_entry ctx -> + let c = EConstr.to_constr sigma c in + WithDef (fqid,(c, None)), ctx + end let loc_of_module l = l.CAst.loc diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 474b80ec48..31f811bc8a 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -17,6 +17,11 @@ open Decl_kinds (** [constr_expr] is the abstract syntax tree produced by the parser *) +type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl + +type ident_decl = lident * universe_decl_expr option +type name_decl = lname * universe_decl_expr option + type notation = string type explicitation = @@ -51,7 +56,7 @@ type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list - (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) + (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) | CPatAtom of reference option | CPatOr of cases_pattern_expr list | CPatNotation of notation * cases_pattern_notation_substitution @@ -121,7 +126,7 @@ and recursion_order_expr = | CWfRec of constr_expr | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) -(** Anonymous defs allowed ?? *) +(* Anonymous defs allowed ?? *) and local_binder_expr = | CLocalAssum of lname list * binder_kind * constr_expr | CLocalDef of lname * constr_expr * constr_expr option @@ -139,7 +144,7 @@ type constr_pattern_expr = constr_expr type with_declaration_ast = | CWith_Module of Id.t list Loc.located * qualid Loc.located - | CWith_Definition of Id.t list Loc.located * constr_expr + | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr type module_ast_r = | CMident of qualid diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 7e9bc8caa9..0a6e5b3b31 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -160,11 +160,6 @@ type option_ref_value = (** Identifier and optional list of bound universes and constraints. *) -type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl - -type ident_decl = lident * universe_decl_expr option -type name_decl = lname * universe_decl_expr option - type sort_expr = Sorts.family type definition_expr = @@ -536,3 +531,14 @@ type vernac_when = | VtNow | VtLater type vernac_classification = vernac_type * vernac_when + + +(** Deprecated stuff *) +type universe_decl_expr = Constrexpr.universe_decl_expr +[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] + +type ident_decl = Constrexpr.ident_decl +[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] + +type name_decl = Constrexpr.name_decl +[@@ocaml.deprecated "alias of Constrexpr.name_decl"] diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c5a8c7b233..11faef02cb 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -798,7 +798,7 @@ let drop_parameters depth n argstk = s. @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 71453a04bd..b9c71d72af 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -216,7 +216,7 @@ val whd_stack : s. @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> diff --git a/kernel/environ.mli b/kernel/environ.mli index 51388b8f3b..4e6ac1e725 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -201,7 +201,7 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) (** Add universe constraints to the environment. - @raises UniverseInconsistency + @raise UniverseInconsistency . *) val add_constraints : Univ.Constraint.t -> env -> env diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 97745771e1..d4fba63fb3 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -43,7 +43,7 @@ val check_constraint : t -> univ_constraint -> bool val check_constraints : Constraint.t -> t -> bool (** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) + @raise AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared diff --git a/lib/lib.mllib b/lib/lib.mllib index b2260ba097..0891859423 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -15,7 +15,6 @@ CWarnings Rtree System Explore -RTree CProfile Future Spawn diff --git a/library/summary.ml b/library/summary.ml index 6ca8715559..7ef19fbfb4 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -89,6 +89,16 @@ let unfreeze_single name state = Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]); iraise e +let warn_summary_out_of_scope = + let name = "summary-out-of-scope" in + let category = "dev" in + let default = CWarnings.Disabled in + CWarnings.create ~name ~category ~default (fun name -> + Pp.str (Printf.sprintf + "A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s" + name) + ) + let unfreeze_summaries ?(partial=false) { summaries; ml_module } = (* The unfreezing of [ml_modules_summary] has to be anticipated since it * may modify the content of [summaries] by loading new ML modules *) @@ -101,7 +111,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } = try decl.unfreeze_function String.Map.(find name summaries) with Not_found -> if not partial then begin - Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name); + warn_summary_out_of_scope name; decl.init_function () end; in diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 430d18893a..e393c2bbfc 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -21,6 +21,24 @@ let thm_token = G_vernac.thm_token let hint = Gram.entry_create "hint" +let warn_deprecated_focus = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.strbrk + "The Focus command is deprecated; use bullets or focusing brackets instead" + ) + +let warn_deprecated_focus_n n = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.(str "The Focus command is deprecated;" ++ spc () + ++ str "use '" ++ int n ++ str ": {' instead") + ) + +let warn_deprecated_unfocus = + CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" + (fun () -> Pp.strbrk "The Unfocus command is deprecated") + (* Proof commands *) GEXTEND Gram GLOBAL: hint command; @@ -51,9 +69,15 @@ GEXTEND Gram | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n - | IDENT "Focus" -> VernacFocus None - | IDENT "Focus"; n = natural -> VernacFocus (Some n) - | IDENT "Unfocus" -> VernacUnfocus + | IDENT "Focus" -> + warn_deprecated_focus ~loc:!@loc (); + VernacFocus None + | IDENT "Focus"; n = natural -> + warn_deprecated_focus_n n ~loc:!@loc (); + VernacFocus (Some n) + | IDENT "Unfocus" -> + warn_deprecated_unfocus ~loc:!@loc (); + VernacUnfocus | IDENT "Unfocused" -> VernacUnfocused | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 595a60f335..feaef31619 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -12,10 +12,10 @@ open Pp open CErrors open Util open Names +open Vernacexpr open Constrexpr open Constrexpr_ops open Extend -open Vernacexpr open Decl_kinds open Declarations open Misctypes @@ -142,7 +142,7 @@ let name_of_ident_decl : ident_decl -> name_decl = (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition ident_decl; + record_field decl_notation rec_definition ident_decl univ_decl; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -557,8 +557,8 @@ GEXTEND Gram [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ] ; with_declaration: - [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr -> - CWith_Definition (fqid,c) + [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> + CWith_Definition (fqid,udecl,c) | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid -> CWith_Module (fqid,qid) ] ] diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9aae251f1a..258c4bb11c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -442,6 +442,7 @@ module Prim = let name = Gram.entry_create "Prim.name" let identref = Gram.entry_create "Prim.identref" + let univ_decl = Gram.entry_create "Prim.univ_decl" let ident_decl = Gram.entry_create "Prim.ident_decl" let pattern_ident = Gram.entry_create "pattern_ident" let pattern_identref = Gram.entry_create "pattern_identref" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8592968dc1..e66aa4ade8 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -198,6 +198,7 @@ module Prim : val ident : Id.t Gram.entry val name : lname Gram.entry val identref : lident Gram.entry + val univ_decl : universe_decl_expr Gram.entry val ident_decl : ident_decl Gram.entry val pattern_ident : Id.t Gram.entry val pattern_identref : lident Gram.entry diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index 264b48a082..c403f7c5a1 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -46,7 +46,7 @@ Extract Constant EqNat.eq_nat_decide => "Big.eq". Extract Constant Peano_dec.eq_nat_dec => "Big.eq". -Extract Constant Compare_dec.nat_compare => +Extract Constant Nat.compare => "Big.compare_case Eq Lt Gt". Extract Constant Compare_dec.leb => "Big.le". diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 35af714171..a2f809a0c1 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -59,7 +59,7 @@ Extract Inlined Constant EqNat.eq_nat_decide => "(=)". Extract Inlined Constant Peano_dec.eq_nat_dec => "(=)". -Extract Constant Compare_dec.nat_compare => +Extract Constant Nat.compare => "fun n m -> if n=m then Eq else if n<m then Lt else Gt". Extract Inlined Constant Compare_dec.leb => "(<=)". Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)". diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 543a37ff8d..f066ea462f 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -21,6 +21,7 @@ Require Import List. Require Import Bool. Require Import OrderedRing. Require Import Refl. +Require Coq.micromega.Tauto. Set Implicit Arguments. @@ -796,7 +797,7 @@ Definition xnormalise (t:Formula C) : list (NFormula) := | OpLe => (psub lhs rhs ,Strict) :: nil end. -Require Import Coq.micromega.Tauto. +Import Coq.micromega.Tauto. Definition cnf_normalise (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnormalise t). diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 85e2a5b235..c5a09d677e 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -30,6 +30,7 @@ Require Export Ncring_initial. Require Export Ncring_tac. Require Export Integral_domain. Require Import DiscrR. +Require Import ZArith. Declare ML Module "nsatz_plugin". @@ -56,9 +57,8 @@ simpl. simpl; cring. Qed. (* adpatation du code de Benjamin aux setoides *) -Require Import ZArith. -Require Export Ring_polynom. -Require Export InitialRing. +Export Ring_polynom. +Export InitialRing. Definition PolZ := Pol Z. Definition PEZ := PExpr Z. diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 0f5417e7db..ad3afafd85 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -7,15 +7,14 @@ *************************************************************************) open Names -open Constr let module_refl_name = "ReflOmegaCore" let module_refl_path = ["Coq"; "romega"; module_refl_name] type result = | Kvar of string - | Kapp of string * constr list - | Kimp of constr * constr + | Kapp of string * EConstr.t list + | Kimp of EConstr.t * EConstr.t | Kufo let meaningful_submodule = [ "Z"; "N"; "Pos" ] @@ -30,9 +29,10 @@ let string_of_global r = in prefix^(Names.Id.to_string (Nametab.basename_of_global r)) -let destructurate t = - let c, args = decompose_app t in - match Constr.kind c, args with +let destructurate sigma t = + let c, args = EConstr.decompose_app sigma t in + let open Constr in + match EConstr.kind sigma c, args with | Const (sp,_), args -> Kapp (string_of_global (Globnames.ConstRef sp), args) | Construct (csp,_) , args -> @@ -45,10 +45,11 @@ let destructurate t = exception DestConstApp -let dest_const_apply t = - let f,args = decompose_app t in +let dest_const_apply sigma t = + let open Constr in + let f,args = EConstr.decompose_app sigma t in let ref = - match Constr.kind f with + match EConstr.kind sigma f with | Const (sp,_) -> Globnames.ConstRef sp | Construct (csp,_) -> Globnames.ConstructRef csp | Ind (isp,_) -> Globnames.IndRef isp @@ -66,10 +67,22 @@ let coq_modules = let bin_module = [["Coq";"Numbers";"BinNums"]] let z_module = [["Coq";"ZArith";"BinInt"]] -let init_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x -let constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" coq_modules x -let z_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" z_module x -let bin_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" bin_module x +let init_constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x +let constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" coq_modules x +let z_constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" z_module x +let bin_constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" bin_module x (* Logic *) let coq_refl_equal = lazy(init_constant "eq_refl") @@ -130,62 +143,64 @@ let coq_O = lazy(init_constant "O") let rec mk_nat = function | 0 -> Lazy.force coq_O - | n -> mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) + | n -> EConstr.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) (* Lists *) -let mkListConst c = - let r = +let mkListConst c = + let r = Coqlib.coq_reference "" ["Init";"Datatypes"] c - in - let inst = - if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|] - else fun _ -> Univ.Instance.empty in - fun u -> mkConstructU (Globnames.destConstructRef r, inst u) + let inst = + if Global.is_polymorphic r then + fun u -> EConstr.EInstance.make (Univ.Instance.of_array [|u|]) + else + fun _ -> EConstr.EInstance.empty + in + fun u -> EConstr.mkConstructU (Globnames.destConstructRef r, inst u) -let coq_cons univ typ = mkApp (mkListConst "cons" univ, [|typ|]) -let coq_nil univ typ = mkApp (mkListConst "nil" univ, [|typ|]) +let coq_cons univ typ = EConstr.mkApp (mkListConst "cons" univ, [|typ|]) +let coq_nil univ typ = EConstr.mkApp (mkListConst "nil" univ, [|typ|]) let mk_list univ typ l = let rec loop = function | [] -> coq_nil univ typ | (step :: l) -> - mkApp (coq_cons univ typ, [| step; loop l |]) in + EConstr.mkApp (coq_cons univ typ, [| step; loop l |]) in loop l -let mk_plist = +let mk_plist = let type1lev = Universes.new_univ_level () in - fun l -> mk_list type1lev mkProp l + fun l -> mk_list type1lev EConstr.mkProp l let mk_list = mk_list Univ.Level.set type parse_term = - | Tplus of constr * constr - | Tmult of constr * constr - | Tminus of constr * constr - | Topp of constr - | Tsucc of constr + | Tplus of EConstr.t * EConstr.t + | Tmult of EConstr.t * EConstr.t + | Tminus of EConstr.t * EConstr.t + | Topp of EConstr.t + | Tsucc of EConstr.t | Tnum of Bigint.bigint | Tother type parse_rel = - | Req of constr * constr - | Rne of constr * constr - | Rlt of constr * constr - | Rle of constr * constr - | Rgt of constr * constr - | Rge of constr * constr + | Req of EConstr.t * EConstr.t + | Rne of EConstr.t * EConstr.t + | Rlt of EConstr.t * EConstr.t + | Rle of EConstr.t * EConstr.t + | Rgt of EConstr.t * EConstr.t + | Rge of EConstr.t * EConstr.t | Rtrue | Rfalse - | Rnot of constr - | Ror of constr * constr - | Rand of constr * constr - | Rimp of constr * constr - | Riff of constr * constr + | Rnot of EConstr.t + | Ror of EConstr.t * EConstr.t + | Rand of EConstr.t * EConstr.t + | Rimp of EConstr.t * EConstr.t + | Riff of EConstr.t * EConstr.t | Rother -let parse_logic_rel c = match destructurate c with +let parse_logic_rel sigma c = match destructurate sigma c with | Kapp("True",[]) -> Rtrue | Kapp("False",[]) -> Rfalse | Kapp("not",[t]) -> Rnot t @@ -211,29 +226,29 @@ let rec mk_positive n = if Bigint.equal n Bigint.one then Lazy.force coq_xH else let (q,r) = Bigint.euclid n Bigint.two in - mkApp + EConstr.mkApp ((if Bigint.equal r Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI), [| mk_positive q |]) let mk_N = function | 0 -> Lazy.force coq_N0 - | n -> mkApp (Lazy.force coq_Npos, + | n -> EConstr.mkApp (Lazy.force coq_Npos, [| mk_positive (Bigint.of_int n) |]) module type Int = sig - val typ : constr Lazy.t - val is_int_typ : Proofview.Goal.t -> constr -> bool - val plus : constr Lazy.t - val mult : constr Lazy.t - val opp : constr Lazy.t - val minus : constr Lazy.t - - val mk : Bigint.bigint -> constr - val parse_term : constr -> parse_term - val parse_rel : Proofview.Goal.t -> constr -> parse_rel + val typ : EConstr.t Lazy.t + val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool + val plus : EConstr.t Lazy.t + val mult : EConstr.t Lazy.t + val opp : EConstr.t Lazy.t + val minus : EConstr.t Lazy.t + + val mk : Bigint.bigint -> EConstr.t + val parse_term : Evd.evar_map -> EConstr.t -> parse_term + val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel (* check whether t is built only with numbers and + * - *) - val get_scalar : constr -> Bigint.bigint option + val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option end module Z : Int = struct @@ -244,9 +259,9 @@ let mult = lazy (z_constant "Z.mul") let opp = lazy (z_constant "Z.opp") let minus = lazy (z_constant "Z.sub") -let recognize_pos t = +let recognize_pos sigma t = let rec loop t = - let f,l = dest_const_apply t in + let f,l = dest_const_apply sigma t in match Id.to_string f,l with | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) | "xO",[t] -> Bigint.mult Bigint.two (loop t) @@ -255,12 +270,12 @@ let recognize_pos t = in try Some (loop t) with DestConstApp -> None -let recognize_Z t = +let recognize_Z sigma t = try - let f,l = dest_const_apply t in + let f,l = dest_const_apply sigma t in match Id.to_string f,l with - | "Zpos",[t] -> recognize_pos t - | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos t) + | "Zpos",[t] -> recognize_pos sigma t + | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos sigma t) | "Z0",[] -> Some Bigint.zero | _ -> None with DestConstApp -> None @@ -268,14 +283,14 @@ let recognize_Z t = let mk_Z n = if Bigint.equal n Bigint.zero then Lazy.force coq_Z0 else if Bigint.is_strictly_pos n then - mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) + EConstr.mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) else - mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) + EConstr.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) let mk = mk_Z -let parse_term t = - match destructurate t with +let parse_term sigma t = + match destructurate sigma t with | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2) | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2) | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2) @@ -283,35 +298,35 @@ let parse_term t = | Kapp("Z.succ",[t]) -> Tsucc t | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - (match recognize_Z t with Some t -> Tnum t | None -> Tother) + (match recognize_Z sigma t with Some t -> Tnum t | None -> Tother) | _ -> Tother let is_int_typ gl t = - Tacmach.New.pf_apply Reductionops.is_conv gl - (EConstr.of_constr t) (EConstr.of_constr (Lazy.force coq_Z)) + Tacmach.New.pf_apply Reductionops.is_conv gl t (Lazy.force coq_Z) let parse_rel gl t = - match destructurate t with + let sigma = Proofview.Goal.sigma gl in + match destructurate sigma t with | Kapp("eq",[typ;t1;t2]) when is_int_typ gl typ -> Req (t1,t2) | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2) | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2) - | _ -> parse_logic_rel t + | _ -> parse_logic_rel sigma t -let rec get_scalar t = - match destructurate t with +let rec get_scalar sigma t = + match destructurate sigma t with | Kapp("Z.add", [t1;t2]) -> - Option.lift2 Bigint.add (get_scalar t1) (get_scalar t2) + Option.lift2 Bigint.add (get_scalar sigma t1) (get_scalar sigma t2) | Kapp ("Z.sub",[t1;t2]) -> - Option.lift2 Bigint.sub (get_scalar t1) (get_scalar t2) + Option.lift2 Bigint.sub (get_scalar sigma t1) (get_scalar sigma t2) | Kapp ("Z.mul",[t1;t2]) -> - Option.lift2 Bigint.mult (get_scalar t1) (get_scalar t2) - | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar t) - | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar t) - | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar t) - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z t + Option.lift2 Bigint.mult (get_scalar sigma t1) (get_scalar sigma t2) + | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar sigma t) + | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar sigma t) + | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar sigma t) + | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z sigma t | _ -> None end diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index ecddc55de2..64668df007 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -8,117 +8,116 @@ (** Coq objects used in romega *) -open Constr (* from Logic *) -val coq_refl_equal : constr lazy_t -val coq_and : constr lazy_t -val coq_not : constr lazy_t -val coq_or : constr lazy_t -val coq_True : constr lazy_t -val coq_False : constr lazy_t -val coq_I : constr lazy_t +val coq_refl_equal : EConstr.t lazy_t +val coq_and : EConstr.t lazy_t +val coq_not : EConstr.t lazy_t +val coq_or : EConstr.t lazy_t +val coq_True : EConstr.t lazy_t +val coq_False : EConstr.t lazy_t +val coq_I : EConstr.t lazy_t (* from ReflOmegaCore/ZOmega *) -val coq_t_int : constr lazy_t -val coq_t_plus : constr lazy_t -val coq_t_mult : constr lazy_t -val coq_t_opp : constr lazy_t -val coq_t_minus : constr lazy_t -val coq_t_var : constr lazy_t - -val coq_proposition : constr lazy_t -val coq_p_eq : constr lazy_t -val coq_p_leq : constr lazy_t -val coq_p_geq : constr lazy_t -val coq_p_lt : constr lazy_t -val coq_p_gt : constr lazy_t -val coq_p_neq : constr lazy_t -val coq_p_true : constr lazy_t -val coq_p_false : constr lazy_t -val coq_p_not : constr lazy_t -val coq_p_or : constr lazy_t -val coq_p_and : constr lazy_t -val coq_p_imp : constr lazy_t -val coq_p_prop : constr lazy_t - -val coq_s_bad_constant : constr lazy_t -val coq_s_divide : constr lazy_t -val coq_s_not_exact_divide : constr lazy_t -val coq_s_sum : constr lazy_t -val coq_s_merge_eq : constr lazy_t -val coq_s_split_ineq : constr lazy_t - -val coq_direction : constr lazy_t -val coq_d_left : constr lazy_t -val coq_d_right : constr lazy_t - -val coq_e_split : constr lazy_t -val coq_e_extract : constr lazy_t -val coq_e_solve : constr lazy_t - -val coq_interp_sequent : constr lazy_t -val coq_do_omega : constr lazy_t - -val mk_nat : int -> constr -val mk_N : int -> constr +val coq_t_int : EConstr.t lazy_t +val coq_t_plus : EConstr.t lazy_t +val coq_t_mult : EConstr.t lazy_t +val coq_t_opp : EConstr.t lazy_t +val coq_t_minus : EConstr.t lazy_t +val coq_t_var : EConstr.t lazy_t + +val coq_proposition : EConstr.t lazy_t +val coq_p_eq : EConstr.t lazy_t +val coq_p_leq : EConstr.t lazy_t +val coq_p_geq : EConstr.t lazy_t +val coq_p_lt : EConstr.t lazy_t +val coq_p_gt : EConstr.t lazy_t +val coq_p_neq : EConstr.t lazy_t +val coq_p_true : EConstr.t lazy_t +val coq_p_false : EConstr.t lazy_t +val coq_p_not : EConstr.t lazy_t +val coq_p_or : EConstr.t lazy_t +val coq_p_and : EConstr.t lazy_t +val coq_p_imp : EConstr.t lazy_t +val coq_p_prop : EConstr.t lazy_t + +val coq_s_bad_constant : EConstr.t lazy_t +val coq_s_divide : EConstr.t lazy_t +val coq_s_not_exact_divide : EConstr.t lazy_t +val coq_s_sum : EConstr.t lazy_t +val coq_s_merge_eq : EConstr.t lazy_t +val coq_s_split_ineq : EConstr.t lazy_t + +val coq_direction : EConstr.t lazy_t +val coq_d_left : EConstr.t lazy_t +val coq_d_right : EConstr.t lazy_t + +val coq_e_split : EConstr.t lazy_t +val coq_e_extract : EConstr.t lazy_t +val coq_e_solve : EConstr.t lazy_t + +val coq_interp_sequent : EConstr.t lazy_t +val coq_do_omega : EConstr.t lazy_t + +val mk_nat : int -> EConstr.t +val mk_N : int -> EConstr.t (** Precondition: the type of the list is in Set *) -val mk_list : constr -> constr list -> constr -val mk_plist : types list -> types +val mk_list : EConstr.t -> EConstr.t list -> EConstr.t +val mk_plist : EConstr.types list -> EConstr.types (** Analyzing a coq term *) (* The generic result shape of the analysis of a term. One-level depth, except when a number is found *) type parse_term = - Tplus of constr * constr - | Tmult of constr * constr - | Tminus of constr * constr - | Topp of constr - | Tsucc of constr + Tplus of EConstr.t * EConstr.t + | Tmult of EConstr.t * EConstr.t + | Tminus of EConstr.t * EConstr.t + | Topp of EConstr.t + | Tsucc of EConstr.t | Tnum of Bigint.bigint | Tother (* The generic result shape of the analysis of a relation. One-level depth. *) type parse_rel = - Req of constr * constr - | Rne of constr * constr - | Rlt of constr * constr - | Rle of constr * constr - | Rgt of constr * constr - | Rge of constr * constr + Req of EConstr.t * EConstr.t + | Rne of EConstr.t * EConstr.t + | Rlt of EConstr.t * EConstr.t + | Rle of EConstr.t * EConstr.t + | Rgt of EConstr.t * EConstr.t + | Rge of EConstr.t * EConstr.t | Rtrue | Rfalse - | Rnot of constr - | Ror of constr * constr - | Rand of constr * constr - | Rimp of constr * constr - | Riff of constr * constr + | Rnot of EConstr.t + | Ror of EConstr.t * EConstr.t + | Rand of EConstr.t * EConstr.t + | Rimp of EConstr.t * EConstr.t + | Riff of EConstr.t * EConstr.t | Rother (* A module factorizing what we should now about the number representation *) module type Int = sig (* the coq type of the numbers *) - val typ : constr Lazy.t + val typ : EConstr.t Lazy.t (* Is a constr expands to the type of these numbers *) - val is_int_typ : Proofview.Goal.t -> constr -> bool + val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool (* the operations on the numbers *) - val plus : constr Lazy.t - val mult : constr Lazy.t - val opp : constr Lazy.t - val minus : constr Lazy.t + val plus : EConstr.t Lazy.t + val mult : EConstr.t Lazy.t + val opp : EConstr.t Lazy.t + val minus : EConstr.t Lazy.t (* building a coq number *) - val mk : Bigint.bigint -> constr + val mk : Bigint.bigint -> EConstr.t (* parsing a term (one level, except if a number is found) *) - val parse_term : constr -> parse_term + val parse_term : Evd.evar_map -> EConstr.t -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : Proofview.Goal.t -> constr -> parse_rel + val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel (* Is a particular term only made of numbers and + * - ? *) - val get_scalar : constr -> Bigint.bigint option + val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option end (* Currently, we only use Z numbers *) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 54ff44fbd3..d182497840 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,7 +8,6 @@ open Pp open Util -open Constr open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -67,14 +66,14 @@ type comparaison = Eq | Leq | Geq | Gt | Lt | Neq (it could contains some [Term.Var] but no [Term.Rel]). So no need to lift when breaking or creating arrows. *) type oproposition = - Pequa of constr * oequation (* constr = copy of the Coq formula *) + Pequa of EConstr.t * oequation (* constr = copy of the Coq formula *) | Ptrue | Pfalse | Pnot of oproposition | Por of int * oproposition * oproposition | Pand of int * oproposition * oproposition | Pimp of int * oproposition * oproposition - | Pprop of constr + | Pprop of EConstr.t (* The equations *) and oequation = { @@ -101,9 +100,9 @@ and oequation = { type environment = { (* La liste des termes non reifies constituant l'environnement global *) - mutable terms : constr list; + mutable terms : EConstr.t list; (* La meme chose pour les propositions *) - mutable props : constr list; + mutable props : EConstr.t list; (* Traduction des indices utilisés ici en les indices finaux utilisés par * la tactique Omega après dénombrement des variables utiles *) real_indices : int IntHtbl.t; @@ -185,7 +184,7 @@ let print_env_reification env = | t :: l -> let sigma, env = Pfedit.get_current_context () in let s = Printf.sprintf "(%c%02d)" c i in - spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + spc () ++ str s ++ str " := " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++ loop c (succ i) l in let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in @@ -218,8 +217,8 @@ let display_omega_var i = Printf.sprintf "OV%d" i l'environnement initial contenant tout. Il faudra le réduire après calcul des variables utiles. *) -let add_reified_atom t env = - try List.index0 Constr.equal t env.terms +let add_reified_atom sigma t env = + try List.index0 (EConstr.eq_constr sigma) t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i @@ -236,8 +235,8 @@ let set_reified_atom v t env = (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) -let add_prop env t = - try List.index0 Constr.equal t env.props +let add_prop sigma env t = + try List.index0 (EConstr.eq_constr sigma) t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i @@ -290,7 +289,7 @@ let oformula_of_omega af = in loop af.body -let app f v = mkApp(Lazy.force f,v) +let app f v = EConstr.mkApp(Lazy.force f,v) (* \subsection{Oformula vers COQ reel} *) @@ -347,18 +346,19 @@ let reified_conn = function | Pimp _ -> app coq_p_imp | _ -> assert false -let rec reified_of_oprop env t = match t with +let rec reified_of_oprop sigma env t = match t with | Pequa (_,{ e_comp=cmp; e_left=t1; e_right=t2 }) -> reified_cmp cmp [| reified_of_formula env t1; reified_of_formula env t2 |] | Ptrue -> Lazy.force coq_p_true | Pfalse -> Lazy.force coq_p_false - | Pnot t -> app coq_p_not [| reified_of_oprop env t |] + | Pnot t -> app coq_p_not [| reified_of_oprop sigma env t |] | Por (_,t1,t2) | Pand (_,t1,t2) | Pimp (_,t1,t2) -> - reified_conn t [| reified_of_oprop env t1; reified_of_oprop env t2 |] - | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |] + reified_conn t + [| reified_of_oprop sigma env t1; reified_of_oprop sigma env t2 |] + | Pprop t -> app coq_p_prop [| mk_nat (add_prop sigma env t) |] -let reified_of_proposition env f = - try reified_of_oprop env f +let reified_of_proposition sigma env f = + try reified_of_oprop sigma env f with reraise -> pprint stderr f; raise reraise let reified_of_eq env (l,r) = @@ -475,28 +475,28 @@ let mkPor i x y = Por (i,x,y) let mkPand i x y = Pand (i,x,y) let mkPimp i x y = Pimp (i,x,y) -let rec oformula_of_constr env t = - match Z.parse_term t with - | Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2 - | Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2 +let rec oformula_of_constr sigma env t = + match Z.parse_term sigma t with + | Tplus (t1,t2) -> binop sigma env (fun x y -> Oplus(x,y)) t1 t2 + | Tminus (t1,t2) -> binop sigma env (fun x y -> Ominus(x,y)) t1 t2 | Tmult (t1,t2) -> - (match Z.get_scalar t1 with - | Some n -> Omult (Oint n,oformula_of_constr env t2) + (match Z.get_scalar sigma t1 with + | Some n -> Omult (Oint n,oformula_of_constr sigma env t2) | None -> - match Z.get_scalar t2 with - | Some n -> Omult (oformula_of_constr env t1, Oint n) - | None -> Oatom (add_reified_atom t env)) - | Topp t -> Oopp(oformula_of_constr env t) - | Tsucc t -> Oplus(oformula_of_constr env t, Oint one) + match Z.get_scalar sigma t2 with + | Some n -> Omult (oformula_of_constr sigma env t1, Oint n) + | None -> Oatom (add_reified_atom sigma t env)) + | Topp t -> Oopp(oformula_of_constr sigma env t) + | Tsucc t -> Oplus(oformula_of_constr sigma env t, Oint one) | Tnum n -> Oint n - | Tother -> Oatom (add_reified_atom t env) + | Tother -> Oatom (add_reified_atom sigma t env) -and binop env c t1 t2 = - let t1' = oformula_of_constr env t1 in - let t2' = oformula_of_constr env t2 in +and binop sigma env c t1 t2 = + let t1' = oformula_of_constr sigma env t1 in + let t2' = oformula_of_constr sigma env t2 in c t1' t2' -and binprop env (neg2,depends,origin,path) +and binprop sigma env (neg2,depends,origin,path) add_to_depends neg1 gl c t1 t2 = let i = new_connector_id env in let depends1 = if add_to_depends then Left i::depends else depends in @@ -504,41 +504,41 @@ and binprop env (neg2,depends,origin,path) if add_to_depends then IntHtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path}; let t1' = - oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in + oproposition_of_constr sigma env (neg1,depends1,origin,O_left::path) gl t1 in let t2' = - oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in + oproposition_of_constr sigma env (neg2,depends2,origin,O_right::path) gl t2 in (* On numérote le connecteur dans l'environnement. *) c i t1' t2' -and mk_equation env ctxt c connector t1 t2 = - let t1' = oformula_of_constr env t1 in - let t2' = oformula_of_constr env t2 in +and mk_equation sigma env ctxt c connector t1 t2 = + let t1' = oformula_of_constr sigma env t1 in + let t2' = oformula_of_constr sigma env t2 in (* On ajoute l'equation dans l'environnement. *) let omega = normalize_equation env ctxt connector t1' t2' in add_equation env omega; Pequa (c,omega) -and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = +and oproposition_of_constr sigma env ((negated,depends,origin,path) as ctxt) gl c = match Z.parse_rel gl c with - | Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2 - | Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2 - | Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2 - | Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2 - | Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2 - | Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2 + | Req (t1,t2) -> mk_equation sigma env ctxt c Eq t1 t2 + | Rne (t1,t2) -> mk_equation sigma env ctxt c Neq t1 t2 + | Rle (t1,t2) -> mk_equation sigma env ctxt c Leq t1 t2 + | Rlt (t1,t2) -> mk_equation sigma env ctxt c Lt t1 t2 + | Rge (t1,t2) -> mk_equation sigma env ctxt c Geq t1 t2 + | Rgt (t1,t2) -> mk_equation sigma env ctxt c Gt t1 t2 | Rtrue -> Ptrue | Rfalse -> Pfalse | Rnot t -> let ctxt' = (not negated, depends, origin,(O_mono::path)) in - Pnot (oproposition_of_constr env ctxt' gl t) - | Ror (t1,t2) -> binprop env ctxt (not negated) negated gl mkPor t1 t2 - | Rand (t1,t2) -> binprop env ctxt negated negated gl mkPand t1 t2 + Pnot (oproposition_of_constr sigma env ctxt' gl t) + | Ror (t1,t2) -> binprop sigma env ctxt (not negated) negated gl mkPor t1 t2 + | Rand (t1,t2) -> binprop sigma env ctxt negated negated gl mkPand t1 t2 | Rimp (t1,t2) -> - binprop env ctxt (not negated) (not negated) gl mkPimp t1 t2 + binprop sigma env ctxt (not negated) (not negated) gl mkPimp t1 t2 | Riff (t1,t2) -> (* No lifting here, since Omega only works on closed propositions. *) - binprop env ctxt negated negated gl mkPand - (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) + binprop sigma env ctxt negated negated gl mkPand + (EConstr.mkArrow t1 t2) (EConstr.mkArrow t2 t1) | _ -> Pprop c (* Destructuration des hypothèses et de la conclusion *) @@ -553,27 +553,25 @@ let display_gl env t_concl t_lhyps = type defined = Defined | Assumed -let reify_hyp env gl i = +let reify_hyp sigma env gl i = let open Context.Named.Declaration in let ctxt = (false,[],i,[]) in match Tacmach.New.pf_get_hyp i gl with - | LocalDef (_,d,t) when Z.is_int_typ gl (EConstr.Unsafe.to_constr t) -> - let d = EConstr.Unsafe.to_constr d in + | LocalDef (_,d,t) when Z.is_int_typ gl t -> let dummy = Lazy.force coq_True in - let p = mk_equation env ctxt dummy Eq (mkVar i) d in + let p = mk_equation sigma env ctxt dummy Eq (EConstr.mkVar i) d in i,Defined,p | LocalDef (_,_,t) | LocalAssum (_,t) -> - let t = EConstr.Unsafe.to_constr t in - let p = oproposition_of_constr env ctxt gl t in + let p = oproposition_of_constr sigma env ctxt gl t in i,Assumed,p let reify_gl env gl = + let sigma = Proofview.Goal.sigma gl in let concl = Tacmach.New.pf_concl gl in - let concl = EConstr.Unsafe.to_constr concl in let hyps = Tacmach.New.pf_ids_of_hyps gl in let ctxt_concl = (true,[],id_concl,[O_mono]) in - let t_concl = oproposition_of_constr env ctxt_concl gl concl in - let t_lhyps = List.map (reify_hyp env gl) hyps in + let t_concl = oproposition_of_constr sigma env ctxt_concl gl concl in + let t_lhyps = List.map (reify_hyp sigma env gl) hyps in let () = if !debug then display_gl env t_concl t_lhyps in t_concl, t_lhyps @@ -684,8 +682,7 @@ let rec stated_in_tree = function | Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2) | Leaf s -> stated_in_trace s.s_trace -let mk_refl t = - EConstr.of_constr (app coq_refl_equal [|Lazy.force Z.typ; t|]) +let mk_refl t = app coq_refl_equal [|Lazy.force Z.typ; t|] let digest_stated_equations env tree = let do_equation st (vars,gens,eqns,ids) = @@ -775,7 +772,7 @@ let maximize_prop equas c = | t1', t2' -> Pand(i,t1',t2')) | Pimp(i,t1,t2) -> (match loop t1, loop t2 with - | Pprop p1, Pprop p2 -> Pprop (Term.mkArrow p1 p2) (* no lift (closed) *) + | Pprop p1, Pprop p2 -> Pprop (EConstr.mkArrow p1 p2) (* no lift (closed) *) | t1', t2' -> Pimp(i,t1',t2')) | Ptrue -> Pprop (app coq_True [||]) | Pfalse -> Pprop (app coq_False [||]) @@ -852,12 +849,15 @@ let hyp_idx env_hyp i = a O_SUM followed by a O_BAD_CONSTANT *) let sum_bad inv i1 i2 = + let open EConstr in mkApp (Lazy.force coq_s_sum, [| Z.mk Bigint.one; i1; Z.mk (if inv then negone else Bigint.one); i2; mkApp (Lazy.force coq_s_bad_constant, [| mk_nat 0 |])|]) -let rec reify_trace env env_hyp = function +let rec reify_trace env env_hyp = + let open EConstr in + function | CONSTANT_NOT_NUL(e,_) :: [] | CONSTANT_NEG(e,_) :: [] | CONSTANT_NUL e :: [] -> @@ -958,7 +958,7 @@ l'extraction d'un ensemble minimal de solutions permettant la résolution globale du système et enfin construit la trace qui permet de faire rejouer cette solution par la tactique réflexive. *) -let resolution unsafe env (reified_concl,reified_hyps) systems_list = +let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list = if !debug then Printf.printf "\n====================================\n"; let all_solutions = List.mapi (solve_system env) systems_list in let solution_tree = solve_with_constraints all_solutions [] in @@ -1006,15 +1006,15 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = (** The environment [env] (and especially [env.real_indices]) is now ready for the coming reifications: *) let l_reified_stated = List.map (reified_of_eq env) to_reify_stated in - let reified_concl = reified_of_proposition env reified_concl in + let reified_concl = reified_of_proposition sigma env reified_concl in let l_reified_terms = List.map (fun id -> match Id.Map.find id reified_hyps with | Defined,p -> - reified_of_proposition env p, mk_refl (mkVar id) + reified_of_proposition sigma env p, mk_refl (EConstr.mkVar id) | Assumed,p -> - reified_of_proposition env (maximize_prop useful_equa_ids p), + reified_of_proposition sigma env (maximize_prop useful_equa_ids p), EConstr.mkVar id | exception Not_found -> assert false) useful_hypnames @@ -1036,17 +1036,16 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = let decompose_tactic = decompose_tree env context solution_tree in Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >> - Tactics.convert_concl_no_check (EConstr.of_constr reified) Term.DEFAULTcast >> - Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >> + Tactics.convert_concl_no_check reified Term.DEFAULTcast >> + Tactics.apply (app coq_do_omega [|decompose_tactic|]) >> show_goal >> (if unsafe then (* Trust the produced term. Faster, but might fail later at Qed. Also handy when debugging, e.g. via a Show Proof after romega. *) - Tactics.convert_concl_no_check - (EConstr.of_constr (Lazy.force coq_True)) Term.VMcast + Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast else Tactics.normalise_vm_in_concl) >> - Tactics.apply (EConstr.of_constr (Lazy.force coq_I)) + Tactics.apply (Lazy.force coq_I) let total_reflexive_omega_tactic unsafe = Proofview.Goal.nf_enter begin fun gl -> @@ -1064,7 +1063,8 @@ let total_reflexive_omega_tactic unsafe = List.fold_left (fun s (id,d,p) -> Id.Map.add id (d,p) s) Id.Map.empty hyps in if !debug then display_systems systems_list; - resolution unsafe env (concl,hyps) systems_list + let sigma = Proofview.Goal.sigma gl in + resolution unsafe sigma env (concl,hyps) systems_list with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") end diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index db17c0d654..06cdf76b4e 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -11,7 +11,7 @@ Require Export List. Require Export Bintree. -Require Import Bool. +Require Import Bool BinPos. Declare ML Module "rtauto_plugin". @@ -98,8 +98,6 @@ match F with | F_push H hyps0 F0 => interp_ctx hyps0 F0 ([[H]] -> G) end. -Require Export BinPos. - Ltac wipe := intros;simpl;constructor. Lemma compose0 : @@ -257,122 +255,115 @@ Theorem interp_proof: forall p hyps F gl, check_proof hyps gl p = true -> interp_ctx hyps F [[gl]]. -induction p;intros hyps F gl. - -(* cas Axiom *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f nth_f e;rewrite <- (form_eq_refl e). -apply project with p;trivial. - -(* Cas Arrow_Intro *) -Focus 1. -destruct gl;clean. -simpl;intros. -change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). -apply IHp;try constructor;trivial. - -(* Cas Arrow_Elim *) -Focus 1. -simpl check_proof;case_eq (get p hyps);clean. -intros f ef;case_eq (get p0 hyps);clean. -intros f0 ef0;destruct f0;clean. -case_eq (form_eq f f0_1);clean. -simpl;intros e check_p1. -generalize (project F ef) (project F ef0) -(IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); -clear check_p1 IHp p p0 p1 ef ef0. -simpl. -apply compose3. -rewrite (form_eq_refl e). -auto. - -(* cas Arrow_Destruct *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean. -intros check_p1 check_p2. -generalize (project F ef) -(IHp1 (hyps \ f1_2 =>> f2 \ f1_1) -(F_push f1_1 (hyps \ f1_2 =>> f2) - (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). -simpl;apply compose3;auto. - -(* Cas False_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intros _; generalize (project F ef). -apply compose1;apply False_ind. - -(* Cas And_Intro *) -Focus 1. -simpl;destruct gl;clean. -case_eq (check_proof hyps gl1 p1);clean. -intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). -apply compose2 ;simpl;auto. - -(* cas And_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intro check_p;generalize (project F ef) -(IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). -simpl;apply compose2;intros [h1 h2];auto. - -(* cas And_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro H;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f1_2 =>> f2) -(F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl. -apply compose2;auto. - -(* cas Or_Intro_left *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl1 Hp). -apply compose1;simpl;auto. - -(* cas Or_Intro_right *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl2 Hp). -apply compose1;simpl;auto. - -(* cas Or_elim *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -case_eq (check_proof (hyps \ f1) gl p2);clean. -intros check_p1 check_p2;generalize (project F ef) -(IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); -simpl;apply compose3;simpl;intro h;destruct h;auto. - -(* cas Or_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro check_p0;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) -(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) - (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl. -apply compose2;auto. - -(* cas Cut *) -Focus 1. -simpl;case_eq (check_proof hyps f p1);clean. -intros check_p1 check_p2; -generalize (IHp1 hyps F f check_p1) -(IHp2 (hyps\f) (F_push f hyps F) gl check_p2); -simpl; apply compose2;auto. +induction p; intros hyps F gl. + +- (* Axiom *) + simpl;case_eq (get p hyps);clean. + intros f nth_f e;rewrite <- (form_eq_refl e). + apply project with p;trivial. + +- (* Arrow_Intro *) + destruct gl; clean. + simpl; intros. + change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). + apply IHp; try constructor; trivial. + +- (* Arrow_Elim *) + simpl check_proof; case_eq (get p hyps); clean. + intros f ef; case_eq (get p0 hyps); clean. + intros f0 ef0; destruct f0; clean. + case_eq (form_eq f f0_1); clean. + simpl; intros e check_p1. + generalize (project F ef) (project F ef0) + (IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); + clear check_p1 IHp p p0 p1 ef ef0. + simpl. + apply compose3. + rewrite (form_eq_refl e). + auto. + +- (* Arrow_Destruct *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2); clean. + intros check_p1 check_p2. + generalize (project F ef) + (IHp1 (hyps \ f1_2 =>> f2 \ f1_1) + (F_push f1_1 (hyps \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). + simpl; apply compose3; auto. + +- (* False_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intros _; generalize (project F ef). + apply compose1; apply False_ind. + +- (* And_Intro *) + simpl; destruct gl; clean. + case_eq (check_proof hyps gl1 p1); clean. + intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). + apply compose2 ; simpl; auto. + +- (* And_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intro check_p; + generalize (project F ef) + (IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). + simpl; apply compose2; intros [h1 h2]; auto. + +- (* And_Destruct*) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro H; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f1_2 =>> f2) + (F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H); + clear H; simpl. + apply compose2; auto. + +- (* Or_Intro_left *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl1 Hp). + apply compose1; simpl; auto. + +- (* Or_Intro_right *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl2 Hp). + apply compose1; simpl; auto. + +- (* Or_elim *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + case_eq (check_proof (hyps \ f1) gl p2); clean. + intros check_p1 check_p2; + generalize (project F ef) + (IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); + simpl; apply compose3; simpl; intro h; destruct h; auto. + +- (* Or_Destruct *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro check_p0; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) + (F_push (f1_1 =>> f2) hyps F)) gl check_p0); + simpl. + apply compose2; auto. + +- (* Cut *) + simpl; case_eq (check_proof hyps f p1); clean. + intros check_p1 check_p2; + generalize (IHp1 hyps F f check_p1) + (IHp2 (hyps\f) (F_push f hyps F) gl check_p2); + simpl; apply compose2; auto. Qed. Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True. diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e2ec8d72ae..f049963f1c 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -460,7 +460,7 @@ let red_product_skip_id env sigma c = match EConstr.kind sigma c with let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac -(** Open term to lambda-term coercion {{{ ************************************) +(** Open term to lambda-term coercion *)(* {{{ ************************************) (* This operation takes a goal gl and an open term (sigma, t), and *) (* returns a term t' where all the new evars in sigma are abstracted *) @@ -768,7 +768,7 @@ let discharge_hyp (id', (id, mode)) gl = let cl' = Vars.subst_var id (pf_concl gl) in match pf_get_hyp gl id, mode with | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" -> - Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl'))) + Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl'))) [EConstr.of_constr (mkVar id)]) gl | NamedDecl.LocalDef (_, v, t), _ -> Proofview.V82.of_tactic @@ -1000,7 +1000,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error -(** Profiling {{{ *************************************************************) +(** Profiling *)(* {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; @@ -1128,7 +1128,7 @@ let interp_clr sigma = function (** Basic tacticals *) -(** Multipliers {{{ ***********************************************************) +(** Multipliers *)(* {{{ ***********************************************************) (* tactical *) @@ -1168,7 +1168,7 @@ let tclMULT = function let old_cleartac clr = check_hyps_uniq [] clr; Proofview.V82.of_tactic (Tactics.clear (hyps_ids clr)) let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr) -(** }}} *) +(* }}} *) (** Generalize tactic *) @@ -1199,7 +1199,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs) let genclrtac cl cs clr = let tclmyORELSE tac1 tac2 gl = diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 7c16e1ba91..2b8f1d5409 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -414,6 +414,8 @@ val clr_of_wgen : val unfold : EConstr.t list -> unit Proofview.tactic +val apply_type : EConstr.types -> EConstr.t list -> Proofview.V82.tac + (* New code ****************************************************************) (* To call old code *) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 33ebe26b6c..717657a247 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -30,8 +30,6 @@ module RelDecl = Context.Rel.Declaration (** The "case" and "elim" tactic *) -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - (* TASSI: given the type of an elimination principle, it finds the higher order * argument (index), it computes it's arity and the arity of the eliminator and * checks if the eliminator is recursive or not *) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 7f0b77c9ee..57635edac4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -372,8 +372,6 @@ let is_construct_ref sigma c r = EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - let rwcltac cl rdx dir sr gl = let n, r_n,_, ucst = pf_abs_evars gl sr in let r_n' = pf_abs_cterm gl n r_n in diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 96b6ed2957..ac2c78249b 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -165,7 +165,7 @@ Require Import ssreflect. (* rev_right_loop inv op <-> op, inv obey the inverse loop reverse right *) (* axiom: (x op y) op (inv y) = x for all x, y. *) (* Note that familiar "cancellation" identities like x + y - y = x or *) -(* x - y + x = x are respectively instances of right_loop and rev_right_loop *) +(* x - y + y = x are respectively instances of right_loop and rev_right_loop *) (* The corresponding lemmas will use the K and NK/VK suffixes, respectively. *) (* *) (* - Morphisms for functions and relations: *) @@ -639,6 +639,9 @@ End Injections. Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. +(* Force implicits to use as a view. *) +Prenex Implicits Some_inj. + (* cancellation lemmas for dependent type casts. *) Lemma esymK T x y : cancel (@esym T x y) (@esym T y x). Proof. by case: y /. Qed. diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 70f73c1fe7..2bed8b624b 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -952,7 +952,7 @@ let pr_ssrhint _ _ = pr_hint ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint | [ ] -> [ nohint ] END -(** The "in" pseudo-tactical {{{ **********************************************) +(** The "in" pseudo-tactical *)(* {{{ **********************************************) (* We can't make "in" into a general tactical because this would create a *) (* crippling conflict with the ltac let .. in construct. Hence, we add *) @@ -1438,7 +1438,7 @@ let tactic_expr = Pltac.tactic_expr let old_tac = V82.tactic -(** Name generation {{{ *******************************************************) +(** Name generation *)(* {{{ *******************************************************) (* Since Coq now does repeated internal checks of its external lexical *) (* rules, we now need to carve ssreflect reserved identifiers out of *) @@ -1490,7 +1490,7 @@ let _ = add_internal_name (is_tagged perm_tag) (* We must not anonymize context names discharged by the "in" tactical. *) -(** Tactical extensions. {{{ **************************************************) +(** Tactical extensions. *)(* {{{ **************************************************) (* The TACTIC EXTEND facility can't be used for defining new user *) (* tacticals, because: *) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 21ad6e6ced..9cc4f5cece 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -59,7 +59,7 @@ let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) = | L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3 | R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad)) -(** The "in" pseudo-tactical {{{ **********************************************) +(** The "in" pseudo-tactical *)(* {{{ **********************************************) let hidden_goal_tag = "the_hidden_goal" @@ -127,8 +127,6 @@ let endclausestac id_map clseq gl_id cl0 gl = if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - let tclCLAUSES tac (gens, clseq) gl = if clseq = InGoal || clseq = InSeqGoal then tac gl else let clr_gens = pf_clauseids gl gens clseq in diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index f374526131..e3941c1c5d 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -49,7 +49,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; (* global syntactic changes and vernacular commands *) -(** Alternative notations for "match" and anonymous arguments. {{{ ************) +(** Alternative notations for "match" and anonymous arguments. *)(* {{{ ************) (* Syntax: *) (* if <term> is <pattern> then ... else ... *) @@ -127,7 +127,7 @@ GEXTEND Gram END (* }}} *) -(** Vernacular commands: Prenex Implicits and Search {{{ **********************) +(** Vernacular commands: Prenex Implicits and Search *)(* {{{ **********************) (* This should really be implemented as an extension to the implicit *) (* arguments feature, but unfortuately that API is sealed. The current *) @@ -461,7 +461,7 @@ END (* }}} *) -(** View hint database and View application. {{{ ******************************) +(** View hint database and View application. *)(* {{{ ******************************) (* There are three databases of lemmas used to mediate the application *) (* of reflection lemmas: one for forward chaining, one for backward *) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 5ed5e47f8b..33b18001c9 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -70,7 +70,7 @@ let _ = Goptions.optwrite = debug } let pp s = !pp_ref s -(** Utils {{{ *****************************************************************) +(** Utils *)(* {{{ *****************************************************************) let env_size env = List.length (Environ.named_context env) let safeDestApp c = match kind c with App (f, a) -> f, a | _ -> c, [| |] @@ -179,7 +179,7 @@ let nf_evar sigma c = (* }}} *) -(** Profiling {{{ *************************************************************) +(** Profiling *)(* {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index cd5676f28c..07d0f97575 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -74,7 +74,7 @@ val interp_cpattern : pattern (** The set of occurrences to be matched. The boolean is set to true - * to signal the complement of this set (i.e. {-1 3}) *) + * to signal the complement of this set (i.e. \{-1 3\}) *) type occ = (bool * int list) option (** [subst e p t i]. [i] is the number of binders diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 16d75685d4..3b56513f5e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -278,7 +278,7 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. - @raises UniverseInconsistency iff catch_incon is set to false, + @raise UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli index 242eb802fa..305d045b1f 100644 --- a/pretyping/univdecls.mli +++ b/pretyping/univdecls.mli @@ -14,8 +14,8 @@ type universe_decl = val default_univ_decl : universe_decl -val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr -> +val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr -> Evd.evar_map * universe_decl -val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option -> +val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option -> Evd.evar_map * universe_decl diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8551d040dd..2b7d643d6f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -233,9 +233,9 @@ open Decl_kinds hov 2 (keyword "Hint "++ pph ++ opth) let pr_with_declaration pr_c = function - | CWith_Definition (id,c) -> + | CWith_Definition (id,udecl,c) -> let p = pr_c c in - keyword "Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p + keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p | CWith_Module (id,qid) -> keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid diff --git a/tactics/auto.ml b/tactics/auto.ml index 3eea1a74fd..0c0d9bcfc4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -42,9 +42,9 @@ let compute_secvars gl = open Unification -let auto_core_unif_flags_of st1 st2 useeager = { +let auto_core_unif_flags_of st1 st2 = { modulo_conv_on_closed_terms = Some st1; - use_metas_eagerly_in_conv_on_closed_terms = useeager; + use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; modulo_delta_types = full_transparent_state; @@ -57,8 +57,8 @@ let auto_core_unif_flags_of st1 st2 useeager = { modulo_eta = true; } -let auto_unif_flags_of st1 st2 useeager = - let flags = auto_core_unif_flags_of st1 st2 useeager in { +let auto_unif_flags_of st1 st2 = + let flags = auto_core_unif_flags_of st1 st2 in { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = { flags with modulo_delta = empty_transparent_state }; @@ -67,7 +67,7 @@ let auto_unif_flags_of st1 st2 useeager = } let auto_unif_flags = - auto_unif_flags_of full_transparent_state empty_transparent_state false + auto_unif_flags_of full_transparent_state empty_transparent_state (* Try unification with the precompiled clause, then use registered Apply *) @@ -291,10 +291,10 @@ let tclTRY_dbg d tac = de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) let flags_of_state st = - auto_unif_flags_of st st false + auto_unif_flags_of st st let auto_flags_of_state st = - auto_unif_flags_of full_transparent_state st false + auto_unif_flags_of full_transparent_state st let hintmap_of sigma secvars hdc concl = match hdc with diff --git a/tactics/equality.ml b/tactics/equality.ml index 236db1dcc1..98f627f211 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -56,18 +56,7 @@ type inj_flags = { injection_pattern_l2r_order : bool; } -let discriminate_introduction = ref true - -let discr_do_intro () = !discriminate_introduction - open Goptions -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic introduction of hypotheses by discriminate"; - optkey = ["Discriminate";"Introduction"]; - optread = (fun () -> !discriminate_introduction); - optwrite = (:=) discriminate_introduction } let use_injection_pattern_l2r_order = function | None -> true @@ -1080,13 +1069,10 @@ let discrClause with_evars = onClause (discrSimpleClause with_evars) let discrEverywhere with_evars = tclTHEN (Proofview.tclUNIT ()) (* Delay the interpretation of side-effect *) - (if discr_do_intro () then - (tclTHEN - (tclREPEAT introf) - (tryAllHyps + (tclTHEN + (tclREPEAT introf) + (tryAllHyps (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) - else (* <= 8.2 compat *) - tryAllHypsAndConcl (discrSimpleClause with_evars)) let discr_tac with_evars = function | None -> discrEverywhere with_evars diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index a59046a678..b012a7ecd1 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -511,10 +511,10 @@ let coq_eqdec ~sum ~rev = mkPattern (mkGAppRef sum args) ) -(** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *) +(** [{ ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 }] *) let coq_eqdec_inf_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:false -(** { ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 } *) +(** [{ ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 }] *) let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:true (** %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b99a451030..12aef852d0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -15,7 +15,6 @@ open CErrors open Util open Names open Nameops -open Term open Constr open Termops open Environ @@ -89,18 +88,6 @@ let _ = optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } -(* Shrinking of abstract proofs. *) - -let shrink_abstract = ref true - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "shrinking of abstracted proofs"; - optkey = ["Shrink"; "Abstract"]; - optread = (fun () -> !shrink_abstract) ; - optwrite = (fun b -> shrink_abstract := b) } - (* The following boolean governs what "intros []" do on examples such as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; if false, it behaves as "intro H; case H; clear H" for fresh H. @@ -400,12 +387,11 @@ let find_name mayrepl decl naming gl = match naming with new_fresh_id idl (default_id env sigma decl) gl | NamingBasedOn (id,idl) -> new_fresh_id idl id gl | NamingMustBe (loc,id) -> - (* When name is given, we allow to hide a global name *) - let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in - let id' = next_ident_away id ids_of_hyps in - if not mayrepl && not (Id.equal id' id) then - user_err ?loc (Id.print id ++ str" is already used."); - id + (* When name is given, we allow to hide a global name *) + let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in + if not mayrepl && Id.Set.mem id ids_of_hyps then + user_err ?loc (Id.print id ++ str" is already used."); + id (**************************************************************) (* Computing position of hypotheses for replacing *) @@ -1339,46 +1325,6 @@ let index_of_ind_arg sigma t = | None -> error "Could not find inductive argument of elimination scheme." in aux None 0 t -let enforce_prop_bound_names rename tac = - let open Context.Rel.Declaration in - match rename with - | Some (isrec,nn) when Namegen.use_h_based_elimination_names () -> - (* Rename dependent arguments in Prop with name "H" *) - (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *) - (* elim or induction with schemes built by Indrec.build_induction_scheme *) - let rec aux env sigma i t = - if i = 0 then t else match EConstr.kind sigma t with - | Prod (Name _ as na,t,t') -> - let very_standard = true in - let na = - if Retyping.get_sort_family_of env sigma t = InProp then - (* "very_standard" says that we should have "H" names only, but - this would break compatibility even more... *) - let s = match Namegen.head_name sigma t with - | Some id when not very_standard -> Id.to_string id - | _ -> "" in - Name (add_suffix Namegen.default_prop_ident s) - else - na in - mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t') - | Prod (Anonymous,t,t') -> - mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t') - | LetIn (na,c,t,t') -> - mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t') - | _ -> assert false in - let rename_branch i = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let t = Proofview.Goal.concl gl in - change_concl (aux env sigma i t) - end in - (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) - tac - (Array.map rename_branch nn) - | _ -> - tac - let rec contract_letin_in_lam_header sigma c = match EConstr.kind sigma c with | Lambda (x,t,c) -> mkLambda (x,t,contract_letin_in_lam_header sigma c) @@ -1399,7 +1345,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags (str "The type of elimination clause is not well-formed.")) in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags) + Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags end (* @@ -4221,7 +4167,7 @@ let induction_tac with_evars params indvars elim = let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved) + Clenvtac.clenv_refine with_evars resolved end (* Apply induction "in place" taking into account dependent @@ -4986,10 +4932,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let (_, info) = CErrors.push src in iraise (e, info) in - let const, args = - if !shrink_abstract then shrink_entry sign const - else (const, List.rev (Context.Named.to_instance Constr.mkVar sign)) - in + let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in diff --git a/test-suite/bugs/closed/2245.v b/test-suite/bugs/closed/2245.v new file mode 100644 index 0000000000..f0162f3b27 --- /dev/null +++ b/test-suite/bugs/closed/2245.v @@ -0,0 +1,11 @@ +Module Type Test. + +Section Sec. +Variables (A:Type). +Context (B:Type). +End Sec. + +Fail Check B. (* used to be found !!! *) +Fail Check A. + +End Test. diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index 85ad41d1cf..23a58501f3 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -505,8 +505,6 @@ Qed. Require Export Coq.Logic.FunctionalExtensionality. Print PLanguage. -Unset Standard Proposition Elimination Names. - Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): Transformation (PLanguage l1) (PLanguage l2) := mkTransformation (PLanguage l1) (PLanguage l2) diff --git a/test-suite/bugs/closed/6634.v b/test-suite/bugs/closed/6634.v new file mode 100644 index 0000000000..7f33afcc2f --- /dev/null +++ b/test-suite/bugs/closed/6634.v @@ -0,0 +1,6 @@ +From Coq Require Import ssreflect. + +Lemma normalizeP (p : tt = tt) : p = p. +Proof. +Fail move: {2} tt p. +Abort. diff --git a/test-suite/bugs/closed/6910.v b/test-suite/bugs/closed/6910.v new file mode 100644 index 0000000000..5167a5364a --- /dev/null +++ b/test-suite/bugs/closed/6910.v @@ -0,0 +1,5 @@ +From Coq Require Import ssreflect ssrfun. + +(* We should be able to use Some_inj as a view: *) +Lemma foo (x y : nat) : Some x = Some y -> x = y. +Proof. by move/Some_inj. Qed. diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 0b576db6b3..820022d995 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -2,7 +2,6 @@ Require Import Relations. Require Import FSets. Require Import Arith. Require Import Omega. -Unset Standard Proposition Elimination Names. Set Keyed Unification. diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v new file mode 100644 index 0000000000..e683455162 --- /dev/null +++ b/test-suite/modules/WithDefUBinders.v @@ -0,0 +1,15 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo@{u v|u < v} : Type@{v}. +End T. + +Module M : T with Definition foo@{u v} := Type@{u} : Type@{v}. + Definition foo@{u v} := Type@{u} : Type@{v}. +End M. + +Fail Module M' : T with Definition foo := Type. + +(* Without the binder expression we have to do trickery to get the + universes in the right order. *) +Module M' : T with Definition foo := let t := Type in t. diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v new file mode 100644 index 0000000000..571dde8805 --- /dev/null +++ b/test-suite/success/name_mangling.v @@ -0,0 +1,192 @@ +(* -*- coq-prog-args: ("-mangle-names" "_") -*- *) + +(* Check that refine policy of redefining previous names make these names private *) +(* abstract can change names in the environment! See bug #3146 *) + +Goal True -> True. +intro. +Fail exact H. +exact _0. +Abort. + +Unset Mangle Names. +Goal True -> True. +intro; exact H. +Abort. + +Set Mangle Names. +Set Mangle Names Prefix "baz". +Goal True -> True. +intro. +Fail exact H. +Fail exact _0. +exact baz0. +Abort. + +Goal True -> True. +intro; assumption. +Abort. + +Goal True -> True. +intro x; exact x. +Abort. + +Goal forall x y, x+y=0. +intro x. +refine (fun x => _). +Fail Check x0. +Check x. +Abort. + +(* Example from Emilio *) + +Goal forall b : False, b = b. +intro b. +refine (let b := I in _). +Fail destruct b0. +Abort. + +(* Example from Cyprien *) + +Goal True -> True. +Proof. + refine (fun _ => _). + Fail exact t. +Abort. + +(* Example from Jason *) + +Goal False -> False. +intro H. +Fail abstract exact H. +Abort. + +(* Variant *) + +Goal False -> False. +intro. +Fail abstract exact H. +Abort. + +(* Example from Jason *) + +Goal False -> False. +intro H. +(* Name H' is from Ltac here, so it preserves the privacy *) +(* But abstract messes everything up *) +Fail let H' := H in abstract exact H'. +let H' := H in exact H'. +Qed. + +(* Variant *) + +Goal False -> False. +intro. +Fail let H' := H in abstract exact H'. +Abort. + +(* Indirectly testing preservation of names by move (derived from Jason) *) + +Inductive nat2 := S2 (_ _ : nat2). +Goal forall t : nat2, True. + intro t. + let IHt1 := fresh "IHt1" in + let IHt2 := fresh "IHt2" in + induction t as [? IHt1 ? IHt2]. + Fail exact IHt1. +Abort. + +(* Example on "pose proof" (from Jason) *) + +Goal False -> False. +intro; pose proof I as H0. +Fail exact H. +Abort. + +(* Testing the approach for which non alpha-renamed quantified names are user-generated *) + +Section foo. +Context (b : True). +Goal forall b : False, b = b. +Fail destruct b0. +Abort. + +Goal forall b : False, b = b. +now destruct b. +Qed. +End foo. + +(* Test stability of "fix" *) + +Lemma a : forall n, n = 0. +Proof. +fix a 1. +Check a. +fix 1. +Fail Check a0. +Abort. + +(* Test stability of "induction" *) + +Lemma a : forall n : nat, n = n. +Proof. +intro n; induction n as [ | n IHn ]. +- auto. +- Check n. + Check IHn. +Abort. + +Inductive I := C : I -> I -> I. + +Lemma a : forall n : I, n = n. +Proof. +intro n; induction n as [ n1 IHn1 n2 IHn2 ]. +Check n1. +Check n2. +apply f_equal2. ++ apply IHn1. ++ apply IHn2. +Qed. + +(* Testing remember *) + +Lemma c : 0 = 0. +Proof. +remember 0 as x eqn:Heqx. +Check Heqx. +Abort. + +Lemma c : forall Heqx, Heqx -> 0 = 0. +Proof. +intros Heqx X. +remember 0 as x. +Fail Check Heqx0. (* Heqx0 is not canonical *) +Abort. + +(* An example by Jason from the discussion for PR #268 *) + +Goal nat -> Set -> True. + intros x y. + match goal with + | [ x : _, y : _ |- _ ] + => let z := fresh "z" in + rename y into z, x into y; + let x' := fresh "x" in + rename z into x' + end. + revert y. (* x has been explicitly moved to y *) + Fail revert x. (* x comes from "fresh" *) +Abort. + +Goal nat -> Set -> True. + intros. + match goal with + | [ x : _, y : _ |- _ ] + => let z := fresh "z" in + rename y into z, x into y; + let x' := fresh "x" in + rename z into x' + end. + Fail revert y. (* generated by intros *) + Fail revert x. (* generated by intros *) +Abort. diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v index 3f6b9cb39f..916bb846a9 100644 --- a/test-suite/success/shrink_abstract.v +++ b/test-suite/success/shrink_abstract.v @@ -1,5 +1,3 @@ -Set Shrink Abstract. - Definition foo : forall (n m : nat), bool. Proof. pose (p := 0). diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 683a442cb3..72073bb4f6 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -77,6 +77,7 @@ Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). Reserved Notation "{ x : A | P }" (at level 0, x at level 99). Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). +Reserved Notation "{ x & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 137bd3a0f3..b6afba29a0 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -51,6 +51,7 @@ Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope. Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. +Notation "{ x & P }" := (sigT (fun x => P)) : type_scope. Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 9fd52866e3..238ac7df0b 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -28,6 +28,8 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. [[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997. *) +Require Import RelationClasses Logic. + Set Implicit Arguments. Local Unset Intuition Negation Unfolding. @@ -125,8 +127,6 @@ Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := formulation of choice); Note also a typo in its intended formulation in [[Werner97]]. *) -Require Import RelationClasses Logic. - Definition RepresentativeFunctionalChoice_on := forall R:A->A->Prop, (Equivalence R) -> diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index 88ab4d6e1d..afb78e1c8e 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -29,46 +29,34 @@ Lemma f_incr_implies_g_incr_interv : forall f g:R->R, forall lb ub, (forall x , f lb <= x -> x <= f ub -> lb <= g x <= ub) -> (forall x y, f lb <= x -> x < y -> y <= f ub -> g x < g y). Proof. -intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub. - assert (x_encad : f lb <= x <= f ub). - split ; [assumption | apply Rle_trans with (r2:=y) ; [apply Rlt_le|] ; assumption]. - assert (y_encad : f lb <= y <= f ub). - split ; [apply Rle_trans with (r2:=x) ; [|apply Rlt_le] ; assumption | assumption]. - assert (Temp1 : lb <= lb) by intuition ; assert (Temp2 : ub <= ub) by intuition. - assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)). - assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)). - clear Temp1 Temp2. - case (Rlt_dec (g x) (g y)). - intuition. + intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub. + assert (x_encad : f lb <= x <= f ub) by lra. + assert (y_encad : f lb <= y <= f ub) by lra. + assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)). + assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)). + case (Rlt_dec (g x) (g y)); [ easy |]. intros Hfalse. - assert (Temp := Rnot_lt_le _ _ Hfalse). - assert (Hcontradiction : y <= x). - replace y with (id y) by intuition ; replace x with (id x) by intuition ; - rewrite <- f_eq_g. rewrite <- f_eq_g. - assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y). + assert (Temp := Rnot_lt_le _ _ Hfalse). + enough (y <= x) by lra. + replace y with (id y) by easy. + replace x with (id x) by easy. + rewrite <- f_eq_g by easy. + rewrite <- f_eq_g by easy. + assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y). { intros m n lb_le_m m_le_n n_lt_ub. case (m_le_n). - intros ; apply Rlt_le ; apply f_incr ; [| | apply Rlt_le] ; assumption. - intros Hyp ; rewrite Hyp ; apply Req_le ; reflexivity. - apply f_incr2. - intuition. intuition. - Focus 3. intuition. - Focus 2. intuition. - Focus 2. intuition. Focus 2. intuition. - assert (Temp2 : g x <> ub). - intro Hf. - assert (Htemp : (comp f g) x = f ub). - unfold comp ; rewrite Hf ; reflexivity. - rewrite f_eq_g in Htemp ; unfold id in Htemp. - assert (Htemp2 : x < f ub). - apply Rlt_le_trans with (r2:=y) ; intuition. - clear -Htemp Htemp2. fourier. - intuition. intuition. - clear -Temp2 gx_encad. - case (proj2 gx_encad). - intuition. - intro Hfalse ; apply False_ind ; apply Temp2 ; assumption. - apply False_ind. clear - Hcontradiction x_lt_y. fourier. + - intros; apply Rlt_le, f_incr, Rlt_le; assumption. + - intros Hyp; rewrite Hyp; apply Req_le; reflexivity. + } + apply f_incr2; intuition. + enough (g x <> ub) by lra. + intro Hf. + assert (Htemp : (comp f g) x = f ub). { + unfold comp; rewrite Hf; reflexivity. + } + rewrite f_eq_g in Htemp by easy. + unfold id in Htemp. + fourier. Qed. Lemma derivable_pt_id_interv : forall (lb ub x:R), diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index a50140628a..a79ddead20 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -11,6 +11,7 @@ (* G. Huet 1-9-95 *) Require Import Permut Setoid. +Require Plus. (* comm. and ass. of plus *) Set Implicit Arguments. @@ -69,9 +70,6 @@ Section multiset_defs. unfold meq; unfold munion; simpl; auto. Qed. - - Require Plus. (* comm. and ass. of plus *) - Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x). Proof. unfold meq; unfold multiplicity; unfold munion. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 95ba932324..7940bda1a7 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -13,7 +13,7 @@ (* G. Huet 1-9-95 *) (* Updated Papageno 12/98 *) -Require Import Bool. +Require Import Bool Permut. Set Implicit Arguments. @@ -140,8 +140,6 @@ Hint Resolve seq_right. (** Here we should make uniset an abstract datatype, by hiding [Charac], [union], [charac]; all further properties are proved abstractly *) -Require Import Permut. - Lemma union_rotate : forall x y z:uniset, seq (union x (union y z)) (union z (union x y)). Proof. diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 8f583be97e..d9e5ad676e 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -136,7 +136,7 @@ Section defs. (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) -> (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) -> merge_lem l1 l2. - Require Import Morphisms. + Import Morphisms. Instance: Equivalence (@meq A). Proof. constructor; auto with datatypes. red. apply meq_trans. Defined. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index a302b83292..2be6618ad6 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -165,6 +165,18 @@ intros n0 H; apply Rec; simpl; auto. apply Le.le_S_n; auto. Qed. +(** *** Concatenating lists of strings *) + +(** [concat sep sl] concatenates the list of strings [sl], inserting + the separator string [sep] between each. *) + +Fixpoint concat (sep : string) (ls : list string) := + match ls with + | nil => EmptyString + | cons x nil => x + | cons x xs => x ++ sep ++ concat sep xs + end. + (** *** Test functions *) (** Test if [s1] is a prefix of [s2] *) diff --git a/tools/coqc.ml b/tools/coqc.ml index 3181ef9101..90d8e67c1e 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -111,7 +111,7 @@ let parse_args () = |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" - |"-o"|"-profile-ltac-cutoff" + |"-o"|"-profile-ltac-cutoff"|"-mangle-names" as o) :: rem -> begin match rem with diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 06b2ba41bd..a1a07fce87 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -271,6 +271,11 @@ let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 +let get_identifier opt s = + try Names.Id.of_string s + with CErrors.UserError _ -> + prerr_endline ("Error: valid identifier expected after option "^opt); exit 1 + let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true | _ -> false @@ -466,6 +471,9 @@ let parse_args arglist : coq_cmdopts * string list = |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular oval true (next ()) + |"-mangle-names" -> + Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval + |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 1da46e8ce6..a103cfe7f3 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -341,6 +341,22 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () +let pr_open_cur_subgoals () = + try + let proof = Proof_global.give_me_the_proof () in + Printer.pr_open_subgoals ~proof + with Proof_global.NoCurrentProof -> Pp.str "" + +(* Goal equality heuristic. *) +let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2 +let evleq e1 e2 = CList.equal Evar.equal e1 e2 +let cproof p1 p2 = + let (a1,a2,a3,a4,_),(b1,b2,b3,b4,_) = Proof.proof p1, Proof.proof p2 in + evleq a1 b1 && + CList.equal (pequal evleq evleq) a2 b2 && + CList.equal Evar.equal a3 b3 && + CList.equal Evar.equal a4 b4 + let drop_last_doc = ref None let rec loop ~time ~state = @@ -351,6 +367,10 @@ let rec loop ~time ~state = (* Be careful to keep this loop tail-recursive *) let rec vernac_loop ~state = let nstate = do_vernac ~time ~state in + let proof_changed = not (Option.equal cproof nstate.proof state.proof) in + let print_goals = not !Flags.quiet && + proof_changed && Proof_global.there_are_pending_proofs () in + if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); loop_flush_all (); vernac_loop ~state:nstate (* We recover the current stateid, threading from the caller is diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 07553a2abd..504ffa521b 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -79,6 +79,7 @@ let print_usage_channel co command = \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ +\n -mangle-names x mangle auto-generated names using prefix x\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7c889500ab..56bdcc7e52 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -70,12 +70,6 @@ let print_cmd_header ?loc com = Pp.pp_with !Topfmt.std_ft (pp_cmd_header ?loc com); Format.pp_print_flush !Topfmt.std_ft () -let pr_open_cur_subgoals () = - try - let proof = Proof_global.give_me_the_proof () in - Printer.pr_open_subgoals ~proof - with Proof_global.NoCurrentProof -> Pp.str "" - (* Reenable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) @@ -94,23 +88,8 @@ end let interp_vernac ~time ~check ~interactive ~state (loc,com) = let open State in try - (* XXX: We need to run this before add as the classification is - highly dynamic and depends on the structure of the - document. Hopefully this is fixed when VtMeta can be removed - and Undo etc... are just interpreted regularly. *) - - (* XXX: The classifier can emit warnings so we need to guard - against that... *) - let wflags = CWarnings.get_flags () in - CWarnings.set_flags "none"; - let is_proof_step = match fst (Vernac_classifier.classify_vernac com) with - | VtProofStep _ | VtMeta | VtStartProof _ -> true - | _ -> false - in - CWarnings.set_flags wflags; - - (* The -time option is only supported from console-based - clients due to the way it prints. *) + (* The -time option is only supported from console-based clients + due to the way it prints. *) if time then print_cmd_header ?loc com; let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in @@ -123,14 +102,6 @@ let interp_vernac ~time ~check ~interactive ~state (loc,com) = it otherwise reveals bugs *) (* Stm.observe nsid; *) let ndoc = if check then Stm.finish ~doc else doc in - - (* We could use a more refined criteria that depends on the - vernac. For now we imitate the old approach and rely on the - classification. *) - let print_goals = interactive && not !Flags.quiet && - is_proof_step && Proof_global.there_are_pending_proofs () in - - if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); let new_proof = Proof_global.give_me_the_proof_opt () in { doc = ndoc; sid = nsid; proof = new_proof } with reraise -> diff --git a/vernac/classes.ml b/vernac/classes.ml index 25d893bfbd..192cc8a555 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -374,16 +374,34 @@ let context poly l = with e when CErrors.noncritical e -> user_err Pp.(str "Anonymous variables not allowed in contexts.") in - let uctx = ref (Evd.universe_context_set sigma) in + let univs = + let uctx = Evd.universe_context_set sigma in + match ctx with + | [] -> assert false + | [_] -> + if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) + else Monomorphic_const_entry uctx + | _::_::_ -> + if Lib.sections_are_opened () + then + begin + Declare.declare_universe_context poly uctx; + if poly then Polymorphic_const_entry Univ.UContext.empty + else Monomorphic_const_entry Univ.ContextSet.empty + end + else if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) + else + begin + Declare.declare_universe_context poly uctx; + Monomorphic_const_entry Univ.ContextSet.empty + end + in let fn status (id, b, t) = let b, t = Option.map (to_constr sigma) b, to_constr sigma t in if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) - else Monomorphic_const_entry !uctx - in - let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> (ParameterEntry (None,(t,univs),None), IsAssumption Logical) @@ -405,10 +423,6 @@ let context poly l = in let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) - else Monomorphic_const_entry !uctx - in let nstatus = match b with | None -> pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl @@ -422,6 +436,4 @@ let context poly l = in status && nstatus in - if Lib.sections_are_opened () then - Declare.declare_universe_context poly !uctx; List.fold_left fn true (List.rev ctx) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index f235de3509..56e3243766 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -19,7 +19,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool + Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) (** Internal API *) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 0d6367291c..6f81c4575f 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -17,7 +17,7 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition : program_mode:bool -> - Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> + Id.t -> definition_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit @@ -27,6 +27,6 @@ val do_definition : program_mode:bool -> (** Not used anywhere. *) val interp_definition : - Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> + universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Univdecls.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index edfe7aa819..a794c2db06 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -14,7 +14,6 @@ open Pretyping open Evarutil open Evarconv open Misctypes -open Vernacexpr module RelDecl = Context.Rel.Declaration diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index b181984e07..36c2993afe 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -32,7 +32,7 @@ val do_cofixpoint : type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : Vernacexpr.universe_decl_expr option; + fix_univs : Constrexpr.universe_decl_expr option; fix_annot : Misctypes.lident option; fix_binders : local_binder_expr list; fix_body : constr_expr option; diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 457a1da054..c59286d1a3 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -57,7 +57,7 @@ let push_types env idl tl = type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index b8d85c8d93..8339357246 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -47,7 +47,7 @@ val declare_mutual_inductive_with_eliminations : type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 26c6a8cbee..5eae4fd7f0 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -805,7 +805,14 @@ let vernac_end_segment ({v=id} as lid) = (* Libraries *) +let warn_require_in_section = + let name = "require-in-section" in + let category = "deprecated" in + CWarnings.create ~name ~category + (fun () -> strbrk "Use of “Require” inside a section is deprecated.") + let vernac_require from import qidl = + if Lib.sections_are_opened () then warn_require_in_section (); let qidl = List.map qualid_of_reference qidl in let root = match from with | None -> None |