diff options
159 files changed, 1343 insertions, 1343 deletions
diff --git a/.travis.yml b/.travis.yml index adaae5487..aa2e0e63c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -37,6 +37,7 @@ env: - TEST_TARGET="ci-fiat-crypto" - TEST_TARGET="ci-fiat-parsers" - TEST_TARGET="ci-flocq" + - TEST_TARGET="ci-formal-topology" - TEST_TARGET="ci-hott" - TEST_TARGET="ci-iris-coq" - TEST_TARGET="ci-math-classes" @@ -53,7 +54,6 @@ matrix: allow_failures: - env: TEST_TARGET="ci-geocoq" - - env: TEST_TARGET="ci-vst" # Full Coq test-suite with two compilers # [TODO: use yaml refs and avoid duplication for packages list] @@ -66,7 +66,7 @@ matrix: apt: sources: - avsm - packages: + packages: &extra-packages - opam - aspcud - libgtk2.0-dev @@ -83,7 +83,7 @@ matrix: - imagemagick - env: - TEST_TARGET="test-suite" - - COMPILER="4.04.0" + - COMPILER="4.04.1" - CAMLP5_VER="6.17" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="lablgtk-extras hevea" @@ -91,21 +91,35 @@ matrix: apt: sources: - avsm - packages: + packages: *extra-packages + - env: + - TEST_TARGET="coqocaml" + - EXTRA_CONF="-coqide opt -warn-error" + - EXTRA_OPAM="lablgtk-extras hevea" + # dummy target + - BUILD_TARGET="clean" + addons: + apt: + sources: + - avsm + packages: &coqide-packages - opam - aspcud - libgtk2.0-dev - libgtksourceview2.0-dev - - texlive-latex-base - - texlive-latex-recommended - - texlive-latex-extra - - texlive-math-extra - - texlive-fonts-recommended - - texlive-fonts-extra - - latex-xcolor - - ghostscript - - transfig - - imagemagick + - env: + - TEST_TARGET="coqocaml" + - COMPILER="4.04.1" + - CAMLP5_VER="6.17" + - EXTRA_CONF="-coqide opt -warn-error" + - EXTRA_OPAM="lablgtk-extras hevea" + # dummy target + - BUILD_TARGET="clean" + addons: + apt: + sources: + - avsm + packages: *coqide-packages install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y @@ -116,6 +130,7 @@ install: script: +- set -e - echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r' - ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF} - echo -en 'travis_fold:end:coq.config\\r' @@ -127,6 +142,7 @@ script: - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r' - ${TW} make -j ${NJOBS} ${TEST_TARGET} - echo -en 'travis_fold:end:coq.test\\r' +- set +e # Testing Gitter webhook notifications: @@ -17,7 +17,17 @@ Tactics Most notably, the new implementation recognizes Miller patterns that were missed before because of a missing normalization step. Hopefully this should be fairly uncommon. -- "auto with real" can now discharge comparisons of literals +- Tactic "auto with real" can now discharge comparisons of literals. +- The types of variables in patterns of "match" are now + beta-iota-reduced after type-checking. This has an impact on the + type of the variables that the tactic "refine" introduces in the + context, producing types a priori closer to the expectations. + +Vernacular Commands + +- Goals context can be printed in a more compact way when "Set + Printing Compact Contexts" is activated. + Standard Library diff --git a/Makefile.ci b/Makefile.ci index 4c4606aff..013685218 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,7 +1,7 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \ ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \ - ci-unimath ci-vst ci-bedrock-src ci-bedrock-facade + ci-unimath ci-vst ci-bedrock-src ci-bedrock-facade ci-formal-topology .PHONY: $(CI_TARGETS) diff --git a/Makefile.dev b/Makefile.dev index 5931e46dd..1803cc8ff 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -97,7 +97,10 @@ minibyte: $(COQTOPBYTE) pluginsbyte pluginsopt: $(PLUGINSOPT) pluginsbyte: $(PLUGINS) -.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte +# This should build all the ocaml code but not (most of) the .v files +coqocaml: tools coqbinaries pluginsopt coqide printers + +.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml ########################## ### 2) core ML components diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e0851816c..1dfade261 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -98,13 +98,19 @@ # bedrock_src ######################################################################## : ${bedrock_src_CI_BRANCH:=master} -: ${bedrock_src_CI_GITURL:=https://github.com/JasonGross/bedrock.git} +: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git} ######################################################################## # bedrock_facade ######################################################################## : ${bedrock_facade_CI_BRANCH:=master} -: ${bedrock_facade_CI_GITURL:=https://github.com/JasonGross/bedrock.git} +: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git} + +######################################################################## +# formal-topology +######################################################################## +: ${formal_topology_CI_BRANCH:=ci} +: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git} ######################################################################## # CoLoR diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh new file mode 100755 index 000000000..ecb36349f --- /dev/null +++ b/dev/ci/ci-formal-topology.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes + +Corn_CI_DIR=${CI_BUILD_DIR}/corn + +formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology + +# Setup Math-Classes + +git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} + +( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install ) + +# Setup Corn + +git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} + +( cd ${Corn_CI_DIR} && make -j ${NJOBS} && make install ) + +# Setup formal-topology + +git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR} + +( cd ${formal_topology_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 7caaf2d9d..ce6d5dff0 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -7,7 +7,6 @@ (************************************************************************) (* Printers for the ocaml toplevel. *) -[@@@ocaml.warning "-32"] open Util open Pp @@ -60,14 +59,6 @@ let pprecarg = function str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) -let pprecarg = function - | Declarations.Norec -> str "Norec" - | Declarations.Mrec (mind,i) -> - str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" - | Declarations.Imbr (mind,i) -> - str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" -let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) - (* term printers *) let rawdebug = ref false let ppevar evk = pp (str (Evd.string_of_existential evk)) @@ -458,8 +449,6 @@ let print_pure_constr csr = print_string (Printexc.to_string e);print_flush (); raise e -let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) - let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" @@ -521,7 +510,7 @@ let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; GramNonTerminal - (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)] let _ = try @@ -537,7 +526,7 @@ let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; GramNonTerminal - (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)] (* Setting printer of unbound global reference *) open Names diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 9378529cb..0346c4a55 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1087,8 +1087,8 @@ Fail all:let n:= numgoals in guard n=2. Reset Initial. \end{coq_eval} -\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed exporting} -\index{Tacticals!abstract@{\tt abstract}}} +\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract}\comindex{Qed exporting} +\index{Tacticals!abstract@{\tt abstract}}\index{Tacticals!transparent\_abstract@{\tt transparent\_abstract}}} From the outside ``\texttt{abstract \tacexpr}'' is the same as {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called @@ -1114,13 +1114,24 @@ on. This can be obtained thanks to the option below. {\tt Set Shrink Abstract} \end{quote} -When set, all lemmas generated through \texttt{abstract {\tacexpr}} are -quantified only over the variables that appear in the term constructed by -\texttt{\tacexpr}. +When set, 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. + Use this feature at your own risk; explicitly named and reused subterms + don't play well with asynchronous proofs. +\item \texttt{transparent\_abstract {\tacexpr}}.\\ + Save the subproof in a transparent lemma rather than an opaque one. + Use this feature at your own risk; building computationally relevant terms + with tactics is fragile. +\item \texttt{transparent\_abstract {\tacexpr} using {\ident}}.\\ + Give explicitly the name of the auxiliary transparent lemma. + Use this feature at your own risk; building computationally relevant terms + with tactics is fragile, and explicitly named and reused subterms + don't play well with asynchronous proofs. \end{Variants} \ErrMsg \errindex{Proof is not complete} @@ -1231,7 +1242,7 @@ This will automatically print the same trace as {\tt Info \num} at each tactic c The current value for the {\tt Info Level} option can be checked using the {\tt Test Info Level} command. -\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}} +\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}\optindex{Ltac Batch Debug}} The {\ltac} interpreter comes with a step-by-step debugger. The debugger can be activated using the command @@ -1262,6 +1273,17 @@ r $n$: & advance $n$ steps further\\ r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\ \end{tabular} +A non-interactive mode for the debugger is available via the command + +\begin{quote} +{\tt Set Ltac Batch Debug.} +\end{quote} + +This option has the effect of presenting a newline at every prompt, +when the debugger is on. The debug log thus created, which does not +require user input to generate when this option is set, can then be +run through external tools such as \texttt{diff}. + \subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}} It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 56ce753cd..3daaac88b 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -697,8 +697,8 @@ which can be any valid path. \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}} -This command is equivalent to the command line option {\tt -Q {\dirpath} - {\str}}. It adds the physical directory {\str} to the current {\Coq} +This command is equivalent to the command line option {\tt -Q {\str} + {\dirpath}}. It adds the physical directory {\str} to the current {\Coq} loadpath and maps it to the logical directory {\dirpath}. \begin{Variants} @@ -707,8 +707,8 @@ Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory \end{Variants} \subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}} -This command is equivalent to the command line option {\tt -R {\dirpath} - {\str}}. It adds the physical directory {\str} and all its +This command is equivalent to the command line option {\tt -R {\str} + {\dirpath}}. It adds the physical directory {\str} and all its subdirectories to the current {\Coq} loadpath. \begin{Variants} @@ -960,6 +960,22 @@ time of writing this documentation, the default value is 50). \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}} This command displays the current nesting depth used for display. +\subsection[\tt Unset Printing Compact Contexts.]{\tt Unset Printing Compact Contexts.\optindex{Printing Compact Contexts}} +This command resets the displaying of goals contexts to non compact +mode (default at the time of writing this documentation). Non compact +means that consecutive variables of different types are printed on +different lines. + +\subsection[\tt Set Printing Compact Contexts.]{\tt Set Printing Compact Contexts.\optindex{Printing Compact Contexts}} +This command sets the displaying of goals contexts to compact mode. +The printer tries to reduce the vertical size of goals contexts by +putting several variables (even if of different types) on the same +line provided it does not exceed the printing width (See {\tt Set + Printing Width} above). + +\subsection[\tt Test Printing Compact Contexts.]{\tt Test Printing Compact Contexts.\optindex{Printing Compact Contexts}} +This command displays the current state of compaction of goal d'isolat. + \subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}} This command enables the printing of the ``{\tt (dependent evars: \ldots)}'' line when {\tt -emacs} is passed. diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 6d54b4de1..8ba28b32f 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -118,7 +118,7 @@ the current proof and declare the initial goal as an axiom. \subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof} \label{BeginProof}} This command applies in proof editing mode. It is equivalent to {\tt - exact {\term}; Save.} That is, you have to give the full proof in + exact {\term}. Qed.} That is, you have to give the full proof in one gulp, as a proof term (see Section~\ref{exact}). \variant {\tt Proof.} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 0edc66f83..87b9e4914 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1275,15 +1275,18 @@ in the list of subgoals remaining to prove. \item{\tt assert ( {\ident} := {\term} )} - This behaves as {\tt assert ({\ident} :\ {\type});[exact - {\term}|idtac]} where {\type} is the type of {\term}. This is - deprecated in favor of {\tt pose proof}. + This behaves as {\tt assert ({\ident} :\ {\type}) by exact {\term}} + where {\type} is the type of {\term}. This is deprecated in favor of + {\tt pose proof}. + + If the head of {\term} is {\ident}, the tactic behaves as + {\tt specialize \term}. \ErrMsg \errindex{Variable {\ident} is already declared} -\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}} +\item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}} - This tactic behaves like \texttt{assert T as {\intropattern} by + This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by exact {\term}} where \texttt{T} is the type of {\term}. In particular, \texttt{pose proof {\term} as {\ident}} behaves as @@ -1326,8 +1329,8 @@ in the list of subgoals remaining to prove. following subgoals: {\tt U -> T} and \texttt{U}. The subgoal {\tt U -> T} comes first in the list of remaining subgoal to prove. -\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize}} \\ - {\tt specialize {\ident} with \bindinglist} +\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize} \zeroone{as \intropattern}}\\ + {\tt specialize {\ident} with {\bindinglist} \zeroone{as \intropattern}} The tactic {\tt specialize} works on local hypothesis \ident. The premises of this hypothesis (either universal @@ -1338,14 +1341,19 @@ in the list of subgoals remaining to prove. second form, all instantiation elements must be given, whereas in the first form the application to \term$_1$ {\ldots} \term$_n$ can be partial. The first form is equivalent to - {\tt assert (\ident' := {\ident} {\term$_1$} \dots\ \term$_n$); - clear \ident; rename \ident' into \ident}. + {\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}. + + With the {\tt as} clause, the local hypothesis {\ident} is left + unchanged and instead, the modified hypothesis is introduced as + specified by the {\intropattern}. The name {\ident} can also refer to a global lemma or hypothesis. In this case, for compatibility reasons, the behavior of {\tt specialize} is close to that of {\tt generalize}: the instantiated statement becomes an additional - premise of the goal. + premise of the goal. The {\tt as} clause is especially useful + in this case to immediately introduce the instantiated statement + as a local hypothesis. \begin{ErrMsgs} \item \errindexbis{{\ident} is used in hypothesis \ident'}{is used in hypothesis} diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index d00ee4e5d..5cfcc6fd2 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -40,7 +40,8 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> + | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >> + | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> | ExtTerminal _ :: tl -> <:expr< (fun _ -> $make tl$) >> in make (List.rev pil) @@ -63,7 +64,7 @@ let is_ident x = function | _ -> false let make_extend loc s cl wit = match cl with -| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act -> +| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act -> (** Special handling of identity arguments by not redeclaring an entry *) <:str_item< value $lid:s$ = @@ -246,10 +247,13 @@ EXTEND genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) + | e = LIDENT -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, None) | s = STRING -> ExtTerminal s ] ] ; diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 5b3eb3202..0b3def058 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -23,7 +23,7 @@ type user_symbol = type extend_token = | ExtTerminal of string -| ExtNonTerminal of user_symbol * string +| ExtNonTerminal of user_symbol * string option val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 8b930cf36..87262e1c8 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -25,7 +25,7 @@ type user_symbol = type extend_token = | ExtTerminal of string -| ExtNonTerminal of user_symbol * string +| ExtNonTerminal of user_symbol * string option let mlexpr_of_list f l = List.fold_right diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index b14fba975..3057ee58c 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -31,19 +31,19 @@ let mlexpr_of_ident id = let rec make_patt = function | [] -> <:patt< [] >> - | ExtNonTerminal (_, p) :: l -> + | ExtNonTerminal (_, Some p) :: l -> <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | ExtNonTerminal (g, p) :: l -> + | ExtNonTerminal (g, Some p) :: l -> let t = type_of_user_symbol g in let loc = MLast.loc_of_expr e in let e = make_let raw e l in let v = if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >> - else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in + else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let raw e l @@ -75,7 +75,7 @@ let rec mlexpr_of_symbol = function let make_prod_item = function | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> | ExtNonTerminal (g, id) -> - <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >> + <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_option mlexpr_of_ident id$ >> let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl @@ -87,7 +87,7 @@ let is_constr_gram = function | _ -> false let make_var = function - | ExtNonTerminal (_, p) -> Some p + | ExtNonTerminal (_, p) -> p | _ -> assert false let declare_tactic loc tacname ~level classification clause = match clause with @@ -158,10 +158,13 @@ EXTEND tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) + | e = LIDENT -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, None) | s = STRING -> let () = if s = "" then failwith "Empty terminal." in ExtTerminal s diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 436a7f0d9..7c99b52e8 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -27,7 +27,7 @@ type rule = { let rec make_let e = function | [] -> e - | ExtNonTerminal (g, p) :: l -> + | ExtNonTerminal (g, Some p) :: l -> let t = type_of_user_symbol g in let loc = MLast.loc_of_expr e in let e = make_let e l in @@ -42,7 +42,7 @@ let make_clause { r_patt = pt; r_branch = e; } = (* To avoid warnings *) let mk_ignore c pt = let fold accu = function - | ExtNonTerminal (_, p) -> p :: accu + | ExtNonTerminal (_, Some p) -> p :: accu | _ -> accu in let names = List.fold_left fold [] pt in @@ -101,10 +101,11 @@ let make_fun_classifiers loc s c l = let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> - | ExtNonTerminal (g, id) -> + | ExtNonTerminal (g, ido) -> let nt = type_of_user_symbol g in let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in - <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ + let typ = match ido with None -> None | Some _ -> Some nt in + <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_option (make_rawwit loc) typ$ $mlexpr_of_prod_entry_key base g$ >> let mlexpr_of_clause cl = @@ -178,10 +179,13 @@ EXTEND args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) + | e = LIDENT -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, None) | s = STRING -> ExtTerminal s ] ] diff --git a/ide/coq.ml b/ide/coq.ml index 3a1d87787..cd45e2fcd 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -519,6 +519,7 @@ struct let all_basic = ["Printing"; "All"] let existential = ["Printing"; "Existential"; "Instances"] let universes = ["Printing"; "Universes"] + let unfocused = ["Printing"; "Unfocused"] type bool_descr = { opts : t list; init : bool; label : string } @@ -534,7 +535,8 @@ struct label = "Display _existential variable instances" }; { opts = [universes]; init = false; label = "Display _universe levels" }; { opts = [all_basic;existential;universes]; init = false; - label = "Display all _low-level contents" } + label = "Display all _low-level contents" }; + { opts = [unfocused]; init = false; label = "Display _unfocused goals" } ] (** The current status of the boolean options *) @@ -549,6 +551,8 @@ struct let _ = reset () + let printing_unfocused () = Hashtbl.find current_state unfocused + (** Transmitting options to coqtop *) let enforce h k = diff --git a/ide/coq.mli b/ide/coq.mli index ab8c12a6f..e8e2f5239 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -140,6 +140,8 @@ sig val set : t -> bool -> unit + val printing_unfocused: unit -> bool + (** [enforce] transmits to coq the current option values. It is also called by [goals] and [evars] above. *) diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 91c281c8d..717c4000f 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -85,6 +85,7 @@ let init () = \n <menuitem action='Display existential variable instances' />\ \n <menuitem action='Display universe levels' />\ \n <menuitem action='Display all low-level contents' />\ +\n <menuitem action='Display unfocused goals' />\ \n </menu>\ \n <menu action='Navigation'>\ \n <menuitem action='Forward' />\ diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 966a94da9..56ada9d13 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -54,7 +54,8 @@ let coqide_known_option table = List.mem table [ ["Printing";"All"]; ["Printing";"Records"]; ["Printing";"Existential";"Instances"]; - ["Printing";"Universes"]] + ["Printing";"Universes"]; + ["Printing";"Unfocused"]] let is_known_option cmd = match cmd with | VernacSetOption (o,BoolValue true) diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index f801091cf..0bf5afbfd 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -47,7 +47,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb = hover_cb start stop; false | _ -> false)) -let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with +let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = match goals with | [] -> assert false | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: rem_goals -> let on_hover sel_start sel_stop = @@ -65,8 +65,11 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with let head_str = Printf.sprintf "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "") in - let goal_str index total = Printf.sprintf - "______________________________________(%d/%d)\n" index total + let goal_str ?(shownum=false) index total = + if shownum then Printf.sprintf + "______________________________________(%d/%d)\n" index total + else Printf.sprintf + "______________________________________\n" in (* Insert current goal and its hypotheses *) let hyps_hints, goal_hints = match hints with @@ -97,18 +100,29 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with [tag] else [] in - proof#buffer#insert (goal_str 1 goals_cnt); + proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt); insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) - let fold_goal i _ { Interface.goal_ccl = g } = - proof#buffer#insert (goal_str i goals_cnt); + let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g } = + proof#buffer#insert (goal_str ~shownum i goals_cnt); insert_xml proof#buffer (Richpp.richpp_of_pp width g); proof#buffer#insert "\n" in - let () = Util.List.fold_left_i fold_goal 2 () rem_goals in - + let () = Util.List.fold_left_i (fold_goal ~shownum:true) 2 () rem_goals in + (* show unfocused goal if option set *) + (* Insert remaining goals (no hypotheses) *) + if Coq.PrintOpt.printing_unfocused () then + begin + ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter)); + let unfoc = List.flatten (List.rev (List.map (fun (x,y) -> x@y) unfoc_goals)) in + if unfoc<>[] then + begin + proof#buffer#insert "\nUnfocused Goals:\n"; + Util.List.fold_left_i (fold_goal ~shownum:false) 0 () unfoc + end + end; ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter#backward_to_tag_toggle (Some Tags.Proof.goal))); @@ -172,8 +186,9 @@ let display mode (view : #GText.view_skel) goals hints evars = in List.iteri iter bg end - | Some { Interface.fg_goals = fg } -> - mode view fg hints + | Some { Interface.fg_goals = fg; bg_goals = bg } -> + mode view fg ~unfoc_goals:bg hints + let proof_view () = let buffer = GSourceView2.source_buffer diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index a592b4cff..542f9feaf 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -263,12 +263,6 @@ let cases_pattern_expr_loc = function | CPatDelimiters (loc,_,_) -> loc | CPatCast(loc,_,_) -> loc -let raw_cases_pattern_expr_loc = function - | RCPatAlias (loc,_,_) -> loc - | RCPatCstr (loc,_,_,_) -> loc - | RCPatAtom (loc,_) -> loc - | RCPatOr (loc,_) -> loc - let local_binder_loc = function | CLocalAssum ((loc,_)::_,_,t) | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index f6d97e107..b547288e3 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -36,7 +36,6 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool val constr_loc : constr_expr -> Loc.t val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t -val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t val local_binders_loc : local_binder_expr list -> Loc.t (** {6 Constructors}*) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index df7568c7a..ab1b27eec 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -431,31 +431,6 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b -let rec free_vars_of_pat il = - function - | CPatCstr (loc, c, l1, l2) -> - let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in - List.fold_left free_vars_of_pat il l2 - | CPatAtom (loc, ro) -> - begin match ro with - | Some (Ident (loc, i)) -> (loc, i) :: il - | Some _ | None -> il - end - | CPatNotation (loc, n, l1, l2) -> - let il = List.fold_left free_vars_of_pat il (fst l1) in - List.fold_left (List.fold_left free_vars_of_pat) il (snd l1) - | _ -> anomaly (str "free_vars_of_pat") - -let intern_local_pattern intern lvar env p = - List.fold_left - (fun env (loc, i) -> - let bk = Default Implicit in - let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in - let n = Name i in - let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in - env) - env (free_vars_of_pat [] p) - let glob_local_binder_of_extended = function | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t) | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t) @@ -483,13 +458,15 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio | Some ty -> ty | None -> CHole(loc,None,Misctypes.IntroAnonymous,None) in - let env = intern_local_pattern intern lvar env p in - let il = List.map snd (free_vars_of_pat [] p) in - let cp = + let il,cp = match !intern_cases_pattern_fwd (None,env.scopes) p with - | (_, [(_, cp)]) -> cp + | (il, [(subst,cp)]) -> + if not (Id.Map.equal Id.equal subst Id.Map.empty) then + user_err ~loc (str "Unsupported nested \"as\" clause."); + il,cp | _ -> assert false in + let env = {env with ids = List.fold_right Id.Set.add il env.ids} in let ienv = Id.Set.elements env.ids in let id = Namegen.next_ident_away (Id.of_string "pat") ienv in let na = (loc, Name id) in @@ -901,7 +878,22 @@ let interp_reference vars r = (**********************************************************************) (** {5 Cases } *) -(** {6 Elemtary bricks } *) +(** Private internalization patterns *) +type raw_cases_pattern_expr = + | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t + | RCPatCstr of Loc.t * Globnames.global_reference + * raw_cases_pattern_expr list * raw_cases_pattern_expr list + (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) + | RCPatAtom of Loc.t * Id.t option + | RCPatOr of Loc.t * raw_cases_pattern_expr list + +let raw_cases_pattern_expr_loc = function + | RCPatAlias (loc,_,_) -> loc + | RCPatCstr (loc,_,_,_) -> loc + | RCPatAtom (loc,_) -> loc + | RCPatOr (loc,_) -> loc + +(** {6 Elementary bricks } *) let apply_scope_env env = function | [] -> {env with tmp_scope = None}, [] | sc::scl -> {env with tmp_scope = sc}, scl @@ -931,17 +923,6 @@ let find_remaining_scopes pl1 pl2 ref = in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs), simple_adjust_scopes len_pl2 (aux (impl_list,scope_list))) -let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 - -let product_of_cases_patterns ids idspl = - List.fold_right (fun (ids,pl) (ids',ptaill) -> - (ids @ ids', - (* Cartesian prod of the or-pats for the nth arg and the tail args *) - List.flatten ( - List.map (fun (subst,p) -> - List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) - idspl (ids,[Id.Map.empty,[]]) - (* @return the first variable that occurs twice in a pattern naive n^2 algo *) @@ -1195,12 +1176,23 @@ let alias_of als = match als.alias_ids with *) +let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 + +let product_of_cases_patterns aliases idspl = + List.fold_right (fun (ids,pl) (ids',ptaill) -> + (ids @ ids', + (* Cartesian prod of the or-pats for the nth arg and the tail args *) + List.flatten ( + List.map (fun (subst,p) -> + List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) + idspl (aliases.alias_ids,[aliases.alias_map,[]]) + let rec subst_pat_iterator y t p = match p with | RCPatAtom (_,id) -> begin match id with Some x when Id.equal x y -> t | _ -> p end | RCPatCstr (loc,id,l1,l2) -> - RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1, - List.map (subst_pat_iterator y t) l2) + RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1, + List.map (subst_pat_iterator y t) l2) | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a) | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl) @@ -1217,6 +1209,14 @@ let drop_notations_pattern looked_for = let test_kind top = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found in + (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) + let rec rcp_of_glob = function + | GVar (loc,id) -> RCPatAtom (loc,Some id) + | GHole (loc,_,_,_) -> RCPatAtom (loc,None) + | GRef (loc,g,_) -> RCPatCstr (loc, g,[],[]) + | GApp (loc,GRef (_,g,_),l) -> RCPatCstr (loc, g, List.map rcp_of_glob l,[]) + | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr ") + in let rec drop_syndef top scopes re pats = let (loc,qid) = qualid_of_reference re in try @@ -1286,8 +1286,9 @@ let drop_notations_pattern looked_for = let (argscs1,_) = find_remaining_scopes expl_pl pl g in RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[]) - when Bigint.is_strictly_pos p -> - fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes) + when Bigint.is_strictly_pos p -> + let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in + rcp_of_glob pat | CPatNotation (_,"( _ )",([a],[]),[]) -> in_pat top scopes a | CPatNotation (loc, ntn, fullargs,extrargs) -> @@ -1300,7 +1301,9 @@ let drop_notations_pattern looked_for = in_not top loc scopes (subst,substlist) extrargs c | CPatDelimiters (loc, key, e) -> in_pat top (None,find_delimiters_scope loc key::snd scopes) e - | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes) + | CPatPrim (loc,p) -> + let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes in + rcp_of_glob pat | CPatAtom (loc, Some id) -> begin match drop_syndef top scopes id [] with @@ -1310,8 +1313,21 @@ let drop_notations_pattern looked_for = | CPatAtom (loc,None) -> RCPatAtom (loc,None) | CPatOr (loc, pl) -> RCPatOr (loc,List.map (in_pat top scopes) pl) - | CPatCast _ -> - assert false + | CPatCast (loc,_,_) -> + (* We raise an error if the pattern contains a cast, due to + current restrictions on casts in patterns. Cast in patterns + are supportted only in local binders and only at top + level. In fact, they are currently eliminated by the + parser. The only reason why they are in the + [cases_pattern_expr] type is that the parser needs to factor + the "(c : t)" notation with user defined notations (such as + the pair). In the long term, we will try to support such + casts everywhere, and use them to print the domains of + lambdas in the encoding of match in constr. This check is + here and not in the parser because it would require + duplicating the levels of the [pattern] rule. *) + CErrors.user_err ~loc ~hdr:"drop_notations_pattern" + (Pp.strbrk "Casts are not supported in this pattern.") and in_pat_sc scopes x = in_pat false (x,snd scopes) and in_not top loc scopes (subst,substlist as fullsubst) args = function | NVar id -> @@ -1359,7 +1375,7 @@ let drop_notations_pattern looked_for = let rec intern_pat genv aliases pat = let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 = let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in - let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in + let (ids',pll) = product_of_cases_patterns aliases (idslpl1@idslpl2) in let pl' = List.map (fun (asubst,pl) -> (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in @@ -1393,40 +1409,7 @@ let rec intern_pat genv aliases pat = check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten pl') -(* [check_no_patcast p] raises an error if [p] contains a cast. This code is a - bit ad-hoc, and is due to current restrictions on casts in patterns. We - support them only in local binders and only at top level. In fact, they are - currently eliminated by the parser. The only reason why they are in the - [cases_pattern_expr] type is that the parser needs to factor the "(c : t)" - notation with user defined notations (such as the pair). In the long term, we - will try to support such casts everywhere, and use them to print the domains - of lambdas in the encoding of match in constr. We put this check here and not - in the parser because it would require to duplicate the levels of the - [pattern] rule. *) -let rec check_no_patcast = function - | CPatCast (loc,_,_) -> - CErrors.user_err ~loc ~hdr:"check_no_patcast" - (Pp.strbrk "Casts are not supported here.") - | CPatDelimiters(_,_,p) - | CPatAlias(_,p,_) -> check_no_patcast p - | CPatCstr(_,_,opl,pl) -> - Option.iter (List.iter check_no_patcast) opl; - List.iter check_no_patcast pl - | CPatOr(_,pl) -> - List.iter check_no_patcast pl - | CPatNotation(_,_,subst,pl) -> - check_no_patcast_subst subst; - List.iter check_no_patcast pl - | CPatRecord(_,prl) -> - List.iter (fun (_,p) -> check_no_patcast p) prl - | CPatAtom _ | CPatPrim _ -> () - -and check_no_patcast_subst (pl,pll) = - List.iter check_no_patcast pl; - List.iter (List.iter check_no_patcast) pll - let intern_cases_pattern genv scopes aliases pat = - check_no_patcast pat; intern_pat genv aliases (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat) @@ -1435,7 +1418,6 @@ let _ = fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p let intern_ind_pattern genv scopes pat = - check_no_patcast pat; let no_not = try drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat @@ -1449,7 +1431,7 @@ let intern_ind_pattern genv scopes pat = let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in (with_letin, - match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with + match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type ~loc) | x -> error_bad_inductive_type ~loc:(raw_cases_pattern_expr_loc x) @@ -1775,7 +1757,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = and intern_multiple_pattern env n (loc,pl) = let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in check_number_of_pattern loc n pl; - product_of_cases_patterns [] idsl_pll + product_of_cases_patterns empty_alias idsl_pll (* Expands a disjunction of multiple pattern *) and intern_disjunctive_multiple_pattern env loc n mpl = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 7f11c0a3b..19c872b31 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -19,7 +19,6 @@ open Typeclasses_errors open Pp open Libobject open Nameops -open Misctypes open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -119,11 +118,6 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li | [] -> bdvars, l in aux bound l binders -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Id.Set.add id set - let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = let rec vars bound vs = function | GVar (loc,id) -> @@ -131,61 +125,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp if Id.List.mem_assoc id vs then vs else (id, loc) :: vs else vs - | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> - let vs' = vars bound vs ty in - let bound' = add_name_to_ids bound na in - vars bound' vs' c - | GLetIn (loc,na,b,ty,c) -> - let vs' = vars bound vs b in - let vs'' = Option.fold_left (vars bound) vs' ty in - let bound' = add_name_to_ids bound na in - vars bound' vs'' c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let vs1 = vars_option bound vs rtntypopt in - let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in - List.fold_left (vars_pattern bound) vs2 pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let vs1 = vars_return_type bound vs rtntyp in - let vs2 = vars bound vs1 b in - let bound' = List.fold_left add_name_to_ids bound nal in - vars bound' vs2 c - | GIf (loc,c,rtntyp,b1,b2) -> - let vs1 = vars_return_type bound vs rtntyp in - let vs2 = vars bound vs1 c in - let vs3 = vars bound vs2 b1 in - vars bound vs3 b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bound' = Array.fold_right Id.Set.add idl bound in - let vars_fix i vs fid = - let vs1,bound1 = - List.fold_left - (fun (vs,bound) (na,k,bbd,bty) -> - let vs' = vars_option bound vs bbd in - let vs'' = vars bound vs' bty in - let bound' = add_name_to_ids bound na in - (vs'',bound') - ) - (vs,bound') - bl.(i) - in - let vs2 = vars bound1 vs1 tyl.(i) in - vars bound1 vs2 bv.(i) - in - Array.fold_left_i vars_fix vs idl - | GCast (loc,c,k) -> let v = vars bound vs c in - (match k with CastConv t | CastVM t -> vars bound v t | _ -> v) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs - - and vars_pattern bound vs (loc,idl,p,c) = - let bound' = List.fold_right Id.Set.add idl bound in - vars bound' vs c - - and vars_option bound vs = function None -> vs | Some p -> vars bound vs p - - and vars_return_type bound vs (na,tyopt) = - let bound' = add_name_to_ids bound na in - vars_option bound' vs tyopt + | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vars = List.rev (vars bound [] rt) in List.iter (fun (id, loc) -> diff --git a/interp/notation.ml b/interp/notation.ml index 6aa6f54c0..7be2fe0f0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -444,16 +444,20 @@ let notation_of_prim_token = function | Numeral n -> "- "^(to_string (neg n)) | String _ -> raise Not_found -let find_prim_token g loc p sc = +let find_prim_token check_allowed loc p sc = (* Try for a user-defined numerical notation *) try let (_,c),df = find_notation (notation_of_prim_token p) sc in - g (Notation_ops.glob_constr_of_notation_constr loc c),df + let pat = Notation_ops.glob_constr_of_notation_constr loc c in + check_allowed pat; + pat, df with Not_found -> (* Try for a primitive numerical notation *) let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in check_required_module loc sc spdir; - g (interp ()), ((dirpath (fst spdir),DirPath.empty),"") + let pat = interp () in + check_allowed pat; + pat, ((dirpath (fst spdir),DirPath.empty),"") let interp_prim_token_gen g loc p local_scopes = let scopes = make_current_scopes local_scopes in @@ -466,20 +470,17 @@ let interp_prim_token_gen g loc p local_scopes = | String s -> str "No interpretation for string " ++ qs s) ++ str ".") let interp_prim_token = - interp_prim_token_gen (fun x -> x) + interp_prim_token_gen (fun _ -> ()) -(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) - -let rec rcp_of_glob looked_for = function - | GVar (loc,id) -> RCPatAtom (loc,Some id) - | GHole (loc,_,_,_) -> RCPatAtom (loc,None) - | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[]) +let rec check_allowed_ref_in_pat looked_for = function + | GVar _ | GHole _ -> () + | GRef (_,g,_) -> looked_for g | GApp (loc,GRef (_,g,_),l) -> - looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[]) + looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l | _ -> raise Not_found let interp_prim_token_cases_pattern_expr loc looked_for p = - interp_prim_token_gen (rcp_of_glob looked_for) loc p + interp_prim_token_gen (check_allowed_ref_in_pat looked_for) loc p let interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in diff --git a/interp/notation.mli b/interp/notation.mli index 2e92a00a8..300480ff1 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -85,8 +85,10 @@ val declare_string_interpreter : scope_name -> required_module -> val interp_prim_token : Loc.t -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) + +(* This function returns a glob_const representing a pattern *) val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token -> - local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option) + local_scopes -> glob_constr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index a4a6eb909..77f052ddb 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -36,14 +36,6 @@ type prim_token = | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *) | String of string -type raw_cases_pattern_expr = - | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t - | RCPatCstr of Loc.t * Globnames.global_reference - * raw_cases_pattern_expr list * raw_cases_pattern_expr list - (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *) - | RCPatAtom of Loc.t * Id.t option - | RCPatOr of Loc.t * raw_cases_pattern_expr list - type instance_expr = Misctypes.glob_level list type cases_pattern_expr = diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 33dc2a335..7c2dc5177 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -48,8 +48,8 @@ type 'a glob_sort_gen = | GProp (** representation of [Prop] literal *) | GSet (** representation of [Set] literal *) | GType of 'a (** representation of [Type] literal *) -type sort_info = string Loc.located list -type level_info = string Loc.located option +type sort_info = Name.t Loc.located list +type level_info = Name.t Loc.located option type glob_sort = sort_info glob_sort_gen type glob_level = level_info glob_sort_gen diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 4884d0deb..6971c0a2b 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -354,13 +354,15 @@ let get_new_edges g to_merge = UMap.empty to_merge in let ltle = - UMap.fold (fun _ n acc -> - UMap.merge (fun _ strict1 strict2 -> - match strict1, strict2 with - | Some true, _ | _, Some true -> Some true - | _, _ -> Some false) - acc n.ltle) - to_merge_lvl UMap.empty + let fold _ n acc = + let fold u strict acc = + if strict then UMap.add u strict acc + else if UMap.mem u acc then acc + else UMap.add u false acc + in + UMap.fold fold n.ltle acc + in + UMap.fold fold to_merge_lvl UMap.empty in let ltle, _ = clean_ltle g ltle in let ltle = diff --git a/lib/option.ml b/lib/option.ml index fbb883d30..50fdd079d 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -20,24 +20,24 @@ let has_some = function | _ -> true let is_empty = function -| None -> true -| Some _ -> false + | None -> true + | Some _ -> false (** Lifting equality onto option types. *) let equal f x y = match x, y with -| None, None -> true -| Some x, Some y -> f x y -| _, _ -> false + | None, None -> true + | Some x, Some y -> f x y + | _, _ -> false let compare f x y = match x, y with -| None, None -> 0 -| Some x, Some y -> f x y -| None, Some _ -> -1 -| Some _, None -> 1 + | None, None -> 0 + | Some x, Some y -> f x y + | None, Some _ -> -1 + | Some _, None -> 1 let hash f = function -| None -> 0 -| Some x -> f x + | None -> 0 + | Some x -> f x exception IsNone @@ -57,13 +57,11 @@ let init b x = else None - (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) let flatten = function | Some (Some y) -> Some y | _ -> None - (** [append x y] is the first element of the concatenation of [x] and [y] seen as lists. *) let append o1 o2 = @@ -134,6 +132,7 @@ let cata f a = function | Some c -> f c | None -> a + (** {6 More Specific operations} ***) (** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *) @@ -165,7 +164,6 @@ let lift2 f x y = | _,_ -> None - (** {6 Operations with Lists} *) module List = @@ -183,9 +181,19 @@ module List = | [] -> [] let rec find f = function - |[] -> None - |h :: t -> match f h with - |None -> find f t - |x -> x + | [] -> None + | h :: t -> match f h with + | None -> find f t + | x -> x + + let map f l = + let rec aux f l = match l with + | [] -> [] + | x :: l -> + match f x with + | None -> raise Exit + | Some y -> y :: aux f l + in + try Some (aux f l) with Exit -> None end diff --git a/lib/option.mli b/lib/option.mli index 5e085620e..f06ad9f1d 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -122,5 +122,14 @@ module List : sig [Some y] (in the same order). *) val flatten : 'a option list -> 'a list + (** [List.find f l] is the first [f a] different from [None], + scrolling through elements [a] of [l] in left-to-right order; + it is [None] if no such element exists. *) val find : ('a -> 'b option) -> 'a list -> 'b option + + (** [List.map f [a1;...;an]] is the list [Some [b1;...;bn]] if + for all i, there is a [bi] such that [f ai] is [Some bi]; it is + [None] if, for at least one i, [f ai] is [None]. *) + val map : ('a -> 'b option) -> 'a list -> 'b list option + end diff --git a/library/declare.ml b/library/declare.ml index 31c9c24bc..91e0cb44b 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -514,11 +514,10 @@ let do_constraint poly l = match x with | GProp -> Loc.dummy_loc, (false, Univ.Level.prop) | GSet -> Loc.dummy_loc, (false, Univ.Level.set) - | GType None -> + | GType None | GType (Some (_, Anonymous)) -> user_err ~hdr:"Constraint" (str "Cannot declare constraints on anonymous universes") - | GType (Some (loc, id)) -> - let id = Id.of_string id in + | GType (Some (loc, Name id)) -> let names, _ = Global.global_universe_names () in try loc, Idmap.find id names with Not_found -> diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 97a3e89a5..984957589 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -17,7 +17,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : - Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item + Loc.t * 'a raw_abstract_argument_type option * ('s, 'a) symbol -> 's grammar_prod_item type 'a ty_arg = ('a -> raw_generic_argument) @@ -38,7 +38,7 @@ let rec ty_rule_of_gram = function AnyTyRule r | GramNonTerminal (_, t, tok) :: rem -> let AnyTyRule rem = ty_rule_of_gram rem in - let inj = Some (fun obj -> Genarg.in_gen t obj) in + let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in let r = TyNext (rem, tok, inj) in AnyTyRule r diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 1ad947200..29baaf052 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -15,7 +15,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string - | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type * + | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type option * ('s, 'a) Extend.symbol -> 's grammar_prod_item val extend_vernac_command_grammar : diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 0f2ed88fe..15f100c3b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -146,12 +146,12 @@ GEXTEND Gram [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType [] - | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u) + | "Type"; "@{"; u = universe; "}" -> GType u ] ] ; universe: - [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids - | id = identref -> [id] + [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids + | id = name -> [id] ] ] ; lconstr: @@ -298,7 +298,7 @@ GEXTEND Gram [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None - | id = identref -> GType (Some (fst id, Id.to_string (snd id))) + | id = name -> GType (Some id) ] ] ; fix_constr: diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 7c5efaea3..1cb417bf4 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -397,33 +397,18 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = simplest_elim false_t] end } -let discriminate_tac (cstr,u as cstru) p = +(* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *) +let discriminate_tac cstru p = Proofview.Goal.enter { enter = begin fun gl -> - let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in + let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl gl in - let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in - let identity = Universes.constr_of_global (Lazy.force _I) in - let identity = EConstr.of_constr identity in - let trivial = Universes.constr_of_global (Lazy.force _True) in - let trivial = EConstr.of_constr trivial in let evm = Tacmach.New.project gl in - let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in - let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in - let outtype = mkSort outtype in - let pred = mkLambda(Name xid,outtype,mkRel 1) in + let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in - let proj = build_projection intype cstru trivial concl gl in - let injt = app_global _f_equal - [|intype;outtype;proj;t1;t2;mkVar hid|] in - let endt k = - injt (fun injt -> - app_global _eq_rect - [|outtype;trivial;pred;identity;concl;injt|] k) in - let neweq = app_global _eq [|intype;t1;t2|] in + let neweq=app_global _eq [|intype;lhs;rhs|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) - [proof_tac p; endt refine_exact_check]) + [proof_tac p; Equality.discrHyp hid]) end } (* wrap everything *) diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 53b726432..ec3a49df4 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause | [ in_clause'(cl) ] -> [ cl ] END +let local_test_lpar_id_colon = + let err () = raise Stream.Failure in + Pcoq.Gram.Entry.of_parser "lpar_id_colon" + (fun strm -> + match Util.stream_nth 0 strm with + | Tok.KEYWORD "(" -> + (match Util.stream_nth 1 strm with + | Tok.IDENT _ -> + (match Util.stream_nth 2 strm with + | Tok.KEYWORD ":" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +let pr_lpar_id_colon _ _ _ _ = mt () + +ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon +| [ local_test_lpar_id_colon(x) ] -> [ () ] +END + (* spiwack: the print functions are incomplete, but I don't know what they are used for *) let pr_r_nat_field natf = diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 7d4bccfad..9b4167512 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -67,6 +67,10 @@ val pr_by_arg_tac : (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> raw_tactic_expr option -> Pp.std_ppcmds +val test_lpar_id_colon : unit Pcoq.Gram.entry + +val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type + (** Spiwack: Primitive for retroknowledge registration *) val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 21419d1f9..bd48614db 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -463,7 +463,7 @@ open Evar_tactics (* TODO: add support for some test similar to g_constr.name_colon so that expressions like "evar (list A)" do not raise a syntax error *) TACTIC EXTEND evar - [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] + [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] END @@ -812,6 +812,19 @@ TACTIC EXTEND destauto | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END +(**********************************************************************) + +(**********************************************************************) +(* A version of abstract constructing transparent terms *) +(* Introduced by Jason Gross and Benjamin Delaware in June 2016 *) +(**********************************************************************) + +TACTIC EXTEND transparent_abstract +| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl -> + Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ] +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl -> + Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ] +END (* ********************************************************************* *) diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ca5d198c2..d717ed0a5 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -460,7 +460,9 @@ END let pr_ltac_production_item = function | Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, (arg, sep), id) -> +| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg +| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false +| Tacentries.TacNonTerm (_, (arg, sep), Some id) -> let sep = match sep with | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) @@ -470,7 +472,9 @@ let pr_ltac_production_item = function VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item | [ string(s) ] -> [ Tacentries.TacTerm s ] | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ] + [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ] +| [ ident(nt) ] -> + [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ] END VERNAC COMMAND EXTEND VernacTacticNotation diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 4b3ca80af..e33c25cf8 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq = | _ -> err ()) (* idem for (x:t) *) -let test_lpar_id_colon = - Gram.Entry.of_parser "lpar_id_colon" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ":" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) +open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index b73b66e56..a61957559 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list @@ -264,8 +264,9 @@ type 'a extra_genarg_printer = let rec pack prods args = match prods, args with | [], [] -> [] | TacTerm s :: prods, args -> TacTerm s :: pack prods args - | TacNonTerm (loc, symb, id) :: prods, arg :: args -> - TacNonTerm (loc, (symb, arg), id) :: pack prods args + | TacNonTerm (_, _, None) :: prods, args -> pack prods args + | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args -> + TacNonTerm (loc, (symb, arg), ido) :: pack prods args | _ -> raise Not_found in let prods = pack pp.pptac_prods l in diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 729338fb9..433f342c4 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -21,7 +21,7 @@ open Ppextend type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 32750383b..91262f6fd 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -21,7 +21,7 @@ open Nameops type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type raw_argument = string * string option type argument = Genarg.ArgT.any Extend.user_symbol @@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state = in let map = function | TacTerm s -> GramTerminal s - | TacNonTerm (loc, s, _) -> + | TacNonTerm (loc, s, ido) -> let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in - GramNonTerminal (loc, typ, e) + GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e) in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in @@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s - | TacNonTerm (loc, (nt, sep), id) -> + | TacNonTerm (loc, (nt, sep), ido) -> let symbol = parse_user_entry nt sep in let interp s = function | None -> @@ -220,7 +220,7 @@ let interp_prod_item = function end in let symbol = interp_entry_name interp symbol in - TacNonTerm (loc, symbol, id) + TacNonTerm (loc, symbol, ido) let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in @@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj = let cons_production_parameter = function | TacTerm _ -> None -| TacNonTerm (_, _, id) -> Some id +| TacNonTerm (_, _, ido) -> ido let add_glob_tactic_notation local ~level prods forml ids tac = let parule = { @@ -362,7 +362,7 @@ let add_ml_tactic_notation name ~level prods = let open Tacexpr in let get_id = function | TacTerm s -> None - | TacNonTerm (_, _, id) -> Some id + | TacNonTerm (_, _, ido) -> ido in let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 069504473..dac62dad3 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type raw_argument = string * string option (** An argument type as provided in Tactic notations, i.e. a string like diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index dffeade29..dac15ff79 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -85,6 +85,19 @@ let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None) +let batch = ref false + +open Goptions + +let _ = + declare_bool_option + { optsync = false; + optdepr = false; + optname = "Ltac batch debug"; + optkey = ["Ltac";"Batch";"Debug"]; + optread = (fun () -> !batch); + optwrite = (fun x -> batch := x) } + let rec drop_spaces inst i = if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1) else i @@ -150,6 +163,7 @@ let rec prompt level = begin let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> + if Pervasives.(!batch) then return (DebugOn (level+1)) else let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index fc9d70ae7..c649cfb2c 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -8,7 +8,7 @@ (* The `Quote' tactic *) -(* The basic idea is to automatize the inversion of interpetation functions +(* The basic idea is to automatize the inversion of interpretation functions in 2-level approach Examples are given in \texttt{theories/DEMOS/DemoQuote.v} diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index d59ffee54..6b8ef630a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -333,12 +333,12 @@ let _ = add_map "ring" my_reference "gen_phiZ", (function _->Eval); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot); pol_cst "Pphi_pow", (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring + (* PEeval: evaluate polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)]) + pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot)]) (****************************************************************************) (* Ring database *) @@ -780,20 +780,20 @@ let _ = add_map "field" (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) my_reference "display_linear", - (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); + (function -1|9|10|11|13|15|16->Eval|12|14->Rec|_->Prot); my_reference "display_pow_linear", (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot); pol_cst "Pphi_pow", - (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring + (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot); + (* PEeval: evaluate polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot); - (* FEeval: evaluate morphism, protect field + pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot); + (* FEeval: evaluate polynomial, protect field operations and make recursive call on the var map *) - my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);; + my_reference "FEeval", (function -1|12|15->Eval|10|14->Rec|_->Prot)]);; let _ = add_map "field_cond" (map_without_eq diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6bc2a4f94..8a49cd548 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1245,6 +1245,12 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let typs = List.map2 RelDecl.set_name names cs_args in + (* Beta-iota-normalize types to better compatibility of refine with 8.4 behavior *) + (* This is a bit too strong I think, in the sense that what we would *) + (* really like is to have beta-iota reduction only at the positions where *) + (* parameters are substituted *) + let typs = List.map (map_type (nf_betaiota !(pb.evdref))) typs in + (* We build the matrix obtained by expanding the matching on *) (* "C x1..xn as x" followed by a residual matching on eqn into *) (* a matching on "x1 .. xn eqn" *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index e18625c42..bd7350dc4 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -175,6 +175,19 @@ let cofixp_reducible flgs _ stk = else false +let debug_cbv = ref false +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optname = "cbv visited constants display"; + Goptions.optkey = ["Debug";"Cbv"]; + Goptions.optread = (fun () -> !debug_cbv); + Goptions.optwrite = (fun a -> debug_cbv:=a); +} + +let pr_key = function + | ConstKey (sp,_) -> Names.Constant.print sp + | VarKey id -> Names.Id.print id + | RelKey n -> Pp.(str "REL_" ++ int n) (* The main recursive functions * @@ -254,9 +267,17 @@ let rec norm_head info env t stack = and norm_head_ref k info env stack normt = if red_set_ref (info_flags info) normt then match ref_value_cache info normt with - | Some body -> strip_appl (shift_value k body) stack - | None -> (VAL(0,make_constr_ref k normt),stack) - else (VAL(0,make_constr_ref k normt),stack) + | Some body -> + if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); + strip_appl (shift_value k body) stack + | None -> + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + (VAL(0,make_constr_ref k normt),stack) + else + begin + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + (VAL(0,make_constr_ref k normt),stack) + end (* cbv_stack_term performs weak reduction on constr t under the subs * env, with context stack, i.e. ([env]t stack). First computes weak diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 2334be966..edcfa99c8 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -361,6 +361,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst + | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> + Array.fold_left2 (sorec ctx env) subst args1 args2 | _ -> raise PatternMatchingFailure in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1eec85f45..0d798b4d9 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -422,7 +422,9 @@ let detype_sort sigma = function | Type u -> GType (if !print_universes - then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)] + then + let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in + [dl, Name.mk_name (Id.of_string_soft u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -434,7 +436,8 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l))) + let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in + GType (Some (dl, Name.mk_name (Id.of_string_soft l))) let detype_instance sigma l = let l = EInstance.kind sigma l in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f0d011477..4ada91eb5 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -470,23 +470,13 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c = (* Managing pattern-unification *) (********************************) -let map_all f l = - let rec map_aux f l = match l with - | [] -> [] - | x :: l -> - match f x with - | None -> raise Exit - | Some y -> y :: map_aux f l - in - try Some (map_aux f l) with Exit -> None - let expand_and_check_vars sigma aliases l = let map a = match get_alias_chain_of sigma aliases a with | None, [] -> Some a | None, a :: _ -> Some a | Some _, _ -> None in - map_all map l + Option.List.map map l let alias_distinct l = let rec check (rels, vars) = function @@ -540,7 +530,7 @@ let is_unification_pattern_meta env evd nb m l t = | Rel n -> if n <= nb then Some (RelAlias n) else None | _ -> None in - match map_all map l with + match Option.List.map map l with | Some l -> begin match find_unification_pattern_args env evd l t with | Some _ as x when not (dependent evd (mkMeta m) t) -> x @@ -550,10 +540,10 @@ let is_unification_pattern_meta env evd nb m l t = None let is_unification_pattern_evar env evd (evk,args) l t = - match map_all (fun c -> to_alias evd c) l with + match Option.List.map (fun c -> to_alias evd c) l with | Some l when noccur_evar env evd evk t -> let args = remove_instance_local_defs evd evk args in - let args = map_all (fun c -> to_alias evd c) args in + let args = Option.List.map (fun c -> to_alias evd c) args in begin match args with | None -> None | Some args -> diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index ebbfa195f..6509aaac3 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -214,120 +214,62 @@ let fold_glob_constr f acc = function f acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc -let iter_glob_constr f = fold_glob_constr (fun () -> f) () +let fold_return_type_with_binders f g v acc (na,tyopt) = + Option.fold_left (f (name_fold g na v)) acc tyopt -let same_id na id = match na with -| Anonymous -> false -| Name id' -> Id.equal id id' +let fold_glob_constr_with_binders g f v acc = function + | GVar _ -> acc + | GApp (_,c,args) -> List.fold_left (f v) (f v acc c) args + | GLambda (_,na,_,b,c) | GProd (_,na,_,b,c) -> + f (name_fold g na v) (f v acc b) c + | GLetIn (_,na,b,t,c) -> + f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c + | GCases (_,_,rtntypopt,tml,pl) -> + let fold_pattern acc (_,idl,p,c) = f (List.fold_right g idl v) acc c in + let fold_tomatch (v',acc) (tm,(na,onal)) = + (Option.fold_left (fun v'' (_,_,nal) -> List.fold_right (name_fold g) nal v'') + (name_fold g na v') onal, + f v acc tm) in + let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in + let acc = Option.fold_left (f v') acc rtntypopt in + List.fold_left fold_pattern acc pl + | GLetTuple (_,nal,rtntyp,b,c) -> + f v (f v (fold_return_type_with_binders f g v acc rtntyp) b) c + | GIf (_,c,rtntyp,b1,b2) -> + f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2 + | GRec (_,_,idl,bll,tyl,bv) -> + let f' i acc fid = + let v,acc = + List.fold_left + (fun (v,acc) (na,k,bbd,bty) -> + (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty)) + (v,acc) + bll.(i) in + f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in + Array.fold_left_i f' acc idl + | GCast (_,c,k) -> + let acc = match k with + | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in + f v acc c + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc + +let iter_glob_constr f = fold_glob_constr (fun () -> f) () let occur_glob_constr id = - let rec occur = function + let rec occur barred acc = function | GVar (loc,id') -> Id.equal id id' - | GApp (loc,f,args) -> (occur f) || (List.exists occur args) - | GLambda (loc,na,bk,ty,c) -> - (occur ty) || (not (same_id na id) && (occur c)) - | GProd (loc,na,bk,ty,c) -> - (occur ty) || (not (same_id na id) && (occur c)) - | GLetIn (loc,na,b,t,c) -> - (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c)) - | GCases (loc,sty,rtntypopt,tml,pl) -> - (occur_option rtntypopt) - || (List.exists (fun (tm,_) -> occur tm) tml) - || (List.exists occur_pattern pl) - | GLetTuple (loc,nal,rtntyp,b,c) -> - occur_return_type rtntyp id - || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c)) - | GIf (loc,c,rtntyp,b1,b2) -> - occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2) - | GRec (loc,fk,idl,bl,tyl,bv) -> - not (Array.for_all4 (fun fid bl ty bd -> - let rec occur_fix = function - [] -> not (occur ty) && (Id.equal fid id || not(occur bd)) - | (na,k,bbd,bty)::bl -> - not (occur bty) && - (match bbd with - Some bd -> not (occur bd) - | _ -> true) && - (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in - occur_fix bl) - idl bl tyl bv) - | GCast (loc,c,k) -> (occur c) || (match k with CastConv t - | CastVM t | CastNative t -> occur t | CastCoerce -> false) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false - - and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c) - - and occur_option = function None -> false | Some p -> occur p - - and occur_return_type (na,tyopt) id = not (same_id na id) && occur_option tyopt - - in occur - - -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Id.Set.add id set + | c -> + (* [g] looks if [id] appears in a binding position, in which + case, we don't have to look in the corresponding subterm *) + let g id' barred = barred || Id.equal id id' in + let f barred acc c = acc || not barred && occur false acc c in + fold_glob_constr_with_binders g f barred acc c in + occur false false let free_glob_vars = - let rec vars bounded vs = function - | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs - | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> - let vs' = vars bounded vs ty in - let bounded' = add_name_to_ids bounded na in - vars bounded' vs' c - | GLetIn (loc,na,b,ty,c) -> - let vs' = vars bounded vs b in - let vs'' = Option.fold_left (vars bounded) vs' ty in - let bounded' = add_name_to_ids bounded na in - vars bounded' vs'' c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let vs1 = vars_option bounded vs rtntypopt in - let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in - List.fold_left (vars_pattern bounded) vs2 pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let vs1 = vars_return_type bounded vs rtntyp in - let vs2 = vars bounded vs1 b in - let bounded' = List.fold_left add_name_to_ids bounded nal in - vars bounded' vs2 c - | GIf (loc,c,rtntyp,b1,b2) -> - let vs1 = vars_return_type bounded vs rtntyp in - let vs2 = vars bounded vs1 c in - let vs3 = vars bounded vs2 b1 in - vars bounded vs3 b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bounded' = Array.fold_right Id.Set.add idl bounded in - let vars_fix i vs fid = - let vs1,bounded1 = - List.fold_left - (fun (vs,bounded) (na,k,bbd,bty) -> - let vs' = vars_option bounded vs bbd in - let vs'' = vars bounded vs' bty in - let bounded' = add_name_to_ids bounded na in - (vs'',bounded') - ) - (vs,bounded') - bl.(i) - in - let vs2 = vars bounded1 vs1 tyl.(i) in - vars bounded1 vs2 bv.(i) - in - Array.fold_left_i vars_fix vs idl - | GCast (loc,c,k) -> let v = vars bounded vs c in - (match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs - - and vars_pattern bounded vs (loc,idl,p,c) = - let bounded' = List.fold_right Id.Set.add idl bounded in - vars bounded' vs c - - and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p - - and vars_return_type bounded vs (na,tyopt) = - let bounded' = add_name_to_ids bounded na in - vars_option bounded' vs tyopt - in + let rec vars bound vs = function + | GVar (loc,id') -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs + | c -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vs = vars Id.Set.empty Id.Set.empty rt in Id.Set.elements vs @@ -353,57 +295,16 @@ let add_and_check_ident id set = Id.Set.add id set let bound_glob_vars = - let rec vars bound = function - | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c -> - let bound = name_fold add_and_check_ident na bound in - fold_glob_constr vars bound c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let bound = vars_option bound rtntypopt in - let bound = - List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in - List.fold_left vars_pattern bound pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound b in - let bound = List.fold_right (name_fold add_and_check_ident) nal bound in - vars bound c - | GIf (loc,c,rtntyp,b1,b2) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound c in - let bound = vars bound b1 in - vars bound b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bound = Array.fold_right Id.Set.add idl bound in - let vars_fix i bound fid = - let bound = - List.fold_left - (fun bound (na,k,bbd,bty) -> - let bound = vars_option bound bbd in - let bound = vars bound bty in - name_fold add_and_check_ident na bound - ) - bound - bl.(i) - in - let bound = vars bound tyl.(i) in - vars bound bv.(i) - in - Array.fold_left_i vars_fix bound idl - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound - | GApp _ | GCast _ as c -> fold_glob_constr vars bound c - - and vars_pattern bound (loc,idl,p,c) = - let bound = List.fold_right add_and_check_ident idl bound in - vars bound c - - and vars_option bound = function None -> bound | Some p -> vars bound p - - and vars_return_type bound (na,tyopt) = - let bound = name_fold add_and_check_ident na bound in - vars_option bound tyopt + let rec vars bound = + fold_glob_constr_with_binders + (fun id () -> bound := add_and_check_ident id !bound) + (fun () () -> vars bound) + () () in fun rt -> - vars Id.Set.empty rt + let bound = ref Id.Set.empty in + vars bound rt; + !bound (** Mapping of names in binders *) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533..af2834e49 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -37,6 +37,7 @@ val map_glob_constr_left_to_right : val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a +val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 7fe81c9a4..1669f8334 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,7 @@ let smartmap_cast_type f c = let glob_sort_eq g1 g2 = match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true -| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2 +| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2 | _ -> false let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 33a68589c..a22db1407 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -159,7 +159,9 @@ let pattern_of_constr env sigma t = (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> + | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> + (* These are the two evar kinds used for existing goals *) + (* see Proofview.mark_in_evm *) PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> PMeta None) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index fa37f8cf6..7b9d9ae4b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -192,45 +192,51 @@ let _ = optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) -let interp_universe_level_name evd (loc,s) = - let names, _ = Global.global_universe_names () in - if CString.string_contains ~where:s ~what:"." then - match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s) - | n :: dp -> - let num = int_of_string n in - let dp = DirPath.make (List.map Id.of_string dp) in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - else - try - let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, snd (Idmap.find id names) - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ~loc ~name:s univ_rigid evd - else user_err ~loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) +let interp_universe_level_name ~anon_rigidity evd (loc,s) = + match s with + | Anonymous -> + new_univ_level_variable ~loc anon_rigidity evd + | Name s -> + let s = Id.to_string s in + let names, _ = Global.global_universe_names () in + if CString.string_contains ~where:s ~what:"." then + match List.rev (CString.split '.' s) with + | [] -> anomaly (str"Invalid universe name " ++ str s) + | n :: dp -> + let num = int_of_string n in + let dp = DirPath.make (List.map Id.of_string dp) in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level + else + try + let level = Evd.universe_of_name evd s in + evd, level + with Not_found -> + try + let id = try Id.of_string s with _ -> raise Not_found in + evd, snd (Idmap.find id names) + with Not_found -> + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ~loc ~name:s univ_rigid evd + else user_err ~loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ str s)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in evd, Univ.Universe.make l | l -> List.fold_left (fun (evd, u) l -> - let evd', l = interp_universe_level_name evd l in + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in (evd', Univ.sup u (Univ.Universe.make l))) (evd, Univ.Universe.type0m) l let interp_level_info loc evd : Misctypes.level_info -> _ = function | None -> new_univ_level_variable ~loc univ_rigid evd - | Some (loc,s) -> interp_universe_level_name evd (loc,s) + | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (loc,s) let interp_sort ?loc evd = function | GProp -> evd, Prop Null diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 3041ac259..b546c39ae 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -151,8 +151,8 @@ let tag_var = tag Tag.variable let pr_univ l = match l with - | [_,x] -> str x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")" + | [_,x] -> pr_name x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> pr_name (snd x)) l ++ str")" let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" @@ -166,7 +166,7 @@ let tag_var = tag Tag.variable | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType None -> tag_type (str "Type") - | GType (Some (_, u)) -> tag_type (str u) + | GType (Some (_, u)) -> tag_type (pr_name u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -191,7 +191,7 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | Some (_,u) -> str u + | Some (_,u) -> pr_name u | None -> tag_type (str "Type")) let pr_universe_instance l = diff --git a/printing/printer.ml b/printing/printer.ml index 93d221f03..e0ca51f0c 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -28,12 +28,53 @@ module CompactedDecl = Context.Compacted.Declaration let emacs_str s = if !Flags.print_emacs then s else "" -let delayed_emacs_cmd s = - if !Flags.print_emacs then s () else str "" let get_current_context () = Pfedit.get_current_context () +let enable_unfocused_goal_printing = ref false +let enable_goal_tags_printing = ref false +let enable_goal_names_printing = ref false + +let should_tag() = !enable_goal_tags_printing +let should_unfoc() = !enable_unfocused_goal_printing +let should_gname() = !enable_goal_names_printing + + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of unfocused goal"; + optkey = ["Printing";"Unfocused"]; + optread = (fun () -> !enable_unfocused_goal_printing); + optwrite = (fun b -> enable_unfocused_goal_printing:=b) } + +(* This is set on by proofgeneral proof-tree mode. But may be used for + other purposes *) +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of goal tags"; + optkey = ["Printing";"Goal";"Tags"]; + optread = (fun () -> !enable_goal_tags_printing); + optwrite = (fun b -> enable_goal_tags_printing:=b) } + + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of goal names"; + optkey = ["Printing";"Goal";"Names"]; + optread = (fun () -> !enable_goal_names_printing); + optwrite = (fun b -> enable_goal_names_printing:=b) } + + (**********************************************************************) (** Terms *) @@ -262,6 +303,13 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (**********************************************************************) (* Contexts and declarations *) + +(* Flag for compact display of goals *) + +let get_compact_context,set_compact_context = + let compact_context = ref false in + (fun () -> !compact_context),(fun b -> compact_context := b) + let pr_compacted_decl env sigma decl = let ids, pbody, typ = match decl with | CompactedDecl.LocalAssum (ids, typ) -> @@ -342,15 +390,40 @@ let pr_ne_context_of header env sigma = List.is_empty (Environ.named_context env) then (mt ()) else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ()) +(* Heuristic for horizontalizing hypothesis that the user probably + considers as "variables": An hypothesis H:T where T:S and S<>Prop. *) +let should_compact env sigma typ = + get_compact_context() && + let type_of_typ = Retyping.get_type_of env sigma (EConstr.of_constr typ) in + not (is_Prop (EConstr.to_constr sigma type_of_typ)) + + +(* If option Compact Contexts is set, we pack "simple" hypothesis in a + hov box (with three sapaces as a separator), the global box being a + v box *) let rec bld_sign_env env sigma ctxt pps = match ctxt with | [] -> pps + | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ -> + let pps',ctxt' = bld_sign_env_id env sigma ctxt (mt ()) true in + (* putting simple hyps in a more horizontal flavor *) + bld_sign_env env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps') | d:: ctxt' -> - let pidt = pr_var_list_decl env sigma d in - let pps' = pps ++ brk (0,0) ++ pidt in - bld_sign_env env sigma ctxt' pps' + let pidt = pr_var_list_decl env sigma d in + let pps' = pps ++ brk (0,0) ++ pidt in + bld_sign_env env sigma ctxt' pps' +and bld_sign_env_id env sigma ctxt pps is_start = + match ctxt with + | [] -> pps,ctxt + | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ -> + let pidt = pr_var_list_decl env sigma d in + let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in + bld_sign_env_id env sigma ctxt' pps' false + | _ -> pps,ctxt +(* compact printing an env (variables and de Bruijn). Separator: three + spaces between simple hyps, and newline otherwise *) let pr_context_limit_compact ?n env sigma = let ctxt = Termops.compact_named_context (named_context env) in let lgth = List.length ctxt in @@ -360,15 +433,14 @@ let pr_context_limit_compact ?n env sigma = | Some n when n > lgth -> lgth | Some n -> n in let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in - (* a dot line hinting the number of hiden hyps. *) + (* a dot line hinting the number of hidden hyps. *) let hidden_dots = String.make (List.length ctxt_hidden) '.' in let sign_env = v 0 (str hidden_dots ++ (mt ()) ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in let db_env = - fold_rel_context - (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d) + fold_rel_context (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d) env ~init:(mt ()) in - (sign_env ++ db_env) + sign_env ++ db_env (* The number of printed hypothesis in a goal *) (* If [None], no limit *) @@ -419,23 +491,25 @@ let default_pr_goal gs = (* display a goal tag *) let pr_goal_tag g = let s = " (ID " ^ Goal.uid g ^ ")" in - str (emacs_str s) - -let display_name = false + str s (* display a goal name *) let pr_goal_name sigma g = - if display_name then str " " ++ Pp.surround (pr_existential_key sigma g) + if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt () +let pr_goal_header nme sigma g = + let (g,sigma) = Goal.V82.nf_evar sigma g in + str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"") + ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ()) + (* display the conclusion of a goal *) let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in - str (emacs_str "") ++ - str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++ - str " is:" ++ cut () ++ str" " ++ pc + let header = pr_goal_header (int n) sigma g in + header ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) let pr_evgl_sign sigma evi = @@ -491,8 +565,8 @@ let pr_ne_evar_set hd tl sigma l = let pr_selected_subgoal name sigma g = let pg = default_pr_goal { sigma=sigma ; it=g; } in - v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g - ++ str " is:" ++ cut () ++ pg) + let header = pr_goal_header name sigma g in + v 0 (header ++ str " is:" ++ cut () ++ pg) let default_pr_subgoal n sigma = let rec prrec p = function @@ -585,27 +659,27 @@ let print_dependent_evars gl sigma seeds = end i (str ",") end evars (str "") in - fnl () ++ - str "(dependent evars:" ++ evars ++ str ")" ++ fnl () - else - fnl () ++ - str "(dependent evars: (printing disabled) )" ++ fnl () + cut () ++ cut () ++ + str "(dependent evars:" ++ evars ++ str ")" + else if !Flags.print_emacs then + (* IDEs prefer something dummy instead of nothing *) + cut () ++ cut () ++ str "(dependent evars: (printing disabled) )" + else mt () in - constraints ++ delayed_emacs_cmd evars + constraints ++ evars () (* Print open subgoals. Checks for uninstantiated existential variables *) (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) -(* courtieu: in emacs mode, even less cases where the first goal is printed - in its entirety *) -let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals = +let default_pr_subgoals ?(pr_first=true) + close_cmd sigma seeds shelf stack unfocused goals = (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a | b::l -> Pp.int a ++ str"-" ++ print_stack b l in - let print_unfocused l = + let print_unfocused_nums l = match l with | [] -> None | a::l -> Some (str"unfocused: " ++ print_stack a l) @@ -625,7 +699,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals | [] -> Pp.mt () | a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")" in - let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in + let extra = Option.List.flatten [ print_unfocused_nums stack ; print_shelf shelf ] in let print_extra = print_extra_list extra in let focused_if_needed = let needed = not (CList.is_empty extra) && pr_first in @@ -642,8 +716,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals in let print_multiple_goals g l = if pr_first then - default_pr_goal { it = g ; sigma = sigma; } ++ fnl () ++ - pr_rec 2 l + default_pr_goal { it = g ; sigma = sigma; } + ++ (if l=[] then mt () else cut ()) + ++ pr_rec 2 l else pr_rec 1 (g::l) in @@ -658,32 +733,27 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals begin let exl = Evarutil.non_instantiated sigma in if Evar.Map.is_empty exl then - (str"No more subgoals." - ++ print_dependent_evars None sigma seeds) + (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else let pei = pr_evars_int sigma 1 exl in - (str "No more subgoals, but there are non-instantiated existential variables:" - ++ fnl () ++ (hov 0 pei) - ++ print_dependent_evars None sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + v 0 ((str "No more subgoals," + ++ str " but there are non-instantiated existential variables:" + ++ cut () ++ (hov 0 pei) + ++ print_dependent_evars None sigma seeds + ++ cut () ++ str "You can use Grab Existential Variables.")) end - | [g] when not !Flags.print_emacs && pr_first -> - let pg = default_pr_goal { it = g ; sigma = sigma; } in - v 0 ( - str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra - ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg - ++ print_dependent_evars (Some g) sigma seeds - ) | g1::rest -> let goals = print_multiple_goals g1 rest in let ngoals = List.length rest+1 in v 0 ( - int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ - print_extra ++ - str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1") - ++ pr_goal_tag g1 - ++ pr_goal_name sigma g1 ++ cut () - ++ goals + int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") + ++ print_extra + ++ str (if (should_gname()) then ", subgoal 1" else "") + ++ (if should_tag() then pr_goal_tag g1 else str"") + ++ pr_goal_name sigma g1 ++ cut () ++ goals + ++ (if unfocused=[] then str "" + else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut() + ++ pr_rec (List.length rest + 2) unfocused)) ++ print_dependent_evars (Some g1) sigma seeds ) @@ -692,7 +762,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals type printer_pr = { - pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; } @@ -726,16 +796,16 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = begin match goals with | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in begin match bgoals,shelf,given_up with - | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals + | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals | [] , [] , _ -> Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up + ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> Feedback.msg_info (str "All the remaining goals are on the shelf."); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf + ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ @@ -743,9 +813,13 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = if Pp.ismt s then s else fnl () ++ s) ++ fnl () in - pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals + pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals end - | _ -> pr_subgoals None sigma seeds shelf stack goals + | _ -> + let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in + let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in + let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in + pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused end let pr_nth_open_subgoal n = diff --git a/printing/printer.mli b/printing/printer.mli index 504392e35..24107394e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -18,6 +18,11 @@ open Glob_term (** These are the entry points for printing terms, context, tac, ... *) + +val enable_unfocused_goal_printing: bool ref +val enable_goal_tags_printing : bool ref +val enable_goal_names_printing : bool ref + (** Terms *) val pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds @@ -111,6 +116,9 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds (** Contexts *) +(** Display compact contexts of goals (simple hyps on the same line) *) +val set_compact_context : bool -> unit +val get_compact_context : unit -> bool val pr_context_unlimited : env -> evar_map -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds @@ -132,10 +140,22 @@ val pr_cpred : Cpred.t -> std_ppcmds val pr_idpred : Id.Pred.t -> std_ppcmds val pr_transparent_state : transparent_state -> std_ppcmds -(** Proofs *) +(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) val pr_goal : goal sigma -> std_ppcmds -val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds + +(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals] + prints the goals of the list [goals] followed by the goals in + [unfocused], in a short way (typically only the conclusion) except + for the first goal if [pr_first] is true. This function can be + replaced by another one by calling [set_printer_pr] (see below), + typically by plugin writers. The default printer prints only the + focused goals unless the conrresponding option + [enable_unfocused_goal_printing] is set. [seeds] is for printing + dependent evars (mainly for emacs proof tree mode). *) +val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list + -> goal list -> goal list -> std_ppcmds + val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds val pr_concl : int -> evar_map -> goal -> std_ppcmds @@ -190,7 +210,7 @@ val pr_goal_by_id : Id.t -> std_ppcmds val pr_goal_by_uid : string -> std_ppcmds type printer_pr = { - pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; };; diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 900c8cc6f..65b2ec32d 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -9,8 +9,6 @@ open Equality open Names open Pp -open Tacticals -open Tactics open Term open Termops open CErrors @@ -127,45 +125,13 @@ let autorewrite ?(conds=Naive) tac_main lbas = (Proofview.tclUNIT()) lbas)) let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) - let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in - let general_rewrite_in id = - let id = ref id in - let to_be_cleared = ref false in - fun dir cstr tac gl -> - let last_hyp_id = - match Tacmach.pf_hyps gl with - d :: _ -> Context.Named.Declaration.get_id d - | _ -> (* even the hypothesis id is missing *) - raise (Logic.RefinerError (Logic.NoSuchHyp !id)) - in - let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in - let gls = gl'.Evd.it in - match gls with - g::_ -> - (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with - d ::_ -> - let lastid = Context.Named.Declaration.get_id d in - if not (Id.equal last_hyp_id lastid) then - begin - let gl'' = - if !to_be_cleared then - tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl - else gl' in - id := lastid ; - to_be_cleared := true ; - gl'' - end - else - begin - to_be_cleared := false ; - gl' - end - | _ -> assert false) (* there must be at least an hypothesis *) - | _ -> assert false (* rewriting cannot complete a proof *) - in - let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y (EConstr.of_constr z) w) in + let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in + let general_rewrite_in id dir cstr tac = + let cstr = EConstr.of_constr cstr in + general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false id cstr false + in Tacticals.New.tclMAP (fun id -> Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac bas -> diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2d6dffdd2..05eb0a976 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1202,7 +1202,7 @@ module Search = struct Feedback.msg_debug (pr_depth info.search_depth ++ str": no match for " ++ Printer.pr_econstr_env (Goal.env gl) s concl ++ - spc () ++ str ", " ++ int (List.length poss) ++ + str ", " ++ int (List.length poss) ++ str" possibilities"); match e with | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 472cd8f22..641929a77 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -67,7 +67,6 @@ let choose_noteq eqonleft = left_with_bindings false Misctypes.NoBindings open Sigma.Notations -open Context.Rel.Declaration (* A surgical generalize which selects the right occurrences by hand *) (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index b08456f2f..d023b4568 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -105,6 +105,12 @@ let get_coq_eq ctx = with Not_found -> error "eq not found." +let univ_of_eq env eq = + let eq = EConstr.of_constr eq in + match kind_of_term (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with + | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false) + | _ -> assert false + (**********************************************************************) (* Check if an inductive type [ind] has the form *) (* *) @@ -761,7 +767,7 @@ let build_congr env (eq,refl,ctx) ind = let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let b = List.nth constrargs (i + mib.mind_nparams - 1) in let varB = fresh env (Id.of_string "B") in @@ -769,6 +775,7 @@ let build_congr env (eq,refl,ctx) ind = let varf = fresh env (Id.of_string "f") in let ci = make_case_info (Global.env()) ind RegularStyle in let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in + let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in let c = my_it_mkLambda_or_LetIn paramsctxt (mkNamedLambda varB (mkSort (Type uni)) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 211a7338b..556df6e55 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4907,7 +4907,7 @@ let shrink_entry sign const = } in (const, args) -let abstract_subproof id gk tac = +let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in @@ -4927,7 +4927,10 @@ let abstract_subproof id gk tac = else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, empty_named_context_val) in let id = next_global_ident_away id (pf_ids_of_hyps gl) in - let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in + let concl = match goal_type with + | None -> Proofview.Goal.concl gl + | Some ty -> ty in + let concl = it_mkNamedProd_or_LetIn concl sign in let concl = try flush_and_check_evars !evdref concl with Uninstantiated_evar _ -> @@ -4957,8 +4960,8 @@ let abstract_subproof id gk tac = else (const, List.rev (Context.Named.to_instance Constr.mkVar sign)) in let args = List.map EConstr.of_constr args in - let cd = Entries.DefinitionEntry const in - let decl = (cd, IsProof Lemma) 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 let cst () = (** do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in @@ -4976,18 +4979,21 @@ let abstract_subproof id gk tac = Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> - exact_no_check (applist (lem, args)) + tacK lem args in let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in Sigma.Unsafe.of_pair (tac, evd) end } +let abstract_subproof ~opaque id gk tac = + cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) + let anon_id = Id.of_string "anonymous" -let tclABSTRACT name_op tac = +let name_op_to_name name_op object_kind suffix = let open Proof_global in - let default_gk = (Global, false, Proof Theorem) in - let s, gk = match name_op with + let default_gk = (Global, false, object_kind) in + match name_op with | Some s -> (try let _, gk, _ = current_proof_statement () in s, gk with NoCurrentProof -> s, default_gk) @@ -4995,9 +5001,13 @@ let tclABSTRACT name_op tac = let name, gk = try let name, gk, _ = current_proof_statement () in name, gk with NoCurrentProof -> anon_id, default_gk in - add_suffix name "_subproof", gk - in - abstract_subproof s gk tac + add_suffix name suffix, gk + +let tclABSTRACT ?(opaque=true) name_op tac = + let s, gk = if opaque + then name_op_to_name name_op (Proof Theorem) "_subproof" + else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in + abstract_subproof ~opaque s gk tac let unify ?(state=full_transparent_state) x y = Proofview.Goal.s_enter { s_enter = begin fun gl -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index ba4a9706d..07a803542 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -401,7 +401,9 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic -val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic +val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic + +val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> unit Proofview.tactic diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex ba85286dd..b99d80e95 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/Makefile b/test-suite/Makefile index c10cd4ed4..39ef05269 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -31,11 +31,12 @@ BIN := ../bin/ LIB := $(shell cd ..; pwd) coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite -bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite -bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite +coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqtopbyte := $(BIN)coqtop.byte -command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source -coqc := $(coqtop) -compile +coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source +coqtopcompile := $(coqtop) -compile coqdep := $(BIN)coqdep -coqlib $(LIB) SHOW := $(if $(VERBOSE),@true,@echo) @@ -52,7 +53,7 @@ get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_ # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1))) has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) -get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command)) +get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload)) bogomips:= @@ -219,7 +220,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be prepared" ; \ @@ -249,7 +250,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ @@ -405,79 +406,26 @@ modules/%.vo: modules/%.v # Miscellaneous tests ####################################################################### -misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log +misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh)) -# Check that both coqdep and coqtop/coqc supports -R -# Check that both coqdep and coqtop/coqc takes the later -R -# See bugs 2242, 2337, 2339 -deps-order: misc/deps-order.log -misc/deps-order.log: - @echo "TEST misc/deps-order" - $(HIDE){ \ - echo $(call log_intro,deps-order); \ - rm -f misc/deps/*/*.vo; \ - tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ - $(coqdep) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \ - | head -n 1 > $$tmpoutput; \ - diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \ - $(bincoqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \ - $(bincoqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \ - $(coqtop) -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \ - S=$$?; times; \ - if [ $$R = 0 -a $$S = 0 ]; then \ - echo $(log_success); \ - echo " misc/deps-order...Ok"; \ - else \ - echo $(log_failure); \ - echo " misc/deps-order...Error! (unexpected order)"; \ - fi; \ - rm $$tmpoutput; \ - } > "$@" - -deps-checksum: misc/deps-checksum.log -misc/deps-checksum.log: - @echo "TEST misc/deps-checksum" - $(HIDE){ \ - echo $(call log_intro,deps-checksum); \ - rm -f misc/deps/*/*.vo; \ - $(bincoqc) -R misc/deps/A A misc/deps/A/A.v; \ - $(bincoqc) -R misc/deps/B A misc/deps/B/A.v; \ - $(bincoqc) -R misc/deps/B A misc/deps/B/B.v; \ - $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \ - if [ $$? = 0 ]; then \ - echo $(log_success); \ - echo " misc/deps-checksum...Ok"; \ - else \ - echo $(log_failure); \ - echo " misc/deps-checksum...Error!"; \ - fi; \ - } > "$@" - - -# Sort universes for the whole standard library -EXPECTED_UNIVERSES := 4 # Prop is not counted -universes: misc/universes.log -misc/universes.log: misc/universes/all_stdlib.v - @echo "TEST misc/universes" +$(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) + @echo "TEST $<" $(HIDE){ \ - $(bincoqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \ - $(bincoqc) -R misc/universes Universes misc/universes/universes 2>&1; \ - mv universes.txt misc/universes; \ - N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \ - times; \ - if [ "$$N" -eq $(EXPECTED_UNIVERSES) ]; then \ + echo $(call log_intro,$<); \ + export coqc="$(coqc)"; \ + export coqtop="$(coqtop)"; \ + export coqdep="$(coqdep)"; \ + export coqtopbyte="$(coqtopbyte)"; \ + "$<" 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ echo $(log_success); \ - echo " misc/universes...Ok ($(EXPECTED_UNIVERSES) universes)"; \ + echo " $<...Ok"; \ else \ echo $(log_failure); \ - echo " misc/universes...Error! ($$N/$(EXPECTED_UNIVERSES) universes)"; \ + echo " $<...Error!"; \ fi; \ } > "$@" -misc/universes/all_stdlib.v: - cd .. && $(MAKE) test-suite/$@ - - # IDE : some tests of backtracking for coqtop -ideslave ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @@ -501,9 +449,9 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) %.vio.log:%.v @echo "TEST $<" $(HIDE){ \ - $(bincoqc) -quick -R vio vio $* 2>&1 && \ + $(coqc) -quick -R vio vio $* 2>&1 && \ $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \ - $(bincoqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ + $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -518,8 +466,8 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) %.chk.log:%.v @echo "TEST $<" $(HIDE){ \ - $(bincoqc) -R coqchk coqchk $* 2>&1 && \ - $(bincoqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \ + $(coqc) -R coqchk coqchk $* 2>&1 && \ + $(coqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v deleted file mode 100644 index 5c64716c7..000000000 --- a/test-suite/bench/lists-100.v +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0. -Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. -Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. -Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3. -Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4. -Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5. -Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6. -Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7. -Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8. -Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9. -Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10. -Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11. -Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12. -Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13. -Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14. -Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15. -Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16. -Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17. -Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18. -Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19. -Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20. -Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21. -Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22. -Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23. -Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24. -Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25. -Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26. -Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27. -Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28. -Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29. -Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30. -Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31. -Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32. -Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33. -Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34. -Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35. -Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36. -Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37. -Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38. -Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39. -Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40. -Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41. -Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42. -Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43. -Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44. -Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45. -Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46. -Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47. -Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48. -Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49. -Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50. -Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51. -Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52. -Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53. -Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54. -Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55. -Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56. -Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57. -Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58. -Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59. -Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60. -Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61. -Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62. -Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63. -Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64. -Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65. -Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66. -Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67. -Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68. -Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69. -Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70. -Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71. -Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72. -Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73. -Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74. -Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75. -Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76. -Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77. -Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78. -Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79. -Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80. -Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81. -Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82. -Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83. -Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84. -Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85. -Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86. -Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87. -Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88. -Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89. -Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90. -Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91. -Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92. -Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93. -Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94. -Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95. -Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96. -Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97. -Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98. -Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99. diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v deleted file mode 100644 index 5c64716c7..000000000 --- a/test-suite/bench/lists_100.v +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0. -Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. -Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. -Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3. -Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4. -Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5. -Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6. -Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7. -Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8. -Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9. -Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10. -Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11. -Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12. -Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13. -Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14. -Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15. -Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16. -Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17. -Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18. -Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19. -Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20. -Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21. -Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22. -Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23. -Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24. -Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25. -Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26. -Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27. -Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28. -Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29. -Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30. -Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31. -Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32. -Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33. -Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34. -Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35. -Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36. -Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37. -Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38. -Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39. -Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40. -Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41. -Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42. -Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43. -Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44. -Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45. -Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46. -Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47. -Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48. -Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49. -Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50. -Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51. -Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52. -Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53. -Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54. -Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55. -Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56. -Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57. -Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58. -Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59. -Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60. -Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61. -Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62. -Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63. -Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64. -Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65. -Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66. -Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67. -Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68. -Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69. -Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70. -Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71. -Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72. -Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73. -Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74. -Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75. -Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76. -Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77. -Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78. -Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79. -Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80. -Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81. -Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82. -Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83. -Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84. -Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85. -Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86. -Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87. -Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88. -Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89. -Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90. -Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91. -Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92. -Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93. -Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94. -Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95. -Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96. -Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97. -Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98. -Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99. diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v index 7d0dc090e..36ab7ff59 100644 --- a/test-suite/bugs/closed/3080.v +++ b/test-suite/bugs/closed/3080.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-nois") -*- *) Delimit Scope type_scope with type. Delimit Scope function_scope with function. diff --git a/test-suite/bugs/closed/3323.v b/test-suite/bugs/closed/3323.v index 22b1603b6..4622634ea 100644 --- a/test-suite/bugs/closed/3323.v +++ b/test-suite/bugs/closed/3323.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 5302 lines to 4649 lines, then from 4660 lines to 355 lines, then from 360 lines to 269 lines, then from 269 lines to 175 lines, then from 144 lines to 119 lines, then from 297 lines to 117 lines, then from 95 lines to 79 lines, then from 82 lines to 68 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3332.v b/test-suite/bugs/closed/3332.v index d86470cde..a3564bfcc 100644 --- a/test-suite/bugs/closed/3332.v +++ b/test-suite/bugs/closed/3332.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-time") -*- *) +(* -*- coq-prog-args: ("-time") -*- *) Definition foo : True. Proof. Abort. (* Toplevel input, characters 15-21: diff --git a/test-suite/bugs/closed/3346.v b/test-suite/bugs/closed/3346.v index 638404f2c..09bd78934 100644 --- a/test-suite/bugs/closed/3346.v +++ b/test-suite/bugs/closed/3346.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Monomorphic Inductive paths (A : Type) (a : A) : A -> Type := idpath : paths A a a. (* This should fail with -indices-matter *) Fail Check paths nat O O : Prop. diff --git a/test-suite/bugs/closed/3348.v b/test-suite/bugs/closed/3348.v index d9ac09d8d..904de6896 100644 --- a/test-suite/bugs/closed/3348.v +++ b/test-suite/bugs/closed/3348.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Set Printing Universes. Inductive Empty : Set := . diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index f8113e4c7..555accfd5 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -20,7 +20,7 @@ while it is expected to have type "IsHProp (* Top.17 *) Empty" Defined. Module B. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *) Set Universe Polymorphism. Inductive paths {A} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. diff --git a/test-suite/bugs/closed/3375.v b/test-suite/bugs/closed/3375.v index d7ce02ea8..1e0c8e61f 100644 --- a/test-suite/bugs/closed/3375.v +++ b/test-suite/bugs/closed/3375.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *) +(* -*- mode: coq; coq-prog-args: ("-impredicative-set") -*- *) (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 330 lines to 45 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v index f7ab5f76a..ae8e41e29 100644 --- a/test-suite/bugs/closed/3393.v +++ b/test-suite/bugs/closed/3393.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 8760 lines to 7519 lines, then from 7050 lines to 909 lines, then from 846 lines to 578 lines, then from 497 lines to 392 lines, then from 365 lines to 322 lines, then from 252 lines to 205 lines, then from 215 lines to 204 lines, then from 210 lines to 182 lines, then from 175 lines to 157 lines *) Set Universe Polymorphism. Axiom admit : forall {T}, T. diff --git a/test-suite/bugs/closed/3427.v b/test-suite/bugs/closed/3427.v index 374a53928..9a57ca770 100644 --- a/test-suite/bugs/closed/3427.v +++ b/test-suite/bugs/closed/3427.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 0 lines to 7171 lines, then from 7184 lines to 558 lines, then from 556 lines to 209 lines *) Generalizable All Variables. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3539.v b/test-suite/bugs/closed/3539.v index d258bb31f..b0c4b2370 100644 --- a/test-suite/bugs/closed/3539.v +++ b/test-suite/bugs/closed/3539.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 11678 lines to 11330 lines, then from 10721 lines to 9544 lines, then from 9549 lines to 794 lines, then from 810 lines to 785 lines, then from 628 lines to 246 lines, then from 220 lines to 89 lines, then from 80 lines to 47 lines *) (* coqc version trunk (August 2014) compiled on Aug 22 2014 4:17:28 with OCaml 4.01.0 coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (a67cc6941434124465f20b14a1256f2ede31a60e) *) diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 4b4f81dbc..73709268a 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 3595 lines to 3518 lines, then from 3133 lines to 2950 lines, then from 2911 lines to 415 lines, then from 431 lines to 407 \ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then from 434 lines to 66 lines, then from 163 lines to 48 lines *) (* coqc version trunk (September 2014) compiled on Sep 11 2014 14:48:8 with OCaml 4.01.0 diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index 8687eaab0..179f81e66 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *) (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index a327bbf2a..bb6af6a66 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) +(* -*- coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *) (* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *) diff --git a/test-suite/bugs/closed/3956.v b/test-suite/bugs/closed/3956.v index c19a2d4a0..66dee702a 100644 --- a/test-suite/bugs/closed/3956.v +++ b/test-suite/bugs/closed/3956.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter"); mode: visual-line -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter"); mode: visual-line -*- *) Set Universe Polymorphism. Set Primitive Projections. Close Scope nat_scope. diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index e4d76732a..fc1c504f1 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -1,6 +1,6 @@ Unset Strict Universe Declaration. Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *) (* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *) diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v index 816bc845f..b23684671 100644 --- a/test-suite/bugs/closed/4121.v +++ b/test-suite/bugs/closed/4121.v @@ -1,5 +1,5 @@ Unset Strict Universe Declaration. -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *) (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *) diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v index 60c935459..1ad81345d 100644 --- a/test-suite/bugs/closed/4394.v +++ b/test-suite/bugs/closed/4394.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Require Import Equality List. Inductive Foo (I : Type -> Type) (A : Type) : Type := diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v index 5c23f8404..a89cf0cbc 100644 --- a/test-suite/bugs/closed/4400.v +++ b/test-suite/bugs/closed/4400.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality. Set Printing Universes. Inductive Foo (I : Type -> Type) (A : Type) : Type := diff --git a/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v index a32acf789..56a7b4f6e 100644 --- a/test-suite/bugs/closed/4456.v +++ b/test-suite/bugs/closed/4456.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) (* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *) (* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0 coqtop version 8.5beta3 (November 2015) *) diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index c6fcc24b6..117d6523a 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 1199 lines to 430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, then from 269 lines to 255 lines *) diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index 64c7fd8eb..c3e0da111 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) (* File reduced by coq-bug-finder from original input, then from 1125 lines to 346 lines, then from 360 lines to 346 lines, then from 822 lines to 271 lines, then from 285 lines to 271 lines *) diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 64dd8c304..4ad53bc62 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v index c89a86d63..a59eed2c8 100644 --- a/test-suite/bugs/closed/4656.v +++ b/test-suite/bugs/closed/4656.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Goal True. constructor 1. Qed. diff --git a/test-suite/bugs/closed/4673.v b/test-suite/bugs/closed/4673.v index 1ae508185..10e48db6d 100644 --- a/test-suite/bugs/closed/4673.v +++ b/test-suite/bugs/closed/4673.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) (* File reduced by coq-bug-finder from original input, then from 2407 lines to 22 lines, then from 528 lines to 35 lines, then from 331 lines to 42 lines, then from 56 lines to 42 lines, then from 63 lines to 46 lines, then from 60 lines to 46 lines *) (* coqc version 8.5 (February 2016) compiled on Feb 21 2016 15:26:16 with OCaml 4.02.3 coqtop version 8.5 (February 2016) *) Axiom proof_admitted : False. diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v index f047624c8..2d41828f1 100644 --- a/test-suite/bugs/closed/4722.v +++ b/test-suite/bugs/closed/4722.v @@ -1 +1 @@ -(* -*- coq-prog-args: ("-emacs" "-R" "4722" "Foo") -*- *) +(* -*- coq-prog-args: ("-R" "4722" "Foo") -*- *) diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v index 3854bbffd..cfb4548d2 100644 --- a/test-suite/bugs/closed/4727.v +++ b/test-suite/bugs/closed/4727.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0), (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) -> o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v index a6ebda61c..a90abd71c 100644 --- a/test-suite/bugs/closed/4733.v +++ b/test-suite/bugs/closed/4733.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) (*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) Require Import Coq.Lists.List. Require Import Coq.Vectors.Vector. diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v index d87906f31..33a1d1a50 100644 --- a/test-suite/bugs/closed/4769.v +++ b/test-suite/bugs/closed/4769.v @@ -1,5 +1,5 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *) (* File reduced by coq-bug-finder from original input, then from 156 lines to 41 lines, then from 237 lines to 45 lines, then from 163 lines to 66 lines, then from 342 lines to 121 lines, then from 353 lines to 184 lines, then from 343 lines to 255 lines, then from 435 lines to 322 lines, then from 475 lines to 351 lines, then from 442 lines to 377 lines, then from 505 lines to 410 lines, then from 591 lines to 481 lines, then from 596 lines to 535 lines, then from 647 lines to 570 lines, then from 669 lines to 596 lines, then from 687 lines to 620 lines, then from 728 lines to 652 lines, then from 1384 lines to 683 lines, then from 984 lines to 707 lines, then from 1124 lines to 734 lines, then from 775 lines to 738 lines, then from 950 lines to 763 lines, then from 857 lines to 798 lines, then from 983 lines to 752 lines, then from 1598 lines to 859 lines, then from 873 lines to 859 lines, then from 875 lines to 862 lines, then from 901 lines to 863 lines, then from 1047 lines to 865 lines, then from 929 lines to 871 lines, then from 989 lines to 884 lines, then from 900 lines to 884 lines, then from 884 lines to 751 lines, then from 763 lines to 593 lines, then from 482 lines to 232 lines, then from 416 lines to 227 lines, then from 290 lines to 231 lines, then from 348 lines to 235 lines, then from 249 lines to 235 lines, then from 249 lines to 172 lines, then from 186 lines to 172 lines, then from 140 lines to 113 lines, then from 127 lines to 113 lines *) (* coqc version trunk (June 2016) compiled on Jun 2 2016 10:16:20 with OCaml 4.02.3 coqtop version trunk (June 2016) *) diff --git a/test-suite/bugs/closed/4780.v b/test-suite/bugs/closed/4780.v index 4cec43184..71a51c631 100644 --- a/test-suite/bugs/closed/4780.v +++ b/test-suite/bugs/closed/4780.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top" "-top" "bug_bad_induction_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Top" "-top" "bug_bad_induction_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 1889 lines to 144 lines, then from 158 lines to 144 lines *) (* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 coqtop version 8.5pl1 (April 2016) *) diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v index 9d65840ac..bbb34f465 100644 --- a/test-suite/bugs/closed/4785_compat_85.v +++ b/test-suite/bugs/closed/4785_compat_85.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *) +(* -*- coq-prog-args: ("-compat" "8.5") -*- *) Require Coq.Lists.List Coq.Vectors.Vector. Require Coq.Compat.Coq85. diff --git a/test-suite/bugs/closed/4811.v b/test-suite/bugs/closed/4811.v index a91496262..fe6e65a0f 100644 --- a/test-suite/bugs/closed/4811.v +++ b/test-suite/bugs/closed/4811.v @@ -2,7 +2,7 @@ (* Submitted by Jason Gross *) -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) (* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) (* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 coqtop version 8.5pl1 (April 2016) *) diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v index 904abb228..e411ce62f 100644 --- a/test-suite/bugs/closed/4818.v +++ b/test-suite/bugs/closed/4818.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Prob" "-top" "Product") -*- *) (* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *) (* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3 coqtop version 8.5pl1 (June 2016) *) diff --git a/test-suite/bugs/closed/5193.v b/test-suite/bugs/closed/5193.v new file mode 100644 index 000000000..cc8739afe --- /dev/null +++ b/test-suite/bugs/closed/5193.v @@ -0,0 +1,14 @@ +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Typeclasses eauto := debug. +Set Typeclasses Debug Verbosity 2. + +Inductive Finx(n : nat) : Set := +| Fx1(i : nat)(e : n = S i) +| FxS(i : nat)(f : Finx i)(e : n = S i). + +Context `{Finx_eqdec : forall n, Eqdec (Finx n)}. + +Goal {x : Type & Eqdec x}. + eexists. + try typeclasses eauto 1 with typeclass_instances. diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v index 7254afb42..72722f5f6 100644 --- a/test-suite/bugs/closed/5198.v +++ b/test-suite/bugs/closed/5198.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 286 lines to 27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from diff --git a/test-suite/bugs/closed/5219.v b/test-suite/bugs/closed/5219.v new file mode 100644 index 000000000..f7cec1a0c --- /dev/null +++ b/test-suite/bugs/closed/5219.v @@ -0,0 +1,10 @@ +(* Test surgical use of beta-iota in the type of variables coming from + pattern-matching for refine *) + +Goal forall x : sigT (fun x => x = 1), True. + intro x; refine match x with + | existT _ x' e' => _ + end. + lazymatch goal with + | [ H : _ = _ |- _ ] => idtac + end. diff --git a/test-suite/bugs/closed/5300.v b/test-suite/bugs/closed/5300.v new file mode 100644 index 000000000..18202df50 --- /dev/null +++ b/test-suite/bugs/closed/5300.v @@ -0,0 +1,39 @@ +Module Test1. + + Module Type Foo. + Parameter t : unit. + End Foo. + + Module Bar : Foo. + Module Type Rnd. Definition t' : unit := tt. End Rnd. + Module Rnd_inst : Rnd. Definition t' : unit := tt. End Rnd_inst. + Definition t : unit. + exact Rnd_inst.t'. + Qed. + End Bar. + + Print Assumptions Bar.t. +End Test1. + +Module Test2. + Module Type Foo. + Parameter t1 : unit. + Parameter t2 : unit. + End Foo. + + Module Bar : Foo. + Inductive ind := . + Definition t' : unit := tt. + Definition t1 : unit. + Proof. + exact ((fun (_ : ind -> False) => tt) (fun H => match H with end)). + Qed. + Definition t2 : unit. + Proof. + exact t'. + Qed. + End Bar. + + Print Assumptions Bar.t1. + Print Assumptions Bar.t1. +End Test2. diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v new file mode 100644 index 000000000..9b995f450 --- /dev/null +++ b/test-suite/bugs/closed/5487.v @@ -0,0 +1,9 @@ +(* Was a collision between an ltac pattern variable and an evar *) + +Goal forall n, exists m, n = m :> nat. +Proof. + eexists. + Fail match goal with + | [ |- ?x = ?y ] + => match x with y => idtac end + end. diff --git a/test-suite/bugs/closed/5522.v b/test-suite/bugs/closed/5522.v new file mode 100644 index 000000000..0fae9ede4 --- /dev/null +++ b/test-suite/bugs/closed/5522.v @@ -0,0 +1,7 @@ +(* Checking support for scope delimiters and as clauses in 'pat + applied to notations with binders *) + +Notation "'multifun' x .. y 'in' f" := (fun x => .. (fun y => f) .. ) + (at level 200, x binder, y binder, f at level 200). + +Check multifun '((x, y)%core as z) in (x+y,0)=z. diff --git a/test-suite/bugs/closed/HoTT_coq_012.v b/test-suite/bugs/closed/HoTT_coq_012.v index a3c697f8c..420aaf974 100644 --- a/test-suite/bugs/closed/HoTT_coq_012.v +++ b/test-suite/bugs/closed/HoTT_coq_012.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Definition UU := Type. Inductive toto (B : UU) : UU := c (x : B). diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v index 3f5d7b021..39a7103d1 100644 --- a/test-suite/bugs/closed/HoTT_coq_032.v +++ b/test-suite/bugs/closed/HoTT_coq_032.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *) +(* -*- mode: coq; coq-prog-args: ("-xml") -*- *) Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v index e2bf1dbed..263dec485 100644 --- a/test-suite/bugs/closed/HoTT_coq_053.v +++ b/test-suite/bugs/closed/HoTT_coq_053.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Printing Universes. Set Implicit Arguments. Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v index c68796593..635024e98 100644 --- a/test-suite/bugs/closed/HoTT_coq_054.v +++ b/test-suite/bugs/closed/HoTT_coq_054.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) Inductive Empty : Prop := . Inductive paths {A : Type} (a : A) : A -> Type := diff --git a/test-suite/bugs/closed/HoTT_coq_055.v b/test-suite/bugs/closed/HoTT_coq_055.v index a25098771..561b7e557 100644 --- a/test-suite/bugs/closed/HoTT_coq_055.v +++ b/test-suite/bugs/closed/HoTT_coq_055.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Inductive Empty : Prop := . diff --git a/test-suite/bugs/closed/HoTT_coq_059.v b/test-suite/bugs/closed/HoTT_coq_059.v index 9c7e394dc..2e6c735cf 100644 --- a/test-suite/bugs/closed/HoTT_coq_059.v +++ b/test-suite/bugs/closed/HoTT_coq_059.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Inductive eq {A} (x : A) : A -> Type := eq_refl : eq x x. diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v index 90d1d1830..e01f73f1b 100644 --- a/test-suite/bugs/closed/HoTT_coq_062.v +++ b/test-suite/bugs/closed/HoTT_coq_062.v @@ -1,6 +1,6 @@ Unset Strict Universe Declaration. Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *) Set Universe Polymorphism. Definition admit {T} : T. diff --git a/test-suite/bugs/closed/HoTT_coq_097.v b/test-suite/bugs/closed/HoTT_coq_097.v index 38e8007b6..f2b2e57b9 100644 --- a/test-suite/bugs/closed/HoTT_coq_097.v +++ b/test-suite/bugs/closed/HoTT_coq_097.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Set Printing Universes. Inductive Empty : Set := . diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index 7c1ab8dc2..fa4072a8f 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *) (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *) Require Import Coq.Init.Logic. diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v index b6c0da76b..ea4bcd8b4 100644 --- a/test-suite/bugs/closed/HoTT_coq_108.v +++ b/test-suite/bugs/closed/HoTT_coq_108.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *) (* File reduced by coq-bug-finder from 139 lines to 124 lines. *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index 6ee6e6532..cd9cad406 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") *) (* File reduced by coq-bug-finder from original input, then from 4988 lines to 856 lines, then from 648 lines to 398 lines, then from 401 lines to 332 lines, then from 287 lines to 250 lines, then from 257 lines to 241 lines, then from 223 lines to 175 lines *) Set Universe Polymorphism. Set Asymmetric Patterns. diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v index 4530548b8..4541f13d0 100644 --- a/test-suite/bugs/opened/4803.v +++ b/test-suite/bugs/opened/4803.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) (*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) Require Import Coq.Lists.List. Require Import Coq.Vectors.Vector. diff --git a/test-suite/kernel/inds.mv b/test-suite/kernel/inds.mv deleted file mode 100644 index bd1cc49f8..000000000 --- a/test-suite/kernel/inds.mv +++ /dev/null @@ -1,3 +0,0 @@ -Inductive [] nat : Set := O : nat | S : nat->nat. -Check Construct nat 0 1. -Check Construct nat 0 2. diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v deleted file mode 100644 index a64db4dab..000000000 --- a/test-suite/misc/berardi_test.v +++ /dev/null @@ -1,153 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This file formalizes Berardi's paradox which says that in - the calculus of constructions, excluded middle (EM) and axiom of - choice (AC) imply proof irrelevance (PI). - Here, the axiom of choice is not necessary because of the use - of inductive types. -<< -@article{Barbanera-Berardi:JFP96, - author = {F. Barbanera and S. Berardi}, - title = {Proof-irrelevance out of Excluded-middle and Choice - in the Calculus of Constructions}, - journal = {Journal of Functional Programming}, - year = {1996}, - volume = {6}, - number = {3}, - pages = {519-525} -} ->> *) - -Set Implicit Arguments. - -Section Berardis_paradox. - -(** Excluded middle *) -Hypothesis EM : forall P:Prop, P \/ ~ P. - -(** Conditional on any proposition. *) -Definition IFProp (P B:Prop) (e1 e2:P) := - match EM B with - | or_introl _ => e1 - | or_intror _ => e2 - end. - -(** Axiom of choice applied to disjunction. - Provable in Coq because of dependent elimination. *) -Lemma AC_IF : - forall (P B:Prop) (e1 e2:P) (Q:P -> Prop), - (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2). -Proof. -intros P B e1 e2 Q p1 p2. -unfold IFProp. -case (EM B); assumption. -Qed. - - -(** We assume a type with two elements. They play the role of booleans. - The main theorem under the current assumptions is that [T=F] *) -Variable Bool : Prop. -Variable T : Bool. -Variable F : Bool. - -(** The powerset operator *) -Definition pow (P:Prop) := P -> Bool. - - -(** A piece of theory about retracts *) -Section Retracts. - -Variables A B : Prop. - -Record retract : Prop := - {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. - -Record retract_cond : Prop := - {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. - - -(** The dependent elimination above implies the axiom of choice: *) -Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. -Proof. -intros r. -case r; simpl. -trivial. -Qed. - -End Retracts. - -(** This lemma is basically a commutation of implication and existential - quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) - which is provable in classical logic ( => is already provable in - intuitionnistic logic). *) - -Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). -Proof. -intros A B. -destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. - exists f0 g0; trivial. - exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; - destruct hf; auto. -Qed. - - -(** The paradoxical set *) -Definition U := forall P:Prop, pow P. - -(** Bijection between [U] and [(pow U)] *) -Definition f (u:U) : pow U := u U. - -Definition g (h:pow U) : U := - fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h). - -(** We deduce that the powerset of [U] is a retract of [U]. - This lemma is stated in Berardi's article, but is not used - afterwards. *) -Lemma retract_pow_U_U : retract (pow U) U. -Proof. -exists g f. -intro a. -unfold f, g; simpl. -apply AC. -exists (fun x:pow U => x) (fun x:pow U => x). -trivial. -Qed. - -(** Encoding of Russel's paradox *) - -(** The boolean negation. *) -Definition Not_b (b:Bool) := IFProp (b = T) F T. - -(** the set of elements not belonging to itself *) -Definition R : U := g (fun u:U => Not_b (u U u)). - - -Lemma not_has_fixpoint : R R = Not_b (R R). -Proof. -unfold R at 1. -unfold g. -rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). -trivial. -exists (fun x:pow U => x) (fun x:pow U => x); trivial. -Qed. - - -Theorem classical_proof_irrelevence : T = F. -Proof. -generalize not_has_fixpoint. -unfold Not_b. -apply AC_IF. -intros is_true is_false. -elim is_true; elim is_false; trivial. - -intros not_true is_true. -elim not_true; trivial. -Qed. - -End Berardis_paradox. diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh new file mode 100755 index 000000000..1e2afb754 --- /dev/null +++ b/test-suite/misc/deps-checksum.sh @@ -0,0 +1,5 @@ +rm -f misc/deps/*/*.vo +$coqc -R misc/deps/A A misc/deps/A/A.v +$coqc -R misc/deps/B A misc/deps/B/A.v +$coqc -R misc/deps/B A misc/deps/B/B.v +$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh new file mode 100755 index 000000000..375b706f0 --- /dev/null +++ b/test-suite/misc/deps-order.sh @@ -0,0 +1,20 @@ +# Check that both coqdep and coqtop/coqc supports -R +# Check that both coqdep and coqtop/coqc takes the later -R +# See bugs 2242, 2337, 2339 +rm -f misc/deps/*/*.vo +tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` +$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput +diff -u misc/deps/deps.out $tmpoutput 2>&1 +R=$? +times +$coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 +$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1 +$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1 +S=$? +if [ $R = 0 -a $S = 0 ]; then + printf "coqdep and coqtop agree\n" + exit 0 +else + printf "coqdep and coqtop disagree\n" + exit 1 +fi diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh new file mode 100755 index 000000000..cea1de862 --- /dev/null +++ b/test-suite/misc/exitstatus.sh @@ -0,0 +1,7 @@ +$coqtop -load-vernac-source misc/exitstatus/illtyped.v +N=$? +$coqc misc/exitstatus/illtyped.v +P=$? +printf "On ill-typed input, coqtop returned $N.\n" +printf "On ill-typed input, coqc returned $P.\n" +if [ $N = 1 -a $P = 1 ]; then exit 0; else exit 1; fi diff --git a/test-suite/misc/exitstatus/illtyped.v b/test-suite/misc/exitstatus/illtyped.v new file mode 100644 index 000000000..df6bbb389 --- /dev/null +++ b/test-suite/misc/exitstatus/illtyped.v @@ -0,0 +1 @@ +Check S S. diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh new file mode 100755 index 000000000..c822d0eb3 --- /dev/null +++ b/test-suite/misc/printers.sh @@ -0,0 +1,3 @@ +printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound +if [ $? = 0 ]; then exit 1; else exit 0; fi + diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh new file mode 100755 index 000000000..d87a86035 --- /dev/null +++ b/test-suite/misc/universes.sh @@ -0,0 +1,8 @@ +# Sort universes for the whole standard library +EXPECTED_UNIVERSES=4 # Prop is not counted +$coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1 +$coqc -R misc/universes Universes misc/universes/universes 2>&1 +mv universes.txt misc/universes +N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l` +printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES +if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v index 6611db70e..1e9e91979 100644 --- a/test-suite/output-modulo-time/ltacprof.v +++ b/test-suite/output-modulo-time/ltacprof.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *) +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) Ltac sleep' := do 100 (do 100 (do 100 idtac)). Ltac sleep := sleep'. diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index 50131470e..3dad6271a 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-profile-ltac") -*- *) Require Coq.ZArith.BinInt. Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). diff --git a/test-suite/output/CompactContexts.out b/test-suite/output/CompactContexts.out new file mode 100644 index 000000000..9d1d19877 --- /dev/null +++ b/test-suite/output/CompactContexts.out @@ -0,0 +1,7 @@ +1 subgoal + + hP1 : True + a : nat b : list nat h : forall x : nat, {y : nat | y > x} + h2 : True + ============================ + False diff --git a/test-suite/output/CompactContexts.v b/test-suite/output/CompactContexts.v new file mode 100644 index 000000000..07588d34f --- /dev/null +++ b/test-suite/output/CompactContexts.v @@ -0,0 +1,5 @@ +Set Printing Compact Contexts. + +Lemma f (hP1:True) (a:nat) (b:list nat) (h:forall (x:nat) , { y:nat | y > x}) (h2:True): False. +Show. +Abort.
\ No newline at end of file diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v index e69e23276..b2e3c3e92 100644 --- a/test-suite/output/ErrorInModule.v +++ b/test-suite/output/ErrorInModule.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) Module M. Definition foo := nonexistent. End M. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v index 3036f8f05..505c5ce37 100644 --- a/test-suite/output/ErrorInSection.v +++ b/test-suite/output/ErrorInSection.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) Section S. Definition foo := nonexistent. End S. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 49c465b6c..52fe98ac0 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1868,3 +1868,8 @@ Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y := Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end. Check match niln in listn O return O=O with niln => eq_refl end. + +(* A test about nested "as" clauses *) +(* (was failing up to May 2017) *) + +Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end. diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v index db6348fa1..732a024fc 100644 --- a/test-suite/success/Compat84.v +++ b/test-suite/success/Compat84.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Goal True. solve [ constructor 1 ]. Undo. diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index dd5aa81d1..855f26698 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -2,3 +2,26 @@ Scheme Induction for eq Sort Prop. Check eq_ind_dep. + +(* This was broken in v8.5 *) + +Set Rewriting Schemes. +Inductive myeq A (a:A) : A -> Prop := myrefl : myeq A a a. +Unset Rewriting Schemes. + +Check myeq_rect. +Check myeq_ind. +Check myeq_rec. +Check myeq_congr. +Check myeq_sym_internal. +Check myeq_rew. +Check myeq_rew_dep. +Check myeq_rew_fwd_dep. +Check myeq_rew_r. +Check internal_myeq_sym_involutive. +Check myeq_rew_r_dep. +Check myeq_rew_fwd_r_dep. + +Set Rewriting Schemes. +Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true. +Unset Rewriting Schemes. diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v new file mode 100644 index 000000000..fafe27292 --- /dev/null +++ b/test-suite/success/boundvars.v @@ -0,0 +1,14 @@ +(* An example showing a bug in the detection of free variables *) +(* "x" is not free in the common type of "x" and "y" *) + +Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x. + +(* An example showing a bug in the detection of bound variables *) + +Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl. +intro. +match goal with +|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end. +intro. +Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *) +Abort. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index ce9099059..1d35f1ef6 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,3 +317,23 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. + +(* A variant of #2602 which was wrongly succeeding because "a", bound to + "?m", was then internally turned into a "_" in the second matching *) + +Goal exists m, S m > 0. +eexists. +Fail match goal with + | |- context [ S ?a ] => + match goal with + | |- S a > a => idtac + end +end. +Abort. + +(* Test evar syntax *) + +Goal True. +evar (0=0). +Abort. + diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 878875bd9..66ff55edc 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw. Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl. -End Hurkens'.
\ No newline at end of file +End Hurkens'. + +Module Anonymous. + Set Universe Polymorphism. + + Definition defaultid := (fun x => x) : Type -> Type. + Definition collapseid := defaultid@{_ _}. + Check collapseid@{_}. + + Definition anonid := (fun x => x) : Type -> Type@{_}. + Check anonid@{_}. + + Definition defaultalg := (fun x : Type => x) (Type : Type). + Definition usedefaultalg := defaultalg@{_ _ _}. + Check usedefaultalg@{_ _}. + + Definition anonalg := (fun x : Type@{_} => x) (Type : Type). + Check anonalg@{_ _}. + + Definition unrelated@{i j} := nat. + Definition useunrelated := unrelated@{_ _}. + Check useunrelated@{_ _}. + + Definition inthemiddle@{i j k} := + let _ := defaultid@{i j} in + anonalg@{k j}. + (* i <= j < k *) + Definition collapsethemiddle := inthemiddle@{i _ j}. + Check collapsethemiddle@{_ _}. + +End Anonymous. diff --git a/test-suite/success/transparent_abstract.v b/test-suite/success/transparent_abstract.v new file mode 100644 index 000000000..ff4509c4a --- /dev/null +++ b/test-suite/success/transparent_abstract.v @@ -0,0 +1,21 @@ +Class by_transparent_abstract {T} (x : T) := make_by_transparent_abstract : T. +Hint Extern 0 (@by_transparent_abstract ?T ?x) => change T; transparent_abstract exact_no_check x : typeclass_instances. + +Goal True /\ True. +Proof. + split. + transparent_abstract exact I using foo. + let x := (eval hnf in foo) in constr_eq x I. + let x := constr:(ltac:(constructor) : True) in + let T := type of x in + let x := constr:(_ : by_transparent_abstract x) in + let x := (eval cbv delta [by_transparent_abstract] in (let y : T := x in y)) in + pose x as x'. + simpl in x'. + let v := eval cbv [x'] in x' in tryif constr_eq v I then fail 0 else idtac. + hnf in x'. + let v := eval cbv [x'] in x' in tryif constr_eq v I then idtac else fail 0. + exact x'. +Defined. +Check eq_refl : I = foo. +Eval compute in foo. diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 296686e16..6f7498d65 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -188,3 +188,14 @@ Proof. apply idpath. apply idpath. Defined. + +(* An example where it is necessary to evar-normalize the instance of + an evar to evaluate if it is a pattern *) + +Check + let a := ?[P] in + fun (H : forall y (P : nat -> Prop), y = 0 -> P y) + x (p:x=0) => + H ?[y] a p : x = 0. +(* We have to solve "?P ?y[x] == x = 0" knowing from + "p : (x=0) == (?y[x] = 0)" that "?y := x" *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9ae9dde28..3eefe9a84 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -609,6 +609,11 @@ Proof. destruct 1; auto. Qed. +Lemma inhabited_covariant (A B : Type) : (A -> B) -> inhabited A -> inhabited B. +Proof. + intros f [x];exact (inhabits (f x)). +Qed. + (** Declaration of stepl and stepr for eq and iff *) Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index c58d23dad..e71a8774e 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -23,4 +23,4 @@ Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". Declare ML Module "recdef_plugin". (* Default substrings not considered by queries like SearchAbout *) -Add Search Blacklist "_subproof" "Private_". +Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2cc2ecbc2..43a441fc5 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -207,6 +207,17 @@ Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). Proof. destruct p; reflexivity. Defined. +(** [exists x : A, B] is equivalent to [inhabited {x : A | B}] *) +Lemma exists_to_inhabited_sig {A P} : (exists x : A, P x) -> inhabited {x : A | P x}. +Proof. + intros [x y]. exact (inhabits (exist _ x y)). +Qed. + +Lemma inhabited_sig_to_exists {A P} : inhabited {x : A | P x} -> exists x : A, P x. +Proof. + intros [[x y]];exists x;exact y. +Qed. + (** [sumbool] is a boolean type equipped with the justification of their value *) diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 5d1e87ae0..7a846cd1b 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -236,3 +236,10 @@ Tactic Notation "clear" "dependent" hyp(h) := Tactic Notation "revert" "dependent" hyp(h) := generalize dependent h. + +(** Provide an error message for dependent induction that reports an import is +required to use it. Importing Coq.Program.Equality will shadow this notation +with the actual [dependent induction] tactic. *) + +Tactic Notation "dependent" "induction" ident(H) := + fail "To use dependent induction, first [Require Import Coq.Program.Equality.]". diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 07e8b6ef8..116897f4c 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -8,94 +8,9 @@ (************************************************************************) (** Some facts and definitions concerning choice and description in - intuitionistic logic. - -We investigate the relations between the following choice and -description principles - -- AC_rel = relational form of the (non extensional) axiom of choice - (a "set-theoretic" axiom of choice) -- AC_fun = functional form of the (non extensional) axiom of choice - (a "type-theoretic" axiom of choice) -- DC_fun = functional form of the dependent axiom of choice -- ACw_fun = functional form of the countable axiom of choice -- AC! = functional relation reification - (known as axiom of unique choice in topos theory, - sometimes called principle of definite description in - the context of constructive type theory, sometimes - called axiom of no choice) - -- AC_fun_repr = functional choice of a representative in an equivalence class -- AC_fun_setoid_gen = functional form of the general form of the (so-called - extensional) axiom of choice over setoids -- AC_fun_setoid = functional form of the (so-called extensional) axiom of - choice from setoids -- AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of - choice from setoids on locally compatible relations - -- GAC_rel = guarded relational form of the (non extensional) axiom of choice -- GAC_fun = guarded functional form of the (non extensional) axiom of choice -- GAC! = guarded functional relation reification - -- OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice -- OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice - (called AC* in Bell [[Bell]]) -- OAC! - -- ID_iota = intuitionistic definite description -- ID_epsilon = intuitionistic indefinite description - -- D_iota = (weakly classical) definite description principle -- D_epsilon = (weakly classical) indefinite description principle - -- PI = proof irrelevance -- IGP = independence of general premises - (an unconstrained generalisation of the constructive principle of - independence of premises) -- Drinker = drinker's paradox (small form) - (called Ex in Bell [[Bell]]) -- EM = excluded-middle - -- Ext_pred_repr = choice of a representative among extensional predicates -- Ext_pred = extensionality of predicates -- Ext_fun_prop_repr = choice of a representative among extensional functions to Prop - -We let also - -- IPL_2 = 2nd-order impredicative minimal predicate logic (with ex. quant.) -- IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) -- IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.) - -with no prerequisite on the non-emptiness of domains - -Table of contents - -1. Definitions - -2. IPL_2^2 |- AC_rel + AC! = AC_fun - -3.1. typed IPL_2 + Sigma-types + PI |- AC_rel = GAC_rel and IPL_2 |- AC_rel + IGP -> GAC_rel and IPL_2 |- GAC_rel = OAC_rel - -3.2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker - -3.3. D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker - -4. Derivability of choice for decidable relations with well-ordered codomain - -5. Equivalence of choices on dependent or non dependent functional types - -6. Non contradiction of constructive descriptions wrt functional choices - -7. Definite description transports classical logic to the computational world - -8. Choice -> Dependent choice -> Countable choice - -9.1. AC_fun_ext = AC_fun + Ext_fun_repr + EM - -9.2. AC_fun_ext = AC_fun + Ext_prop_fun_repr + PI - -References: - + intuitionistic logic. *) +(** * References: *) +(** [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, unpublished. @@ -133,47 +48,75 @@ Variable P:A->Prop. (** ** Constructive choice and description *) -(** AC_rel *) +(** AC_rel = relational form of the (non extensional) axiom of choice + (a "set-theoretic" axiom of choice) *) Definition RelationalChoice_on := forall R:A->B->Prop, (forall x : A, exists y : B, R x y) -> (exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y). -(** AC_fun *) +(** AC_fun = functional form of the (non extensional) axiom of choice + (a "type-theoretic" axiom of choice) *) (* Note: This is called Type-Theoretic Description Axiom (TTDA) in [[Werner97]] (using a non-standard meaning of "description"). This is called intensional axiom of choice (AC_int) in [[Carlström04]] *) +Definition FunctionalChoice_on_rel (R:A->B->Prop) := + (forall x:A, exists y : B, R x y) -> + exists f : A -> B, (forall x:A, R x (f x)). + Definition FunctionalChoice_on := forall R:A->B->Prop, (forall x : A, exists y : B, R x y) -> (exists f : A->B, forall x : A, R x (f x)). -(** DC_fun *) +(** AC_fun_dep = functional form of the (non extensional) axiom of + choice, with dependent functions *) +Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) := + forall R:forall x:A, B x -> Prop, + (forall x:A, exists y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). + +(** AC_trunc = axiom of choice for propositional truncations + (truncation and quantification commute) *) +Definition InhabitedForallCommute_on (A : Type) (B : A -> Type) := + (forall x, inhabited (B x)) -> inhabited (forall x, B x). + +(** DC_fun = functional form of the dependent axiom of choice *) Definition FunctionalDependentChoice_on := forall (R:A->A->Prop), (forall x, exists y, R x y) -> forall x0, (exists f : nat -> A, f 0 = x0 /\ forall n, R (f n) (f (S n))). -(** ACw_fun *) +(** ACw_fun = functional form of the countable axiom of choice *) Definition FunctionalCountableChoice_on := forall (R:nat->A->Prop), (forall n, exists y, R n y) -> (exists f : nat -> A, forall n, R n (f n)). -(** AC! or Functional Relation Reification (known as Axiom of Unique Choice - in topos theory; also called principle of definite description *) +(** AC! = functional relation reification + (known as axiom of unique choice in topos theory, + sometimes called principle of definite description in + the context of constructive type theory, sometimes + called axiom of no choice) *) Definition FunctionalRelReification_on := forall R:A->B->Prop, (forall x : A, exists! y : B, R x y) -> (exists f : A->B, forall x : A, R x (f x)). -(** AC_fun_repr *) +(** AC_dep! = functional relation reification, with dependent functions + see AC! *) +Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := + forall (R:forall x:A, B x -> Prop), + (forall x:A, exists! y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). + +(** AC_fun_repr = functional choice of a representative in an equivalence class *) (* Note: This is called Type-Theoretic Choice Axiom (TTCA) in [[Werner97]] (by reference to the extensional set-theoretic @@ -187,7 +130,8 @@ Definition RepresentativeFunctionalChoice_on := (Equivalence R) -> (exists f : A->A, forall x : A, (R x (f x)) /\ forall x', R x x' -> f x = f x'). -(** AC_fun_setoid *) +(** AC_fun_setoid = functional form of the (so-called extensional) axiom of + choice from setoids *) Definition SetoidFunctionalChoice_on := forall R : A -> A -> Prop, @@ -197,7 +141,8 @@ Definition SetoidFunctionalChoice_on := (forall x, exists y, T x y) -> exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). -(** AC_fun_setoid_gen *) +(** AC_fun_setoid_gen = functional form of the general form of the (so-called + extensional) axiom of choice over setoids *) (* Note: This is called extensional axiom of choice (AC_ext) in [[Carlström04]]. *) @@ -213,7 +158,8 @@ Definition GeneralizedSetoidFunctionalChoice_on := exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> S (f x) (f x')). -(** AC_fun_setoid_simple *) +(** AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of + choice from setoids on locally compatible relations *) Definition SimpleSetoidFunctionalChoice_on A B := forall R : A -> A -> Prop, @@ -222,19 +168,19 @@ Definition SimpleSetoidFunctionalChoice_on A B := (forall x, exists y, forall x', R x x' -> T x' y) -> exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). -(** ID_epsilon (constructive version of indefinite description; - combined with proof-irrelevance, it may be connected to - Carlström's type theory with a constructive indefinite description - operator) *) +(** ID_epsilon = constructive version of indefinite description; + combined with proof-irrelevance, it may be connected to + Carlström's type theory with a constructive indefinite description + operator *) Definition ConstructiveIndefiniteDescription_on := forall P:A->Prop, (exists x, P x) -> { x:A | P x }. -(** ID_iota (constructive version of definite description; combined - with proof-irrelevance, it may be connected to Carlström's and - Stenlund's type theory with a constructive definite description - operator) *) +(** ID_iota = constructive version of definite description; + combined with proof-irrelevance, it may be connected to + Carlström's and Stenlund's type theory with a + constructive definite description operator) *) Definition ConstructiveDefiniteDescription_on := forall P:A->Prop, @@ -242,7 +188,7 @@ Definition ConstructiveDefiniteDescription_on := (** ** Weakly classical choice and description *) -(** GAC_rel *) +(** GAC_rel = guarded relational form of the (non extensional) axiom of choice *) Definition GuardedRelationalChoice_on := forall P : A->Prop, forall R : A->B->Prop, @@ -250,7 +196,7 @@ Definition GuardedRelationalChoice_on := (exists R' : A->B->Prop, subrelation R' R /\ forall x, P x -> exists! y, R' x y). -(** GAC_fun *) +(** GAC_fun = guarded functional form of the (non extensional) axiom of choice *) Definition GuardedFunctionalChoice_on := forall P : A->Prop, forall R : A->B->Prop, @@ -258,7 +204,7 @@ Definition GuardedFunctionalChoice_on := (forall x : A, P x -> exists y : B, R x y) -> (exists f : A->B, forall x, P x -> R x (f x)). -(** GFR_fun *) +(** GAC! = guarded functional relation reification *) Definition GuardedFunctionalRelReification_on := forall P : A->Prop, forall R : A->B->Prop, @@ -266,27 +212,28 @@ Definition GuardedFunctionalRelReification_on := (forall x : A, P x -> exists! y : B, R x y) -> (exists f : A->B, forall x : A, P x -> R x (f x)). -(** OAC_rel *) +(** OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice *) Definition OmniscientRelationalChoice_on := forall R : A->B->Prop, exists R' : A->B->Prop, subrelation R' R /\ forall x : A, (exists y : B, R x y) -> exists! y, R' x y. -(** OAC_fun *) +(** OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice + (called AC* in Bell [[Bell]]) *) Definition OmniscientFunctionalChoice_on := forall R : A->B->Prop, inhabited B -> exists f : A->B, forall x : A, (exists y : B, R x y) -> R x (f x). -(** D_epsilon *) +(** D_epsilon = (weakly classical) indefinite description principle *) Definition EpsilonStatement_on := forall P:A->Prop, inhabited A -> { x:A | (exists x, P x) -> P x }. -(** D_iota *) +(** D_iota = (weakly classical) definite description principle *) Definition IotaStatement_on := forall P:A->Prop, @@ -300,14 +247,20 @@ Notation RelationalChoice := (forall A B : Type, RelationalChoice_on A B). Notation FunctionalChoice := (forall A B : Type, FunctionalChoice_on A B). -Definition FunctionalDependentChoice := +Notation DependentFunctionalChoice := + (forall A (B:A->Type), DependentFunctionalChoice_on B). +Notation InhabitedForallCommute := + (forall A (B : A -> Type), InhabitedForallCommute_on B). +Notation FunctionalDependentChoice := (forall A : Type, FunctionalDependentChoice_on A). -Definition FunctionalCountableChoice := +Notation FunctionalCountableChoice := (forall A : Type, FunctionalCountableChoice_on A). Notation FunctionalChoiceOnInhabitedSet := (forall A B : Type, inhabited B -> FunctionalChoice_on A B). Notation FunctionalRelReification := (forall A B : Type, FunctionalRelReification_on A B). +Notation DependentFunctionalRelReification := + (forall A (B:A->Type), DependentFunctionalRelReification_on B). Notation RepresentativeFunctionalChoice := (forall A : Type, RepresentativeFunctionalChoice_on A). Notation SetoidFunctionalChoice := @@ -341,38 +294,87 @@ Notation EpsilonStatement := (** Subclassical schemes *) +(** PI = proof irrelevance *) Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. +(** IGP = independence of general premises + (an unconstrained generalisation of the constructive principle of + independence of premises) *) Definition IndependenceOfGeneralPremises := forall (A:Type) (P:A -> Prop) (Q:Prop), inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x. +(** Drinker = drinker's paradox (small form) + (called Ex in Bell [[Bell]]) *) Definition SmallDrinker'sParadox := forall (A:Type) (P:A -> Prop), inhabited A -> exists x, (exists x, P x) -> P x. +(** EM = excluded-middle *) Definition ExcludedMiddle := forall P:Prop, P \/ ~ P. (** Extensional schemes *) +(** Ext_prop_repr = choice of a representative among extensional propositions *) Local Notation ExtensionalPropositionRepresentative := (forall (A:Type), exists h : Prop -> Prop, forall P : Prop, (P <-> h P) /\ forall Q, (P <-> Q) -> h P = h Q). +(** Ext_pred_repr = choice of a representative among extensional predicates *) Local Notation ExtensionalPredicateRepresentative := (forall (A:Type), exists h : (A->Prop) -> (A->Prop), forall (P : A -> Prop), (forall x, P x <-> h P x) /\ forall Q, (forall x, P x <-> Q x) -> h P = h Q). +(** Ext_fun_repr = choice of a representative among extensional functions *) Local Notation ExtensionalFunctionRepresentative := (forall (A B:Type), exists h : (A->B) -> (A->B), forall (f : A -> B), (forall x, f x = h f x) /\ forall g, (forall x, f x = g x) -> h f = h g). +(** We let also + +- IPL_2 = 2nd-order impredicative minimal predicate logic (with ex. quant.) +- IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) +- IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.) + +with no prerequisite on the non-emptiness of domains +*) + +(**********************************************************************) +(** * Table of contents *) + +(* This is very fragile. *) +(** +1. Definitions + +2. IPL_2^2 |- AC_rel + AC! = AC_fun + +3.1. typed IPL_2 + Sigma-types + PI |- AC_rel = GAC_rel and IPL_2 |- AC_rel + IGP -> GAC_rel and IPL_2 |- GAC_rel = OAC_rel + +3.2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker + +3.3. D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker + +4. Derivability of choice for decidable relations with well-ordered codomain + +5. AC_fun = AC_fun_dep = AC_trunc + +6. Non contradiction of constructive descriptions wrt functional choices + +7. Definite description transports classical logic to the computational world + +8. Choice -> Dependent choice -> Countable choice + +9.1. AC_fun_setoid = AC_fun + Ext_fun_repr + EM + +9.2. AC_fun_setoid = AC_fun + Ext_pred_repr + PI + *) + (**********************************************************************) (** * AC_rel + AC! = AC_fun @@ -400,9 +402,6 @@ Proof. apply HR'R; assumption. Qed. -Notation description_rel_choice_imp_funct_choice := - functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6"). - Lemma fun_choice_imp_rel_choice : forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B. Proof. @@ -416,8 +415,6 @@ Proof. trivial. Qed. -Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6"). - Lemma fun_choice_imp_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B. Proof. @@ -431,8 +428,6 @@ Proof. exists f; exact H0. Qed. -Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6"). - Corollary fun_choice_iff_rel_choice_and_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B. @@ -444,8 +439,6 @@ Proof. intros [H H0]; exact (functional_rel_reification_and_rel_choice_imp_fun_choice H0 H). Qed. -Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := - fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6"). (**********************************************************************) (** * Connection between the guarded, non guarded and omniscient choices *) @@ -687,10 +680,6 @@ Qed. Require Import Wf_nat. Require Import Decidable. -Definition FunctionalChoice_on_rel (A B:Type) (R:A->B->Prop) := - (forall x:A, exists y : B, R x y) -> - exists f : A -> B, (forall x:A, R x (f x)). - Lemma classical_denumerable_description_imp_fun_choice : forall A:Type, FunctionalRelReification_on A nat -> @@ -712,18 +701,10 @@ Proof. Qed. (**********************************************************************) -(** * Choice on dependent and non dependent function types are equivalent *) +(** * AC_fun = AC_fun_dep = AC_trunc *) (** ** Choice on dependent and non dependent function types are equivalent *) -Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) := - forall R:forall x:A, B x -> Prop, - (forall x:A, exists y : B x, R x y) -> - (exists f : (forall x:A, B x), forall x:A, R x (f x)). - -Notation DependentFunctionalChoice := - (forall A (B:A->Type), DependentFunctionalChoice_on B). - (** The easy part *) Theorem dep_non_dep_functional_choice : @@ -760,15 +741,34 @@ Proof. destruct Heq using eq_indd; trivial. Qed. -(** ** Reification of dependent and non dependent functional relation are equivalent *) +(** ** Functional choice and truncation choice are equivalent *) -Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := - forall (R:forall x:A, B x -> Prop), - (forall x:A, exists! y : B x, R x y) -> - (exists f : (forall x:A, B x), forall x:A, R x (f x)). +Theorem functional_choice_to_inhabited_forall_commute : + FunctionalChoice -> InhabitedForallCommute. +Proof. + intros choose0 A B Hinhab. + pose proof (non_dep_dep_functional_choice choose0) as choose;clear choose0. + assert (Hexists : forall x, exists _ : B x, True). + { intros x;apply inhabited_sig_to_exists. + refine (inhabited_covariant _ (Hinhab x)). + intros y;exists y;exact I. } + apply choose in Hexists. + destruct Hexists as [f _]. + exact (inhabits f). +Qed. -Notation DependentFunctionalRelReification := - (forall A (B:A->Type), DependentFunctionalRelReification_on B). +Theorem inhabited_forall_commute_to_functional_choice : + InhabitedForallCommute -> FunctionalChoice. +Proof. + intros choose A B R Hexists. + assert (Hinhab : forall x, inhabited {y : B | R x y}). + { intros x;apply exists_to_inhabited_sig;trivial. } + apply choose in Hinhab. destruct Hinhab as [f]. + exists (fun x => proj1_sig (f x)). + exact (fun x => proj2_sig (f x)). +Qed. + +(** ** Reification of dependent and non dependent functional relation are equivalent *) (** The easy part *) @@ -1304,3 +1304,15 @@ Proof. apply repr_fun_choice_imp_excluded_middle. now apply setoid_fun_choice_imp_repr_fun_choice. Qed. + +(**********************************************************************) +(** * Compatibility notations *) +Notation description_rel_choice_imp_funct_choice := + functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6"). + +Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6"). + +Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := + fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6"). + +Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6"). diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index f85222dfb..d811f04ef 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -86,7 +86,7 @@ Module KeyDecidableType(D:DecidableType). Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. - intros; apply InA_eqA with p; auto with *. + intros; apply InA_eqA with p; auto using eqk_equiv. Qed. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). @@ -109,7 +109,7 @@ Module KeyDecidableType(D:DecidableType). Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 0064aebda..93b25e2ed 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -544,13 +544,6 @@ let add_rec_dir_no_import add_file phys_dir log_dir = let add_rec_dir_import add_file phys_dir log_dir = add_directory true (add_file true) phys_dir log_dir -(** -R semantic but only on immediate capitalized subdirs *) - -let add_rec_uppercase_subdirs add_file phys_dir log_dir = - process_subdirectories (fun phys_dir f -> - add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f])) - phys_dir - (** -I semantic: do not go in subdirs. *) let add_caml_dir phys_dir = add_directory false add_caml_known phys_dir [] diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 633c474ad..10da0240d 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -64,8 +64,5 @@ val add_rec_dir_no_import : val add_rec_dir_import : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit -val add_rec_uppercase_subdirs : - (bool -> string -> string list -> string -> unit) -> string -> string list -> unit - val treat_file : dir -> string -> unit val error_cannot_parse : string -> int * int -> 'a diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 9a4f476bd..a80599cd5 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -173,12 +173,13 @@ let print_error_for_buffer ?loc lvl msg buf = then Topfmt.emacs_logger ?pre_hdr lvl msg else Topfmt.std_logger ?pre_hdr lvl msg +(* let print_toplevel_parse_error (e, info) buf = let loc = Loc.get_loc info in let lvl = Feedback.Error in let msg = CErrors.iprint (e, info) in print_error_for_buffer ?loc lvl msg buf - +*) end (*s The Coq prompt is the name of the focused proof, if any, and "Coq" @@ -260,7 +261,10 @@ let read_sentence sid input = with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); - TopErr.print_toplevel_parse_error reraise top_buffer; + (* The caller of read_sentence does the error printing now, this + should be re-enabled once we rely on the feedback error + printer again *) + (* TopErr.print_toplevel_parse_error reraise top_buffer; *) Exninfo.iraise reraise (** Coqloop Console feedback handler *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c3a755860..8f50bfb3d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -247,6 +247,7 @@ let set_emacs () = if not (Option.is_empty !toploop) then error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; + Printer.enable_goal_tags_printing := true; color := `OFF (** Options for CoqIDE *) @@ -291,9 +292,17 @@ let init_gc () = We no longer use [Arg.parse], in order to use share [Usage.print_usage] between coqtop and coqc. *) +let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem" + (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") + +exception NoCoqLib let usage () = - Envars.set_coqlib ~fail:CErrors.error; + begin + try + Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib); init_load_path (); + with NoCoqLib -> usage_no_coqlib () + end; if !batch_mode then Usage.print_usage_coqc () else begin Mltop.load_ml_objects_raw_rex diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e457ca61d..e29048035 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -30,6 +30,7 @@ let print_usage_channel co command = \n -R dir coqdir recursively map physical dir to logical coqdir\ \n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ +\n -coqlib dir set the coq standard library directory\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ \n -noinit start without loading the Init library\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9f6f77ef1..eaf685b18 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -79,7 +79,9 @@ let pr_new_syntax po loc chan_beautify ocom = and a glimpse of the executed command *) let pp_cmd_header loc com = - let shorten s = try (String.sub s 0 30)^"..." with _ -> s in + let shorten s = + if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s + in let noblank s = String.map (fun c -> match c with | ' ' | '\n' | '\t' | '\r' -> '~' @@ -323,8 +325,5 @@ let compile verbosely f = let compile v f = ignore(CoqworkmgrApi.get 1); - begin - try compile v f - with any -> Topfmt.print_err_exn any - end; + compile v f; CoqworkmgrApi.giveback 1 diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index deb2ed3e0..bf274901b 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -44,6 +44,11 @@ let rec search_cst_label lab = function | (l, SFBconst cb) :: _ when Label.equal l lab -> cb | _ :: fields -> search_cst_label lab fields +let rec search_mind_label lab = function + | [] -> raise Not_found + | (l, SFBmind mind) :: _ when Label.equal l lab -> mind + | _ :: fields -> search_mind_label lab fields + (* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But: a) I don't see currently what should be used instead b) this shouldn't be critical for Print Assumption. At worse some @@ -135,6 +140,18 @@ let lookup_constant cst = else lookup_constant_in_impl cst (Some cb) with Not_found -> lookup_constant_in_impl cst None +let lookup_mind_in_impl mind = + try + let mp,dp,lab = repr_kn (canonical_mind mind) in + let fields = memoize_fields_of_mp mp in + search_mind_label lab fields + with Not_found -> + anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind) + +let lookup_mind mind = + try Global.lookup_mind mind + with Not_found -> lookup_mind_in_impl mind + (** Graph traversal of an object, collecting on the way the dependencies of traversed objects *) @@ -227,7 +244,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj = where I_0, I_1, ... are in the same mutual definition and c_ij are all their constructors. *) if Refmap_env.mem firstind_ref data then data, ax2ty else - let mib = Global.lookup_mind mind in + let mib = lookup_mind mind in (* Collects references of parameters *) let param_ctx = mib.mind_params_ctxt in let nparam = List.length param_ctx in @@ -331,7 +348,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = else accu | IndRef (m,_) | ConstructRef ((m,_),_) -> - let mind = Global.lookup_mind m in + let mind = lookup_mind m in if mind.mind_typing_flags.check_guarded then accu else diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e0520216b..5233fab15 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1088,7 +1088,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit Defined cst) else ( let len = Array.length obls in - let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in + let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e191ed0f2..6c31465fc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1412,6 +1412,15 @@ let _ = optwrite = (fun _ -> ()) } let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "display compact goal contexts"; + optkey = ["Printing";"Compact";"Contexts"]; + optread = (fun () -> Printer.get_compact_context()); + optwrite = (fun b -> Printer.set_compact_context b) } + +let _ = declare_int_option { optsync = true; optdepr = false; |