diff options
107 files changed, 400 insertions, 489 deletions
diff --git a/checker/check.ml b/checker/check.ml index 9a750858d..3e22c4b18 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -321,7 +321,7 @@ let intern_from_file (dir, f) = System.marshal_in_segment f ch in (* Verification of the final checksum *) let () = close_in ch in - let ch = open_in f in + let ch = open_in_bin f in if not (String.equal (Digest.channel ch pos) checksum) then errorlabstrm "intern_from_file" (str "Checksum mismatch"); let () = close_in ch in diff --git a/configure.ml b/configure.ml index 4e2e34641..9fa40b0df 100644 --- a/configure.ml +++ b/configure.ml @@ -236,7 +236,6 @@ module Prefs = struct let usecamlp5 = ref true let camlp5dir = ref (None : string option) let arch = ref (None : string option) - let opt = ref false let natdynlink = ref true let coqide = ref (None : ide option) let macintegration = ref true @@ -283,7 +282,7 @@ let args_options = Arg.align [ "-emacs", Arg.String (fun s -> printf "Warning: obsolete -emacs option\n"; Prefs.emacslib := Some s), - "<dir> (Obsolete) same as -emacslib"; + "<dir> Obsolete: same as -emacslib"; "-coqdocdir", arg_string_option Prefs.coqdocdir, "<dir> Where to install Coqdoc style files"; "-camldir", arg_string_option Prefs.camldir, @@ -299,8 +298,8 @@ let args_options = Arg.align [ "<dir> Specifies where is the Camlp5 library and tells to use it"; "-arch", arg_string_option Prefs.arch, "<arch> Specifies the architecture"; - "-opt", Arg.Set Prefs.opt, - " Use OCaml *.opt optimized compilers"; + "-opt", Arg.Unit (fun () -> printf "Warning: obsolete -opt option\n"), + " Obsolete: native OCaml executables detected automatically"; "-natdynlink", arg_bool Prefs.natdynlink, "(yes|no) Use dynamic loading of native code or not"; "-coqide", Arg.String (fun s -> Prefs.coqide := Some (get_ide s)), @@ -361,8 +360,8 @@ type camlexec = (* TODO: autodetect .opt binaries ? *) let camlexec = - { byte = if !Prefs.opt then "ocamlc.opt" else "ocamlc"; - opt = if !Prefs.opt then "ocamlopt.opt" else "ocamlopt"; + { byte = "ocamlc"; + opt = "ocamlopt"; top = "ocaml"; mklib = "ocamlmklib"; dep = "ocamldep"; @@ -371,6 +370,12 @@ let camlexec = yacc = "ocamlyacc"; p4 = "camlp4o" } +let reset_caml_byte c o = c.byte <- o +let reset_caml_opt c o = c.opt <- o +let reset_caml_doc c o = c.doc <- o +let reset_caml_lex c o = c.lex <- o +let reset_caml_dep c o = c.dep <- o + let rebase_camlexec dir c = c.byte <- Filename.concat dir c.byte; c.opt <- Filename.concat dir c.opt; @@ -464,7 +469,8 @@ let browser = (** * OCaml programs *) -let camlbin, camlc = match !Prefs.camldir with +let camlbin, caml_version, camllib = + let camlbin, camlc = match !Prefs.camldir with | Some dir -> rebase_camlexec dir camlexec; Filename.dirname camlexec.byte, camlexec.byte @@ -473,13 +479,21 @@ let camlbin, camlc = match !Prefs.camldir with with Not_found -> die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.byte ^ "Please adjust your path or use the -camldir option of ./configure") + in + let camlcopt = camlc ^ ".opt" in + let camlc = + if is_executable camlcopt then begin + reset_caml_byte camlexec (camlexec.byte ^ ".opt"); + camlcopt + end + else if is_executable camlc then + camlc + else + die ("Error: cannot find the executable '"^camlc^"'.") in + let caml_version, _ = run camlc ["-version"] in + let camllib, _ = run camlc ["-where"] in + camlbin, caml_version, camllib -let _ = - if not (is_executable camlc) then - die ("Error: cannot find the executable '"^camlc^"'.") - -let caml_version, _ = run camlc ["-version"] -let camllib, _ = run camlc ["-where"] let camlp4compat = "-loc loc" (** Caml version as a list of string, e.g. ["4";"00";"1"] *) @@ -619,7 +633,10 @@ let msg_no_dynlink_cmxa () = let check_native () = if !Prefs.byteonly then raise Not_found; - if not (is_executable camlexec.opt || program_in_path camlexec.opt) then + let camloptopt = camlexec.opt ^ ".opt" in + if (is_executable camloptopt || program_in_path camloptopt) then + reset_caml_opt camlexec camloptopt + else if not (is_executable camlexec.opt || program_in_path camlexec.opt) then (msg_no_ocamlopt (); raise Not_found); if not (Sys.file_exists (fullcamlp4lib/camlp4mod^".cmxa")) then (msg_no_camlp4_cmxa (); raise Not_found); @@ -634,6 +651,20 @@ let check_native () = let best_compiler = try check_native (); "opt" with Not_found -> "byte" +let _ = + let camllexopt = camlexec.lex ^ ".opt" in + if is_executable camllexopt || program_in_path camllexopt then + reset_caml_lex camlexec camllexopt + +let _ = + let camldepopt = camlexec.dep ^ ".opt" in + if is_executable camldepopt || program_in_path camldepopt then + reset_caml_dep camlexec camldepopt + +let _ = + let camldocopt = camlexec.doc ^ ".opt" in + if is_executable camldocopt || program_in_path camldocopt then + reset_caml_doc camlexec camldocopt (** * Native dynlink *) diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi index 90e3fdaa5..5b421e49d 100755 --- a/dev/nsis/coq.nsi +++ b/dev/nsis/coq.nsi @@ -196,14 +196,12 @@ SectionEnd Section "Uninstall" -;; We keep the settings -;; Delete "$INSTDIR\config\coqide-gtk2rc" - RMDir /r "$INSTDIR\bin" RMDir /r "$INSTDIR\dev" RMDir /r "$INSTDIR\etc" RMDir /r "$INSTDIR\lib" RMDir /r "$INSTDIR\share" + RMDir /r "$INSTDIR\ide" Delete "$INSTDIR\man\*.1" RMDir "$INSTDIR\man" diff --git a/dev/top_printers.ml b/dev/top_printers.ml index dea70360a..650897ef7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -22,7 +22,6 @@ open Evd open Goptions open Genarg open Clenv -open Universes let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 3605a716e..1eb40cd36 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1782,14 +1782,14 @@ This is useful for declaring the implicit type of a single variable. Implicit generalization is an automatic elaboration of a statement with free variables into a closed statement where these variables are quantified explicitly. Implicit generalization is done inside binders -starting with a \verb|`| and terms delimited by \verb|`{ }| and -\verb|`( )|, always introducing maximally inserted implicit arguments for +starting with a \texttt{\`{}} and terms delimited by \texttt{\`{}\{ \}} and +\texttt{\`{}( )}, always introducing maximally inserted implicit arguments for the generalized variables. Inside implicit generalization delimiters, free variables in the current context are automatically quantified using a product or a lambda abstraction to generate a closed term. In the following statement for example, the variables \texttt{n} and \texttt{m} are automatically generalized and become explicit -arguments of the lemma as we are using \verb|`( )|: +arguments of the lemma as we are using \texttt{\`{}( )}: \begin{coq_example} Generalizable All Variables. @@ -1834,7 +1834,7 @@ Definition id `(x : A) : A := x. Print id. \end{coq_example} -The generalizing binders \verb|`{ }| and \verb|`( )| work similarly to +The generalizing binders \texttt{\`{}\{ \}} and \texttt{\`{}( )} work similarly to their explicit counterparts, only binding the generalized variables implicitly, as maximally-inserted arguments. In these binders, the binding name for the bound object is optional, whereas the type is diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index ce230a0f7..40e0ecc11 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -308,9 +308,9 @@ statement's conclusion has the form {\tt ({\term} t1 .. tn)}. This command is useful to remind the user of the name of library lemmas. -\begin{coq_example*} +\begin{coq_eval} Reset Initial. -\end{coq_example*} +\end{coq_eval} \begin{coq_example} SearchHead le. diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 11954ed0e..24417bd03 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -120,7 +120,7 @@ is on Figure~\ref{init-notations}. \subsection{Complex notations} -Notations can be made from arbitraly complex symbols. One can for +Notations can be made from arbitrarily complex symbols. One can for instance define prefix notations. \begin{coq_example*} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index dcc2bcc1f..ee40a0d51 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -906,7 +906,7 @@ containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$} variables or hypotheses until the goal is not any more a quantification or an implication; \item introduction over an introduction pattern $p$ introduces the - forthcoming quantified variables or premisse of the goal and applies + forthcoming quantified variables or premise of the goal and applies the introduction pattern $p$ to it. \end{itemize} @@ -1020,13 +1020,13 @@ dependencies. This tactic is the inverse of {\tt intro}. This moves the hypothesis named {\ident$_1$} in the local context after the hypothesis named {\ident$_2$}. The proof term is not changed. -If {\ident$_1$} comes before {\ident$_2$} in the order of dependences, -then all hypotheses between {\ident$_1$} and {\ident$_2$} that -(possibly indirectly) depend on {\ident$_1$} are moved also. +If {\ident$_1$} comes before {\ident$_2$} in the order of dependencies, +then all the hypotheses between {\ident$_1$} and {\ident$_2$} that +(possibly indirectly) depend on {\ident$_1$} are moved too. -If {\ident$_1$} comes after {\ident$_2$} in the order of dependences, -then all hypotheses between {\ident$_1$} and {\ident$_2$} that -(possibly indirectly) occur in {\ident$_1$} are moved also. +If {\ident$_1$} comes after {\ident$_2$} in the order of dependencies, +then all the hypotheses between {\ident$_1$} and {\ident$_2$} that +(possibly indirectly) occur in {\ident$_1$} are moved too. \begin{Variants} @@ -1339,7 +1339,7 @@ in the list of subgoals remaining to prove. \label{generalize} This tactic applies to any goal. It generalizes the conclusion with -respect to one of its subterms. +respect to some term. \Example @@ -1415,7 +1415,7 @@ the number of the existential variable since this number is different in every session. When you are referring to hypotheses which you did not name -explicitely, be aware that Coq may make a different decision on how to +explicitly, be aware that Coq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. @@ -1445,7 +1445,7 @@ a hypothesis or in the body or the type of a local definition. \label{admit} The {\tt admit} tactic ``solves'' the current subgoal by an -axiom. This typically allows temporarily skiping a subgoal so as to +axiom. This typically allows temporarily skipping a subgoal so as to progress further in the rest of the proof. To know if some proof still relies on unproved subgoals, one can use the command {\tt Print Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals @@ -2744,7 +2744,7 @@ the same variants as {\tt rewrite} has. This tactic applies to any goal. It replaces all free occurrences of {\term$_1$} in the current goal with {\term$_2$} and generates the equality {\term$_2$}{\tt =}{\term$_1$} as a subgoal. This equality is -automatically solved if it occurs amongst the assumption, or if its +automatically solved if it occurs among the assumption, or if its symmetric form occurs. It is equivalent to {\tt cut \term$_2$=\term$_1$; [intro H{\sl n}; rewrite <- H{\sl n}; clear H{\sl n}| assumption || symmetry; try assumption]}. @@ -3034,7 +3034,7 @@ computational expressions (i.e. with few dead code). \cite{CompiledStrongReduction}. This algorithm is dramatically more efficient than the algorithm used for the {\tt cbv} tactic, but it cannot be fine-tuned. It is specially interesting for full evaluation of algebraic - objects. This includes the case of reflexion-based tactics. + objects. This includes the case of reflection-based tactics. \item {\tt native\_compute} \tacindex{native\_compute} @@ -4781,7 +4781,7 @@ Reset Initial. This tactic puts the {\num} first goals at the end of the list of goals. If {\num} is negative, it will put the last $\left|\num\right|$ goals at -the begining of the list. +the beginning of the list. \Example \begin{coq_example*} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 48e2df19d..76e4efd60 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -68,7 +68,7 @@ but also at the command {\tt Declare ML Module}. Dependencies of \ocaml\ modules are computed by looking at \verb!open! commands and the dot notation {\em module.value}. However, -this is done approximatively and you are advised to use {\tt ocamldep} +this is done approximately and you are advised to use {\tt ocamldep} instead for the \ocaml\ modules dependencies. See the man page of {\tt coqdep} for more details and options. @@ -103,7 +103,7 @@ invocation While customizing a project file, mind the following requirements: \begin{itemize} \item {\Coq} files must end in \texttt{.v}, {\ocaml} modules in - \texttt{.ml4} if they require camlp preproccessing (and in + \texttt{.ml4} if they require camlp preprocessing (and in \texttt{.ml} otherwise), {\ocaml} module signatures, library description and packing files respectively in \texttt{.mli}, \texttt{.mllib} and \texttt{.mlpack}. diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index dc88a00ea..91d30c073 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -36,7 +36,7 @@ \input{../common/title.tex}% extension .tex pour htmlgen %\input{headers} -\usepackage[linktocpage,colorlinks]{hyperref} +\usepackage[linktocpage,colorlinks,bookmarks=true,bookmarksnumbered=true]{hyperref} % The manual advises to load hyperref package last to be able to redefine % necessary commands. % The above should work for both latex and pdflatex. Even if PDF is produced diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index ac38f1ea5..f4b81a241 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -123,7 +123,7 @@ let annotate phrase = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in Vernac.parse_sentence (pa,None) in - let (_, _, xml) = + let (_, xml) = Richprinter.richpp_vernac ast in xml diff --git a/ide/ideutils.ml b/ide/ideutils.ml index d2305b58c..a86944269 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -175,10 +175,7 @@ let select_file_for_save ~title ?filename () = file_chooser#add_select_button_stock `SAVE `SAVE ; file_chooser#add_filter (filter_coq_files ()); file_chooser#add_filter (filter_all_files ()); - (* this line will be used when a lablgtk >= 2.10.0 is the default - on most distributions: - file_chooser#set_do_overwrite_confirmation true; - *) + file_chooser#set_do_overwrite_confirmation true; file_chooser#set_default_response `SAVE; let dir,filename = match filename with |None -> !last_dir, "" diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 1f3990708..5d21efd95 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -186,11 +186,19 @@ object(self) method undo () = Minilib.log "UNDO"; - self#with_lock_undo self#perform_undo (); + self#with_lock_undo begin fun () -> + buffer#begin_user_action (); + self#perform_undo (); + buffer#end_user_action () + end () method redo () = Minilib.log "REDO"; - self#with_lock_undo self#perform_redo (); + self#with_lock_undo begin fun () -> + buffer#begin_user_action (); + self#perform_redo (); + buffer#end_user_action () + end () method process_begin_user_action () = (* Push a new level of event on history stack *) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index f0377cff9..78b88289e 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -10,12 +10,10 @@ open Loc open Names open Constrexpr open Libnames -open Globnames open Nametab open Genredexpr open Genarg open Pattern -open Decl_kinds open Misctypes open Locus diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index eab36d8b2..8fb6601a9 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -1,4 +1,3 @@ -open Names open Cbytecodes open Cemitcodes open Term diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 3c9692a5c..9ecae2b36 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -10,7 +10,6 @@ machine, Oct 2004 *) (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) -open Names open Term open Cbytecodes open Copcodes diff --git a/kernel/closure.ml b/kernel/closure.ml index f06b13d8d..6824c399e 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -771,24 +771,6 @@ let drop_parameters depth n argstk = (* we know that n < stack_args_size(argstk) (if well-typed term) *) anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") - -let rec get_parameters depth n argstk = - match argstk with - Zapp args::s -> - let q = Array.length args in - if n > q then Array.append args (get_parameters depth (n-q) s) - else if Int.equal n q then [||] - else Array.sub args 0 n - | Zshift(k)::s -> - get_parameters (depth-k) n s - | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) - if Int.equal n 0 then [||] - else raise Not_found (* Trying to eta-expand a partial application..., should do - eta expansion first? *) - | _ -> assert false - (* strip_update_shift_app only produces Zapp and Zshift items *) - - (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 47a82cc6c..ce65af975 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -9,7 +9,6 @@ open Declarations open Mod_subst open Univ -open Context (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 4c2c92ccf..90d9c55f1 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -6,13 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Univ open Term -open Context open Environ -open Entries -open Declarations (** {6 Typing functions (not yet tagged as safe) } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 99d9f52c9..ea575e1e0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -654,7 +654,6 @@ let used_section_variables env inds = keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) -let rel_appvect n m = rel_vect n (List.length m) exception UndefinableExpansion diff --git a/kernel/inductive.ml b/kernel/inductive.ml index bb57ad256..6b4dd536a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -447,13 +447,6 @@ type subterm_spec = let eq_wf_paths = Rtree.equal Declareops.eq_recarg -let pp_recarg = function - | Norec -> Pp.str "Norec" - | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i)) - | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i)) - -let pp_wf_paths = Rtree.pp_tree pp_recarg - let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 | Mrec i1, Mrec i2 diff --git a/kernel/names.ml b/kernel/names.ml index b349ccb00..4ccf5b60a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -571,7 +571,6 @@ let constr_modpath (ind,_) = ind_modpath ind let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) -let ith_constructor_of_pinductive (ind,u) i = ((ind,i),u) let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 1a4a4b54d..ada7ae737 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -12,7 +12,6 @@ open Context open Declarations open Util open Nativevalues -open Primitives open Nativeinstr open Nativelambda open Pre_env diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 6a97edc40..ccf2888b5 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -8,7 +8,6 @@ open Names open Term open Pre_env -open Nativevalues open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index dd47bc06a..605c1225c 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -77,7 +77,10 @@ let call_compiler ml_filename = ::include_dirs @ ["-impl"; ml_filename] in if !Flags.debug then Pp.msg_debug (Pp.str (compiler_name ^ " " ^ (String.concat " " args))); - CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename + try CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename + with Unix.Unix_error (e,_,_) -> + Pp.(msg_warning (str (Unix.error_message e))); + false, link_filename let compile fn code = write_ml_code fn code; diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 914f577e2..0b8662ff0 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -12,7 +12,6 @@ open Environ open Mod_subst open Modops open Nativecode -open Nativelib (** This file implements separate compilation for libraries in the native compiler *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 87cebd62f..0609c8517 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -9,7 +9,6 @@ open Names open Term open Mod_subst -open Int (** This module implements the handling of opaque proof terms. Opauqe proof terms are special since: diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4153b323b..b09367dd9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -28,14 +28,6 @@ open Esubst let left2right = ref false -let conv_key k = - match k with - VarKey id -> - VarKey id - | ConstKey (cst,_) -> - ConstKey cst - | RelKey n -> RelKey n - let rec is_empty_stack = function [] -> true | Zupdate _::s -> is_empty_stack s diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a3441aa3e..b54511e40 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -15,7 +15,6 @@ open Errors open Util open Names -open Univ open Term open Context open Declarations @@ -101,10 +100,6 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) - -let subst_instance_j s j = - { uj_val = Vars.subst_univs_level_constr s j.uj_val; - uj_type = Vars.subst_univs_level_constr s j.uj_type } let infer_declaration env kn dcl = match dcl with diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 696fc3d2d..1b54b1ea1 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -8,7 +8,6 @@ open Names open Term -open Univ open Environ open Declarations open Entries diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 80b15f8ba..29315b0a9 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -42,8 +42,6 @@ let conv_vect fconv vect1 vect2 cu = let infos = ref (create_clos_infos betaiotazeta Environ.empty_env) -let eq_table_key = Names.eq_table_key eq_constant - let rec conv_val env pb k v1 v2 cu = if v1 == v2 then cu else conv_whd env pb k (whd_val v1) (whd_val v2) cu diff --git a/lib/cThread.ml b/lib/cThread.ml index 55bb6fd6d..2d1f10bf3 100644 --- a/lib/cThread.ml +++ b/lib/cThread.ml @@ -22,7 +22,7 @@ let thread_friendly_read_fd fd s ~off ~len = let rec loop () = try Unix.read fd s off len with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN|Unix.EINTR),_,_) -> - while not (safe_wait_timed_read fd 1.0) do Thread.yield () done; + while not (safe_wait_timed_read fd 0.05) do Thread.yield () done; loop () in loop () @@ -43,6 +43,18 @@ let really_read_fd fd s off len = i := !i + r done +let really_read_fd_2_oc fd oc len = + let i = ref 0 in + let size = 4096 in + let s = String.create size in + while !i < len do + let len = len - !i in + let r = thread_friendly_read_fd fd s ~off:0 ~len:(min len size) in + if r = 0 then raise End_of_file; + i := !i + r; + output oc s 0 r; + done + let thread_friendly_really_read ic s ~off ~len = try let fd = Unix.descr_of_in_channel ic in @@ -68,9 +80,26 @@ let thread_friendly_input_value ic = let header = String.create Marshal.header_size in really_read_fd fd header 0 Marshal.header_size; let body_size = Marshal.data_size header 0 in - let msg = String.create (body_size + Marshal.header_size) in - String.blit header 0 msg 0 Marshal.header_size; - really_read_fd fd msg Marshal.header_size body_size; - Marshal.from_string msg 0 - with Unix.Unix_error _ -> raise End_of_file + let desired_size = body_size + Marshal.header_size in + if desired_size <= Sys.max_string_length then begin + let msg = String.create desired_size in + String.blit header 0 msg 0 Marshal.header_size; + really_read_fd fd msg Marshal.header_size body_size; + Marshal.from_string msg 0 + end else begin + (* Workaround for 32 bit systems and data > 16M *) + let name, oc = + Filename.open_temp_file ~mode:[Open_binary] "coq" "marshal" in + try + output oc header 0 Marshal.header_size; + really_read_fd_2_oc fd oc body_size; + close_out oc; + let ic = open_in_bin name in + let data = Marshal.from_channel ic in + close_in ic; + Sys.remove name; + data + with e -> Sys.remove name; raise e + end + with Unix.Unix_error _ | Sys_error _ -> raise End_of_file diff --git a/lib/monad.ml b/lib/monad.ml index 4a52684da..a1714a41b 100644 --- a/lib/monad.ml +++ b/lib/monad.ml @@ -111,7 +111,7 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct | [a] -> M.map (fun a' -> [a']) (f a) | a::b::l -> - map f l >>= fun l' -> + map_right f l >>= fun l' -> f b >>= fun b' -> M.map (fun a' -> a'::b'::l') (f a) @@ -387,8 +387,6 @@ let pp_with ?pp_tag ft strm = let ppnl_with ft strm = pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ()))) -let pp_flush_with ft = Format.pp_print_flush ft - (* pretty printing functions WITH FLUSH *) let msg_with ft strm = pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) diff --git a/lib/richpp.ml b/lib/richpp.ml index 745b7d2a2..c4a9c39d5 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Xml_datatype type 'annotation located = { @@ -14,129 +15,117 @@ type 'annotation located = { endpos : int } +type 'a stack = +| Leaf +| Node of string * 'a located gxml list * int * 'a stack + +type 'a context = { + mutable stack : 'a stack; + (** Pending opened nodes *) + mutable offset : int; + (** Quantity of characters printed so far *) + mutable annotations : 'a option Int.Map.t; + (** Map associating annotations to indexes *) + mutable index : int; + (** Current index of annotations *) +} + +(** We use Format to introduce tags inside the pretty-printed document. + Each inserted tag is a fresh index that we keep in sync with the contents + of annotations. + + We build an XML tree on the fly, by plugging ourselves in Format tag + marking functions. As those functions are called when actually writing to + the device, the resulting tree is correct. +*) let rich_pp annotate ppcmds = - (** First, we use Format to introduce tags inside - the pretty-printed document. - - Each inserted tag is a fresh index that we keep in sync with the contents - of annotations. - *) - let annotations = ref [] in - let index = ref (-1) in + + let context = { + stack = Leaf; + offset = 0; + annotations = Int.Map.empty; + index = (-1); + } in + let pp_tag obj = - let () = incr index in - let () = annotations := obj :: !annotations in - string_of_int !index + let index = context.index + 1 in + let () = context.index <- index in + let obj = annotate obj in + let () = context.annotations <- Int.Map.add index obj context.annotations in + string_of_int index + in + + let pp_buffer = Buffer.create 13 in + + let push_pcdata () = + (** Push the optional PCData on the above node *) + let len = Buffer.length pp_buffer in + if len = 0 then () + else match context.stack with + | Leaf -> assert false + | Node (node, child, pos, ctx) -> + let data = Buffer.contents pp_buffer in + let () = Buffer.clear pp_buffer in + let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in + context.offset <- context.offset + len in - let tagged_pp = Format.( - - (** Warning: The following instructions are valid only if - [str_formatter] is not used for another purpose in - Pp.pp_with. *) - - let ft = str_formatter in - - (** We reuse {!Format} standard way of producing tags - inside pretty-printing. *) - pp_set_tags ft true; - - (** The whole output must be a valid document. To that - end, we nest the document inside a tag named <pp>. *) - pp_open_tag ft "pp"; - - (** XML ignores spaces. The problem is that our pretty-printings - are based on spaces to indent. To solve that problem, we - systematically output non-breakable spaces, which are properly - honored by XML. - - To do so, we reconfigure the [str_formatter] temporarily by - hijacking the function that output spaces. *) - let out, flush, newline, std_spaces = - pp_get_all_formatter_output_functions ft () - in - let set = pp_set_all_formatter_output_functions ft ~out ~flush ~newline in - set ~spaces:(fun k -> - for i = 0 to k - 1 do - Buffer.add_string stdbuf " " - done - ); - - (** Some characters must be escaped in XML. This is done by the - following rewriting of the strings held by pretty-printing - commands. *) - Pp.(pp_with ~pp_tag ft (rewrite Xml_printer.pcdata_to_string ppcmds)); - - (** Insert </pp>. *) - pp_close_tag ft (); - - (** Get the final string. *) - let output = flush_str_formatter () in - - (** Finalize by restoring the state of the [str_formatter] and the - default behavior of Format. By the way, there may be a bug here: - there is no {!Format.pp_get_tags} and therefore if the tags flags - was already set to true before executing this piece of code, the - state of Format is not restored. *) - set ~spaces:std_spaces; - pp_set_tags ft false; - output - ) + let open_xml_tag tag = + let () = push_pcdata () in + context.stack <- Node (tag, [], context.offset, context.stack) in - (** Second, we retrieve the final function that relates - each tag to an annotation. *) - let objs = CArray.rev_of_list !annotations in - let get index = annotate objs.(index) in - - (** Third, we parse the resulting string. It is a valid XML - document (in the sense of Xml_parser). As blanks are - meaningful we deactivate canonicalization in the XML - parser. *) - let xml_pp = - try - Xml_parser.(parse ~do_not_canonicalize:true (make (SString tagged_pp))) - with Xml_parser.Error e -> - Printf.eprintf - "Broken invariant (RichPp): \n\ - The output semi-structured pretty-printing is ill-formed.\n\ - Please report.\n\ - %s" - (Xml_parser.error e); - exit 1 + + let close_xml_tag tag = + let () = push_pcdata () in + match context.stack with + | Leaf -> assert false + | Node (node, child, pos, ctx) -> + let () = assert (String.equal tag node) in + let annotation = + try Int.Map.find (int_of_string node) context.annotations + with _ -> None + in + let annotation = { + annotation = annotation; + startpos = pos; + endpos = context.offset; + } in + let xml = Element (node, annotation, List.rev child) in + match ctx with + | Leaf -> + (** Final node: we keep the result in a dummy context *) + context.stack <- Node ("", [xml], 0, Leaf) + | Node (node, child, pos, ctx) -> + context.stack <- Node (node, xml :: child, pos, ctx) in - (** Fourth, the low-level XML is turned into a high-level - semi-structured document that contains a located annotation in - every node. During the traversal of the low-level XML document, - we build a raw string representation of the pretty-print. *) - let rec node buffer = function - | Element (index, [], cs) -> - let startpos, endpos, cs = children buffer cs in - let annotation = try get (int_of_string index) with _ -> None in - (Element (index, { annotation; startpos; endpos }, cs), endpos) + let open Format in - | PCData s -> - Buffer.add_string buffer s; - (PCData s, Buffer.length buffer) + let ft = formatter_of_buffer pp_buffer in - | _ -> - assert false (* Because of the form of XML produced by Format. *) - - and children buffer cs = - let startpos = Buffer.length buffer in - let cs, endpos = - List.fold_left (fun (cs, endpos) c -> - let c, endpos = node buffer c in - (c :: cs, endpos) - ) ([], startpos) cs - in - (startpos, endpos, List.rev cs) - in - let pp_buffer = Buffer.create 13 in - let xml, _ = node pp_buffer xml_pp in + let tag_functions = { + mark_open_tag = (fun tag -> let () = open_xml_tag tag in ""); + mark_close_tag = (fun tag -> let () = close_xml_tag tag in ""); + print_open_tag = ignore; + print_close_tag = ignore; + } in + + pp_set_formatter_tag_functions ft tag_functions; + pp_set_mark_tags ft true; + + (** The whole output must be a valid document. To that + end, we nest the document inside <pp> tags. *) + pp_open_tag ft "pp"; + Pp.(pp_with ~pp_tag ft ppcmds); + pp_close_tag ft (); + + (** Get the resulting XML tree. *) + let () = pp_print_flush ft () in + let () = assert (Buffer.length pp_buffer = 0) in + match context.stack with + | Node ("", [xml], 0, Leaf) -> xml + | _ -> assert false - (** We return the raw pretty-printing and its annotations tree. *) - (Buffer.contents pp_buffer, xml) let annotations_positions xml = let rec node accu = function diff --git a/lib/richpp.mli b/lib/richpp.mli index 446ee1a04..bf80c8dc8 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -17,13 +17,13 @@ type 'annotation located = { } (** [rich_pp get_annotations ppcmds] returns the interpretation - of [ppcmds] as a string as well as a semi-structured document + of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired annotation. If this function returns [None], then no annotation is put. *) val rich_pp : (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds -> - string * 'annotation located Xml_datatype.gxml + 'annotation located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is diff --git a/lib/terminal.ml b/lib/terminal.ml index 1e6c25578..0f6b23af3 100644 --- a/lib/terminal.ml +++ b/lib/terminal.ml @@ -167,7 +167,8 @@ let reset_style = { negative = Some false; } -let has_style t = Unix.isatty t +let has_style t = + Unix.isatty t && Sys.os_type = "Unix" let split c s = let len = String.length s in diff --git a/library/globnames.ml b/library/globnames.ml index 5eb091af4..3befaa9a9 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Errors open Names open Term diff --git a/library/library.ml b/library/library.ml index b078e2c47..e4169d66e 100644 --- a/library/library.ml +++ b/library/library.ml @@ -172,28 +172,32 @@ let open_libraries export modl = (**********************************************************************) -(* import and export - synchronous operations*) +(* import and export of libraries - synchronous operations *) +(* at the end similar to import and export of modules except that it *) +(* is optimized: when importing several libraries at the same time *) +(* which themselves indirectly imports the very same modules, these *) +(* ones are imported only ones *) -let open_import i (_,(dir,export)) = +let open_import_library i (_,(modl,export)) = if Int.equal i 1 then (* even if the library is already imported, we re-import it *) (* if not (library_is_opened dir) then *) - open_libraries export [try_find_library dir] + open_libraries export (List.map try_find_library modl) -let cache_import obj = - open_import 1 obj +let cache_import_library obj = + open_import_library 1 obj -let subst_import (_,o) = o +let subst_import_library (_,o) = o -let classify_import (_,export as obj) = +let classify_import_library (_,export as obj) = if export then Substitute obj else Dispose -let in_import : DirPath.t * bool -> obj = +let in_import_library : DirPath.t list * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with - cache_function = cache_import; - open_function = open_import; - subst_function = subst_import; - classify_function = classify_import } + cache_function = cache_import_library; + open_function = open_import_library; + subst_function = subst_import_library; + classify_function = classify_import_library } (************************************************************************) @@ -310,7 +314,7 @@ let fetch_table what dp (f,pos,digest) = if not (String.equal (System.digest_in f ch) digest) then raise Faulty; let table, pos', digest' = System.marshal_in_segment f ch in let () = close_in ch in - let ch' = open_in f in + let ch' = open_in_bin f in if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty; let () = close_in ch' in table @@ -402,9 +406,6 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) -let deps_to_string deps = - Array.fold_left (fun s (n, _) -> s^"\n - "^(DirPath.to_string n)) "" deps - let rec intern_library (needed, contents) (dir, f) from = Pp.feedback(Feedback.FileDependency (from, f)); (* Look if in the current logical environment *) @@ -543,7 +544,7 @@ let require_library_from_dirpath modrefl export = begin add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> - List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) + add_anonymous_leaf (in_import_library (modrefl,exp))) export end else @@ -559,7 +560,7 @@ let require_library_from_file idopt file export = let needed = List.rev_map snd needed in if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); - Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) + Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp))) export end else @@ -568,21 +569,30 @@ let require_library_from_file idopt file export = (* the function called by Vernacentries.vernac_import *) -let import_module export (loc,qid) = - try - match Nametab.locate_module qid with - | MPfile dir -> - if Lib.is_module_or_modtype () || not export then - add_anonymous_leaf (in_import (dir, export)) - else - add_anonymous_leaf (in_import (dir, export)) - | mp -> - Declaremods.import_module export mp - with - Not_found -> - user_err_loc - (loc,"import_library", - str ((string_of_qualid qid)^" is not a module")) +let safe_locate_module (loc,qid) = + try Nametab.locate_module qid + with Not_found -> + user_err_loc + (loc,"import_library", str (string_of_qualid qid ^ " is not a module")) + +let import_module export modl = + (* Optimization: libraries in a raw in the list are imported + "globally". If there is non-library in the list; it breaks the + optimization For instance: "Import Arith MyModule Zarith" will + not be optimized (possibly resulting in redefinitions, but + "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule" + will have the submodules imported by both Arith and ZArith + imported only once *) + let flush = function + | [] -> () + | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in + let rec aux acc = function + | m :: l -> + (match safe_locate_module m with + | MPfile dir -> aux (dir::acc) l + | mp -> flush acc; Declaremods.import_module export mp; aux [] l) + | [] -> flush acc + in aux [] modl (************************************************************************) (*s Initializing the compilation of a library. *) diff --git a/library/library.mli b/library/library.mli index 13d83a5c0..77d78207d 100644 --- a/library/library.mli +++ b/library/library.mli @@ -37,7 +37,7 @@ type seg_proofs = Term.constr Future.computation array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) -val import_module : bool -> qualid located -> unit +val import_module : bool -> qualid located list -> unit (** {6 Start the compilation of a library } *) val start_library : string -> DirPath.t * string diff --git a/library/loadpath.ml b/library/loadpath.ml index 5876eedd2..ab8b0a307 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -12,14 +12,13 @@ open Errors open Names open Libnames -type path_type = ImplicitPath | ImplicitRootPath | RootPath - (** Load paths. Mapping from physical to logical paths. *) type t = { path_physical : CUnix.physical_path; path_logical : DirPath.t; - path_type : path_type; + path_root : bool; + path_implicit : bool; } let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" @@ -54,13 +53,14 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths -let add_load_path phys_path path_type coq_path = +let add_load_path phys_path coq_path ~root ~implicit = let phys_path = CUnix.canonical_path_name phys_path in let filter p = String.equal p.path_physical phys_path in let binding = { path_logical = coq_path; path_physical = phys_path; - path_type = path_type; + path_root = root; + path_implicit = implicit; } in match List.filter filter !load_paths with | [] -> @@ -93,7 +93,7 @@ let expand_root_path dir = let rec aux = function | [] -> [] | p :: l -> - if p.path_type <> ImplicitPath && is_dirpath_prefix_of p.path_logical dir then + if p.path_root && is_dirpath_prefix_of p.path_logical dir then let suffix = drop_dirpath_prefix p.path_logical dir in extend_path_with_dirpath p.path_physical suffix :: aux l else aux l @@ -123,13 +123,17 @@ let expand_path dir = let rec aux = function | [] -> [] | p :: l -> - match p.path_type with - | ImplicitPath -> expand p dir :: aux l - | ImplicitRootPath -> + match p.path_implicit, p.path_root with + | true, false -> expand p dir :: aux l + | true, true -> let inters = intersections p.path_logical dir in List.map (expand p) inters @ aux l - | RootPath -> + | false, true -> if is_dirpath_prefix_of p.path_logical dir then expand p (drop_dirpath_prefix p.path_logical dir) :: aux l - else aux l in + else aux l + | false, false -> + (* nothing to do, an explicit root path should also match above + if [is_dirpath_prefix_of p.path_logical dir] were true here *) + aux l in aux !load_paths diff --git a/library/loadpath.mli b/library/loadpath.mli index 62dc5d591..d4029303d 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -15,11 +15,6 @@ open Names *) -type path_type = - | ImplicitPath (** Can be implicitly appended to a logical path. *) - | ImplicitRootPath (** Can be implicitly appended to the suffix of a logical path. *) - | RootPath (** Can only be a prefix of a logical path. *) - type t (** Type of loadpath bindings. *) @@ -35,7 +30,7 @@ val get_load_paths : unit -> t list val get_paths : unit -> CUnix.physical_path list (** Same as [get_load_paths] but only get the physical part. *) -val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit +val add_load_path : CUnix.physical_path -> DirPath.t -> root:bool -> implicit:bool -> unit (** [add_load_path phys type log] adds the binding [phys := log] to the current loadpaths. *) diff --git a/library/universes.mli b/library/universes.mli index f2f68d329..252648d7d 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -7,12 +7,9 @@ (************************************************************************) open Util -open Pp open Names open Term -open Context open Environ -open Locus open Univ (** Universes *) diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 0e0eb6d2a..2ff2bd387 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -7,7 +7,6 @@ (************************************************************************) open Ccalgo -open Names open Term type rule= diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 29ea1e777..6c7b09383 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Context open Globnames diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 8006a3e13..7a56cd665 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -16,7 +16,6 @@ open Term open Tactics open Names open Globnames -open Tacticals open Tacmach open Fourier open Contradiction diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c8214ada8..eb5221fd6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -7,7 +7,6 @@ open Context open Namegen open Names open Declarations -open Declareops open Pp open Tacmach open Proof_type @@ -16,7 +15,6 @@ open Tactics open Indfun_common open Libnames open Globnames -open Misctypes (* let msgnl = Pp.msgnl *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 545f8931f..80167686a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -6,7 +6,6 @@ open Vars open Context open Namegen open Names -open Declareops open Pp open Entries open Tactics diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6dbd61cfd..2730fd421 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -8,7 +8,6 @@ open Libnames open Globnames open Glob_term open Declarations -open Declareops open Misctypes open Decl_kinds diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 53f8b0db8..b6c5d426f 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -12,7 +12,6 @@ open Names open Term open Context open Environ -open Mod_subst (** {5 Existential variables and unification states} diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 7f7f4d764..95a6ba79d 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -11,7 +11,6 @@ open Util open Errors open Names open Locus -open Context open Term open Nameops open Termops diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 82330b846..47d9654e5 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Locus open Context open Term diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 654f914b6..adf714db3 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -18,7 +18,6 @@ open Declarations open Declareops open Environ open Reductionops -open Inductive (* The following three functions are similar to the ones defined in Inductive, but they expect an env *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b4e0459c1..1106fefa3 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -23,7 +23,6 @@ open Reductionops open Cbv open Patternops open Locus -open Pretype_errors (* Errors *) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 5862a8525..9f04faa83 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -15,7 +15,6 @@ open Term open Vars open Context open Environ -open Locus (* Sorts and sort family *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 9f3efd72b..2552c67e6 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -11,7 +11,6 @@ open Names open Term open Context open Environ -open Locus (** printers *) val print_sort : sorts -> std_ppcmds diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 817d68782..b64ccf60d 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -14,7 +14,6 @@ open Term open Vars open Context open Evd -open Environ open Util open Typeclasses_errors open Libobject @@ -427,7 +426,6 @@ let add_class cl = cl.cl_projs -open Declarations (* * interface functions diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 4f88dd860..585f066db 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -10,7 +10,6 @@ open Names open Term open Context -open Evd open Environ open Constrexpr open Globnames diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index dd8087713..7982fc852 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -10,7 +10,6 @@ open Loc open Names open Term open Context -open Evd open Environ open Constrexpr open Globnames diff --git a/pretyping/typing.mli b/pretyping/typing.mli index c933106d7..1f822f1a5 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Environ open Evd diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli index 15413d515..b7eb9b1ff 100644 --- a/printing/ppconstrsig.mli +++ b/printing/ppconstrsig.mli @@ -12,8 +12,6 @@ open Libnames open Constrexpr open Names open Misctypes -open Locus -open Genredexpr module type Pp = sig diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 50cc4e2bc..42b4c976a 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -15,9 +15,6 @@ open Names open Constrexpr open Tacexpr open Ppextend -open Environ -open Pattern -open Misctypes type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index ee1669f7f..1631bda37 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -8,7 +8,6 @@ open Pp open Genarg -open Names open Constrexpr open Tacexpr open Ppextend diff --git a/printing/printer.ml b/printing/printer.ml index 8a2d6e7bd..fb98f6073 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -11,7 +11,6 @@ open Errors open Util open Names open Term -open Vars open Environ open Globnames open Nametab diff --git a/printing/richprinter.ml b/printing/richprinter.ml index d71dc82d5..d95e19074 100644 --- a/printing/richprinter.ml +++ b/printing/richprinter.ml @@ -5,21 +5,20 @@ module RichppVernac = Ppvernac.Richpp module RichppTactic = Pptactic.Richpp type rich_pp = - string - * Ppannotation.t Richpp.located Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml * Xml_datatype.xml let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag let make_richpp pr ast = - let raw_pp, rich_pp = + let rich_pp = rich_pp get_annotations (pr ast) in let xml = Ppannotation.( xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp ) in - (raw_pp, rich_pp, xml) + (rich_pp, xml) let richpp_vernac = make_richpp RichppVernac.pr_vernac let richpp_constr = make_richpp RichppConstr.pr_constr_expr diff --git a/printing/richprinter.mli b/printing/richprinter.mli index c67d52c08..41c313514 100644 --- a/printing/richprinter.mli +++ b/printing/richprinter.mli @@ -20,12 +20,10 @@ (** A rich pretty-print is composed of: *) type rich_pp = - (** - a raw pretty-print ; *) - string (** - a generalized semi-structured document whose attributes are annotations ; *) - * Ppannotation.t Richpp.located Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 9b671bcf0..eb1081706 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -10,7 +10,6 @@ open Names open Term open Environ open Evd -open Mod_subst open Unification open Misctypes diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index da40427c4..ea2043613 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -8,7 +8,6 @@ open Term open Clenv -open Proof_type open Tacexpr open Unification diff --git a/proofs/goal.ml b/proofs/goal.ml index e3570242e..107ce7f8e 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -9,8 +9,6 @@ open Util open Pp open Term -open Vars -open Context (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated diff --git a/proofs/logic.ml b/proofs/logic.ml index 53f8093e5..b8206ca1b 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Environ open Reductionops @@ -83,12 +82,6 @@ let apply_to_hyp sign id f = if !check then error_no_such_hypothesis id else sign -let apply_to_hyp_and_dependent_on sign id f g = - try apply_to_hyp_and_dependent_on sign id f g - with Hyp_not_found -> - if !check then error_no_such_hypothesis id - else sign - let check_typability env sigma c = if !check then let _ = type_of env sigma c in () @@ -277,11 +270,6 @@ let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let rename_hyp id1 id2 sign = - apply_to_hyp_and_dependent_on sign id1 - (fun (_,b,t) _ -> (id2,b,t)) - (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) - (**********************************************************************) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f55ab7007..971729245 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -339,10 +339,13 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context let return_proof () = - let { proof; strength = (_,poly,_) } = cur_pstate () in + let { pid; proof; strength = (_,poly,_) } = cur_pstate () in let initial_goals = Proof.initial_goals proof in let evd = - let error s = raise (Errors.UserError("last tactic before Qed",s)) in + let error s = + let prf = str " (in proof " ++ Id.print pid ++ str ")" in + raise (Errors.UserError("last tactic before Qed",s ++ prf)) + in try Proof.return proof with | Proof.UnfinishedProof -> error(str"Attempt to save an incomplete proof") diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 26bb78dfe..47b2b255e 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -10,7 +10,6 @@ open Evd open Names open Term -open Context open Tacexpr open Glob_term open Nametab diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index e709be5bc..f5e2bad2a 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -9,7 +9,6 @@ open Evd open Names open Term -open Context open Tacexpr open Glob_term open Nametab diff --git a/stm/lemmas.mli b/stm/lemmas.mli index d0669d7a3..a0ddd265c 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -10,7 +10,6 @@ open Names open Term open Decl_kinds open Constrexpr -open Tacexpr open Vernacexpr open Pfedit diff --git a/stm/stm.ml b/stm/stm.ml index 7b2468548..3a57d85ba 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1580,6 +1580,7 @@ let collect_proof keep cur hd brkind id = let view = VCS.visit id in match view.step with | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next + | `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) | `Alias _ -> `Sync (no_name,None,`Alias) | `Fork((_,_,_,_::_::_), _) -> @@ -1863,7 +1864,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 -let merge_proof_branch ?id qast keep brname = +let merge_proof_branch ?valid ?id qast keep brname = let brinfo = VCS.get_branch brname in let qed fproof = { qast; keep; brname; brinfo; fproof } in match brinfo with @@ -1886,7 +1887,7 @@ let merge_proof_branch ?id qast keep brname = VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> - iraise (State.exn_on Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) + iraise (State.exn_on ?valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) @@ -2044,7 +2045,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = VCS.commit id (Cmd {cast = x; cids = []; cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> - let rc = merge_proof_branch ~id:newtip x keep head in + let valid = if tty then Some(VCS.get_branch_pos head) else None in + let rc = merge_proof_branch ?valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); rc diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index d71c169d6..a0979f8b1 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -15,7 +15,6 @@ open Bigint open Decl_kinds open Extend open Libnames -open Flags let unlock loc = let start, stop = Loc.unloc loc in diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 84df3ecd5..b20722211 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -119,7 +119,7 @@ let schedule_vio_compilation j fs = let rec filter_argv b = function | [] -> [] | "-schedule-vio2vo" :: rest -> filter_argv true rest - | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest) + | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest) | _ :: rest when b -> filter_argv b rest | s :: rest -> s :: filter_argv b rest in let prog = Sys.argv.(0) in diff --git a/tactics/auto.mli b/tactics/auto.mli index ea3f0ac0d..0cc8a0b1b 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -8,7 +8,6 @@ open Names open Term -open Proof_type open Clenv open Pattern open Evd diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1c15fa40b..e97a42e6e 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -17,7 +17,6 @@ open Proof_type open Tacticals open Tacmach open Tactics -open Patternops open Clenv open Typeclasses open Globnames @@ -42,7 +41,7 @@ let get_typeclasses_dependency_order () = !typeclasses_dependency_order open Goptions -let set_typeclasses_modulo_eta = +let _ = declare_bool_option { optsync = true; optdepr = false; @@ -51,7 +50,7 @@ let set_typeclasses_modulo_eta = optread = get_typeclasses_modulo_eta; optwrite = set_typeclasses_modulo_eta; } -let set_typeclasses_dependency_order = +let _ = declare_bool_option { optsync = true; optdepr = false; diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 9ee14b801..9b69481da 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -9,8 +9,6 @@ open Errors open Term open Hipattern -open Tacmach -open Tacticals open Tactics open Coqlib open Reductionops diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 5c039e72c..6d3dc461e 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -71,14 +71,14 @@ END TACTIC EXTEND left_with [ "left" "with" bindings(bl) ] -> [ let { Evd.sigma = sigma ; it = bl } = bl in - Proofview.Unsafe.tclEVARS sigma <*> Tactics.left_with_bindings false bl + Tacticals.New.tclWITHHOLES false (Tactics.left_with_bindings false bl) sigma ] END TACTIC EXTEND eleft_with [ "eleft" "with" bindings(bl) ] -> [ let { Evd.sigma = sigma ; it = bl } = bl in - Tacticals.New.tclWITHHOLES true (Tactics.left_with_bindings true) sigma bl + Tacticals.New.tclWITHHOLES true (Tactics.left_with_bindings true bl) sigma ] END @@ -95,14 +95,14 @@ END TACTIC EXTEND right_with [ "right" "with" bindings(bl) ] -> [ let { Evd.sigma = sigma ; it = bl } = bl in - Proofview.Unsafe.tclEVARS sigma <*> Tactics.right_with_bindings false bl + Tacticals.New.tclWITHHOLES false (Tactics.right_with_bindings false bl) sigma ] END TACTIC EXTEND eright_with [ "eright" "with" bindings(bl) ] -> [ let { Evd.sigma = sigma ; it = bl } = bl in - Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true) sigma bl + Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true bl) sigma ] END @@ -117,8 +117,8 @@ TACTIC EXTEND constructor | [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [ let { Evd.sigma = sigma; it = bl } = bl in let i = Tacinterp.interp_int_or_var ist i in - let tac c = Tactics.constructor_tac false None i c in - Proofview.Unsafe.tclEVARS sigma <*> tac bl + let tac = Tactics.constructor_tac false None i bl in + Tacticals.New.tclWITHHOLES false tac sigma ] END @@ -131,8 +131,8 @@ TACTIC EXTEND econstructor | [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [ let { Evd.sigma = sigma; it = bl } = bl in let i = Tacinterp.interp_int_or_var ist i in - let tac c = Tactics.constructor_tac true None i c in - Tacticals.New.tclWITHHOLES true tac sigma bl + let tac = Tactics.constructor_tac true None i bl in + Tacticals.New.tclWITHHOLES true tac sigma ] END @@ -141,8 +141,8 @@ END TACTIC EXTEND specialize [ "specialize" constr_with_bindings(c) ] -> [ let { Evd.sigma = sigma; it = c } = c in - let specialize c = Proofview.V82.tactic (Tactics.specialize c) in - Proofview.Unsafe.tclEVARS sigma <*> specialize c + let specialize = Proofview.V82.tactic (Tactics.specialize c) in + Tacticals.New.tclWITHHOLES false specialize sigma ] END @@ -163,14 +163,14 @@ END TACTIC EXTEND split_with [ "split" "with" bindings(bl) ] -> [ let { Evd.sigma = sigma ; it = bl } = bl in - Proofview.Unsafe.tclEVARS sigma <*> Tactics.split_with_bindings false [bl] + Tacticals.New.tclWITHHOLES false (Tactics.split_with_bindings false [bl]) sigma ] END TACTIC EXTEND esplit_with [ "esplit" "with" bindings(bl) ] -> [ let { Evd.sigma = sigma ; it = bl } = bl in - Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true) sigma [bl] + Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true [bl]) sigma ] END diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 19e2f198b..7073e8a2b 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -8,7 +8,6 @@ open Term open Proof_type -open Auto open Evd open Hints diff --git a/tactics/elim.ml b/tactics/elim.ml index b7d5b1028..3cb4fa9c4 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -15,7 +15,6 @@ open Hipattern open Tacmach.New open Tacticals.New open Tactics -open Misctypes open Proofview.Notations let introElimAssumsThen tac ba = diff --git a/tactics/equality.ml b/tactics/equality.ml index c130fa151..838f8865d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -487,9 +487,6 @@ let apply_special_clear_request clear_flag f = e when catchable_exception e -> tclIDTAC end -type delayed_open_constr_with_bindings = - env -> evar_map -> evar_map * constr with_bindings - let general_multi_rewrite with_evars l cl tac = let do1 l2r f = Proofview.Goal.enter begin fun gl -> @@ -497,7 +494,7 @@ let general_multi_rewrite with_evars l cl tac = let env = Proofview.Goal.env gl in let sigma,c = f env sigma in tclWITHHOLES with_evars - (general_rewrite_clause l2r with_evars ?tac c) sigma cl + (general_rewrite_clause l2r with_evars ?tac c cl) sigma end in let rec doN l2r c = function @@ -1474,8 +1471,6 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* then it uses the predicate "\x.phi(proj1_sig x,proj2_sig x)", and so *) (* on for further iterated sigma-tuples *) -exception NothingToRewrite - let cutSubstInConcl l2r eqn = Proofview.Goal.nf_enter begin fun gl -> let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in @@ -1513,9 +1508,6 @@ let try_rewrite tac = | e when catchable_exception e -> tclZEROMSG (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.") - | NothingToRewrite -> - tclZEROMSG - (strbrk "Nothing to rewrite.") | e -> Proofview.tclZERO ~info e end diff --git a/tactics/equality.mli b/tactics/equality.mli index 90d8a224b..3e13ee570 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -11,7 +11,6 @@ open Names open Term open Evd open Environ -open Tacmach open Tacexpr open Ind_tables open Locus diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 42d00e1e1..2c4df0608 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Tacmach open Names open Tacexpr open Locus diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f3482c310..1ffc0519f 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -21,7 +21,6 @@ open Util open Evd open Equality open Misctypes -open Proofview.Notations DECLARE PLUGIN "extratactics" @@ -33,14 +32,15 @@ TACTIC EXTEND admit [ "admit" ] -> [ admit_as_an_axiom ] END -let replace_in_clause_maybe_by (sigma,c1) c2 cl tac = - Proofview.Unsafe.tclEVARS sigma <*> - (replace_in_clause_maybe_by c1 c2 cl) - (Option.map Tacinterp.eval_tactic tac) +let replace_in_clause_maybe_by (sigma1,c1) c2 cl tac = + Tacticals.New.tclWITHHOLES false + (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac)) + sigma1 let replace_term dir_opt (sigma,c) cl = - Proofview.Unsafe.tclEVARS sigma <*> - (replace_term dir_opt c) cl + Tacticals.New.tclWITHHOLES false + (replace_term dir_opt c cl) + sigma TACTIC EXTEND replace ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] @@ -71,8 +71,8 @@ let induction_arg_of_quantified_hyp = function ElimOnIdent and not as "constr" *) let elimOnConstrWithHoles tac with_evars c = - Tacticals.New.tclWITHHOLES with_evars (tac with_evars) - c.sigma (Some (None,ElimOnConstr c.it)) + Tacticals.New.tclWITHHOLES with_evars + (tac with_evars (Some (None,ElimOnConstr c.it))) c.sigma TACTIC EXTEND simplify_eq_main | [ "simplify_eq" constr_with_bindings(c) ] -> @@ -202,7 +202,7 @@ END let onSomeWithHoles tac = function | None -> tac None - | Some c -> Proofview.Unsafe.tclEVARS c.sigma <*> tac (Some c.it) + | Some c -> Tacticals.New.tclWITHHOLES false (tac (Some c.it)) c.sigma TACTIC EXTEND contradiction [ "contradiction" constr_with_bindings_opt(c) ] -> @@ -246,8 +246,8 @@ END let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) = let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in - Proofview.Unsafe.tclEVARS sigma <*> - general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true + Tacticals.New.tclWITHHOLES false + (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) sigma TACTIC EXTEND rewrite_star | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index c200871ef..27d25056e 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -8,7 +8,6 @@ open Names open Term -open Evd open Coqlib (** High-order patterns *) @@ -145,8 +144,6 @@ val is_matching_sigma : constr -> bool val match_eqdec : constr -> bool * constr * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -open Proof_type -open Tacmach val dest_nf_eq : [ `NF ] Proofview.Goal.t -> constr -> (constr * constr * constr) (** Match a negation *) diff --git a/tactics/inv.mli b/tactics/inv.mli index b3478dda2..412f30c20 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Term open Misctypes diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 47a4de444..2f80d26fc 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Term open Constrexpr diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 1bffa9f60..53f3f5652 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -73,7 +73,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = (* Summary and Object declaration *) open Nametab -open Libnames open Libobject let mactab = @@ -86,7 +85,6 @@ let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab) (* Declaration of the TAC-DEFINITION object *) let add (kn,td) = mactab := KNmap.add kn td !mactab -let replace (kn,td) = mactab := KNmap.add kn td !mactab let load_md i ((sp, kn), (local, id, b, t)) = match id with | None -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b1ff0e401..3b497faab 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -497,8 +497,6 @@ let interp_fresh_id ist env sigma l = Id.of_string s in Tactics.fresh_id_in_env avoid id env - - (* Extract the uconstr list from lfun *) let extract_ltac_constr_context ist env = let open Glob_term in @@ -1785,12 +1783,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacIntroPattern l) (* spiwack: print uninterpreted, not sure if it is the expected behaviour. *) - (Tactics.intros_patterns l') + (Tactics.intros_patterns l')) sigma end | TacIntroMove (ido,hto) -> Proofview.Goal.enter begin fun gl -> @@ -1824,11 +1822,11 @@ and interp_atomic ist tac : unit Proofview.tactic = (k,(loc,f))) cb in let sigma,tac = match cl with - | None -> sigma, fun l -> Tactics.apply_with_delayed_bindings_gen a ev l + | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l | Some cl -> let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in - sigma, fun l -> Tactics.apply_delayed_in a ev clear id l cl in - Tacticals.New.tclWITHHOLES ev tac sigma l + sigma, Tactics.apply_delayed_in a ev clear id l cl in + Tacticals.New.tclWITHHOLES ev tac sigma end end | TacElim (ev,(keep,cb),cbo) -> @@ -1837,22 +1835,22 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = Proofview.Goal.sigma gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in - let named_tac cbo = + let named_tac = let tac = Tactics.elim ev keep cb cbo in name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac in - Tacticals.New.tclWITHHOLES ev named_tac sigma cbo + Tacticals.New.tclWITHHOLES ev named_tac sigma end | TacCase (ev,(keep,cb)) -> Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in - let named_tac cb = + let named_tac = let tac = Tactics.general_case_analysis ev keep cb in name_atomic ~env (TacCase(ev,(keep,cb))) tac in - Tacticals.New.tclWITHHOLES ev named_tac sigma cb + Tacticals.New.tclWITHHOLES ev named_tac sigma end | TacFix (idopt,n) -> Proofview.Goal.enter begin fun gl -> @@ -1915,20 +1913,20 @@ and interp_atomic ist tac : unit Proofview.tactic = in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in let tac = Option.map (interp_tactic ist) t in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacAssert(b,t,ipat,c)) - (Tactics.forward b tac ipat' c) + (Tactics.forward b tac ipat' c)) sigma end | TacGeneralize cl -> Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacGeneralize cl) - (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl)) + (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma end | TacGeneralizeDep c -> (new_interp_constr ist c) (fun c -> @@ -1953,11 +1951,11 @@ and interp_atomic ist tac : unit Proofview.tactic = let with_eq = if b then None else Some (true,id) in Tactics.letin_tac with_eq na c None cl in - Proofview.Unsafe.tclEVARS sigma <*> let na = interp_fresh_name ist env sigma na in - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacLetTac(na,c_interp,clp,b,eqpat)) - (let_tac b na c_interp clp eqpat) + (let_tac b na c_interp clp eqpat)) sigma else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = @@ -1970,7 +1968,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacLetTac(na,c,clp,b,eqpat)) (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_fresh_name ist env sigma na) - ((sigma,sigma'),c) clp) sigma' eqpat) + ((sigma,sigma'),c) clp eqpat) sigma') end (* Automation tactics *) @@ -2080,11 +2078,11 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in - let named_tac bll = + let named_tac = let tac = Tactics.split_with_bindings ev bll in name_atomic ~env (TacSplit (ev, bll)) tac in - Tacticals.New.tclWITHHOLES ev named_tac sigma bll + Tacticals.New.tclWITHHOLES ev named_tac sigma end (* Conversion *) | TacReduce (r,cl) -> @@ -2184,10 +2182,10 @@ and interp_atomic ist tac : unit Proofview.tactic = in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma,ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacInversion(DepInversion(k,c_interp,ids),dqhyps)) - (Inv.dinv k c_interp ids_interp dqhyps) + (Inv.dinv k c_interp ids_interp dqhyps)) sigma end | TacInversion (NonDepInversion (k,idl,ids),hyp) -> Proofview.Goal.enter begin fun gl -> @@ -2196,10 +2194,10 @@ and interp_atomic ist tac : unit Proofview.tactic = let hyps = interp_hyp_list ist env sigma idl in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacInversion (NonDepInversion (k,hyps,ids),dqhyps)) - (Inv.inv_clause k ids_interp hyps dqhyps) + (Inv.inv_clause k ids_interp hyps dqhyps)) sigma end | TacInversion (InversionUsing (c,idl),hyp) -> Proofview.Goal.enter begin fun gl -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 59cd065d1..42e61cb57 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -100,20 +100,11 @@ let subst_evaluable subst = let subst_eval_ref = subst_evaluable_reference subst in subst_or_var (subst_and_short_name subst_eval_ref) -let subst_unfold subst (l,e) = - (l,subst_evaluable subst e) - -let subst_flag subst red = - { red with rConst = List.map (subst_evaluable subst) red.rConst } - let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) let subst_glob_constr_or_pattern subst (c,p) = (subst_glob_constr subst c,subst_pattern subst p) -let subst_pattern_with_occurrences subst (l,p) = - (l,subst_glob_constr_or_pattern subst p) - let subst_redexp subst = Miscops.map_red_expr_gen (subst_glob_constr subst) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index cf2126f8d..9b16fe3f7 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -16,7 +16,6 @@ open Context open Declarations open Tacmach open Clenv -open Misctypes (************************************************************************) (* Tacticals re-exported from the Refiner module *) @@ -494,26 +493,23 @@ module New = struct let (loc,_) = evi.Evd.evar_source in Pretype_errors.error_unsolvable_implicit loc env sigma evk None - let tclWITHHOLES accept_unresolved_holes tac sigma x = + let tclWITHHOLES accept_unresolved_holes tac sigma = tclEVARMAP >>= fun sigma_initial -> - if sigma == sigma_initial then tac x + if sigma == sigma_initial then tac else - let check_evars env new_sigma sigma initial_sigma = - try - check_evars env new_sigma sigma initial_sigma; - tclUNIT () - with e when Errors.noncritical e -> - tclZERO e - in - let check_evars_if = + let check_evars_if x = if not accept_unresolved_holes then tclEVARMAP >>= fun sigma_final -> tclENV >>= fun env -> - check_evars env sigma_final sigma sigma_initial + try + let () = check_evars env sigma_final sigma sigma_initial in + tclUNIT x + with e when Errors.noncritical e -> + tclZERO e else - tclUNIT () + tclUNIT x in - Proofview.Unsafe.tclEVARS sigma <*> tac x <*> check_evars_if + Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if let tclTIMEOUT n t = Proofview.tclOR diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 6249bbc59..4e860892d 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,14 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Pp open Names open Term open Context open Tacmach open Proof_type -open Clenv open Tacexpr open Locus open Misctypes @@ -220,7 +218,7 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic + val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 07969c7d7..a96ae2688 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -765,8 +765,6 @@ let intro = intro_gen (NamingAvoid []) MoveLast false false let introf = intro_gen (NamingAvoid []) MoveLast true false let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false -let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false - let intro_move_avoid idopt avoid hto = match idopt with | None -> intro_gen (NamingAvoid avoid) hto true false | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false @@ -1503,7 +1501,7 @@ let apply_with_delayed_bindings_gen b e l = let env = Proofview.Goal.env gl in let sigma, cb = f env sigma in Tacticals.New.tclWITHHOLES e - (general_apply b b e k) sigma (loc,cb) + (general_apply b b e k (loc,cb)) sigma end in let rec aux = function @@ -1606,8 +1604,8 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam let sigma, c = f env sigma in Tacticals.New.tclWITHHOLES with_evars (apply_in_once sidecond_first with_delta with_destruct with_evars - naming id (clear_flag,(loc,c))) - sigma tac + naming id (clear_flag,(loc,c)) tac) + sigma end (* A useful resolution tactic which, if c:A->B, transforms |- C into @@ -2136,12 +2134,12 @@ and intro_pattern_action loc b style pat thin tac id = match pat with let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma,c = f env sigma in - Proofview.Unsafe.tclEVARS sigma <*> + Tacticals.New.tclWITHHOLES false (Tacticals.New.tclTHENFIRST (* Skip the side conditions of the apply *) (apply_in_once false true true true naming id - (None,(sigma,(c,NoBindings))) tac_ipat)) - (tac thin None []) + (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None [])) + sigma end and prepare_intros_loc loc dft = function @@ -2790,12 +2788,6 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = atomize_one (List.length argl) [] [] end -let find_atomic_param_of_ind nparams indtyp = - let argl = snd (decompose_app indtyp) in - let params,args = List.chop nparams argl in - let test c = isVar c && not (List.exists (dependent c) params) in - List.map destVar (List.filter test args) - (* [cook_sign] builds the lists [beforetoclear] (preceding the ind. var.) and [aftertoclear] (coming after the ind. var.) of hyps that must be erased, the lists of hyps to be generalize [decldeps] on the diff --git a/test-suite/bugs/closed/4012.v b/test-suite/bugs/closed/4012.v new file mode 100644 index 000000000..1748e3baa --- /dev/null +++ b/test-suite/bugs/closed/4012.v @@ -0,0 +1,5 @@ +Goal (forall T : Type, T = T) -> Type. +Proof. + intro H. + Fail specialize (H _). +Abort. diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 383a68df8..a2cc8384c 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -79,7 +79,7 @@ let expos = Str.regexp "^" let tex_escaped s = let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in - let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>']") in + let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in let adapt_delim = function | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c | "\\" -> "{\\char'134}" @@ -89,6 +89,7 @@ let tex_escaped s = | "<" -> "{<}" | ">" -> "{>}" | "'" -> "{\\textquotesingle}" + | "`" -> "\\`{}" | _ -> assert false in let adapt = function diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 5dbd5379a..807872988 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Names open Ind_tables diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 22ea09c53..2df7c2273 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Pp open Errors open Indtypes diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 0a351d3cc..cb88ae564 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -8,7 +8,6 @@ open Names open Context -open Evd open Environ open Constrexpr open Typeclasses diff --git a/toplevel/command.mli b/toplevel/command.mli index 1de47d38c..3a38e52ce 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -11,7 +11,6 @@ open Term open Entries open Libnames open Globnames -open Tacexpr open Vernacexpr open Constrexpr open Decl_kinds diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 142f33867..0b9bb2f2e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -378,7 +378,7 @@ let schedule_vio_compilation () = let get_native_name s = (* We ignore even critical errors because this mode has to be super silent *) try - String.concat Filename.dir_sep [Filename.dirname s; + String.concat "/" [Filename.dirname s; Nativelib.output_dir; Library.native_name_from_filename s] with _ -> "" diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 968f72486..b3de3a7c7 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -68,16 +68,24 @@ type tactic_grammar_obj = { tacobj_body : Tacexpr.glob_tactic_expr } -let cache_tactic_notation ((_, key), tobj) = +let key k tobj = + let mp,dp,_ = KerName.repr k in + KerName.make mp dp + (Label.make ("_" ^ string_of_int (Hashtbl.hash tobj.tacobj_tacgram))) + +let cache_tactic_notation ((_,k), tobj) = + let key = key k tobj in Tacenv.register_alias key tobj.tacobj_body; Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp -let open_tactic_notation i ((_, key), tobj) = +let open_tactic_notation i ((_,k), tobj) = + let key = key k tobj in if Int.equal i 1 && not tobj.tacobj_local then Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram -let load_tactic_notation i ((_, key), tobj) = +let load_tactic_notation i ((_,k), tobj) = + let key = key k tobj in (** Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp; diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 9dc1dd5b1..357c5482f 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -165,9 +165,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath ~implicit = if exists_dir dir then begin add_ml_dir dir; - Loadpath.add_load_path dir - (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath) - coq_dirpath + Loadpath.add_load_path dir ~root:true ~implicit coq_dirpath end else msg_warning (str ("Cannot open " ^ dir)) @@ -191,11 +189,9 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let dirs = List.map_filter convert_dirs dirs in let () = add_ml_dir unix_path in let add (path, dir) = - Loadpath.add_load_path path Loadpath.ImplicitPath dir in - let () = if implicit then List.iter add dirs in - Loadpath.add_load_path unix_path - (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath) - coq_root + Loadpath.add_load_path path ~root:false ~implicit dir in + let () = List.iter add dirs in + Loadpath.add_load_path unix_path ~root:true ~implicit coq_root else msg_warning (str ("Cannot open " ^ unix_path)) diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index d39e18a48..40f124ca3 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -14,7 +14,6 @@ open Pp open Globnames open Vernacexpr open Decl_kinds -open Tacexpr (** Forward declaration. *) val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c6e40725b..7f435ce96 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -598,11 +598,8 @@ let vernac_constraint l = do_constraint l (* Modules *) let vernac_import export refl = - let import ref = - Library.import_module export (qualid_of_reference ref) - in - List.iter import refl; - Lib.add_frozen_state () + Library.import_module export (List.map qualid_of_reference refl); + Lib.add_frozen_state () let vernac_declare_module export (loc, id) binders_ast mty_ast = (* We check the state of the system (in section, in module type) |