From 09b5e429cd4f622003277c31391bafc20b389af5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 23 Jan 2015 14:25:02 +0100 Subject: Typos, grammar, layout in CHANGES. --- CHANGES | 54 +++++++++++++++++++++++++++--------------------------- 1 file changed, 27 insertions(+), 27 deletions(-) diff --git a/CHANGES b/CHANGES index 3471bc61c4..6cba4f54f1 100644 --- a/CHANGES +++ b/CHANGES @@ -109,27 +109,27 @@ Tactics * New "multimatch" variant of "match" tactic which backtracks to new branches in case of a later failure. The "match" tactic is equivalent to "once multimatch". - * New selector all: to qualify a tactic allows applying a tactic to - all the focused goal, instead of just the first one as is the + * New selector "all:" such that "all:tac" applies tactic "tac" to + all the focused goals, instead of just the first one as is the default. * A corresponding new option Set Default Goal Selector "all" makes the tactics in scripts be applied to all the focused goal by default - * New selector par: to qualify a tactic allows applying a (terminating) - tactic to all the focused goal in parallel. The number of worker can - be selected with -async-proofs-tac-j and also limited using the + * New selector "par:" such that "par:tac" applies the (terminating) + tactic "tac" to all the focused goal in parallel. The number of worker + can be selected with -async-proofs-tac-j and also limited using the coqworkmgr utility. * New tactics "revgoals", "cycle" and "swap" to reorder goals. - * The semantics of recursive tactics (introduced with Ltac t := - ... or let rec t := ... in ...) changes slightly as t is now - applied to every goal not each goal independently, in particular - it may be applied when no goal are left. This may cause tactics - such as let rec t := constructor;t to loop indefinitely. The - simple fix is to rewrite the recursive calls as follows: let rec t - := constructor;[t..] which recovers the earlier behavior (source - of rare incompatibilities). - * New tactic language feature "numgoals" to count number of goals. - Accompanied by "guard" tactic which fails if a Boolean test does - not pass. + * The semantics of recursive tactics (introduced with "Ltac t := ..." + or "let rec t := ... in ...") changed slightly as t is now + applied to every goals, not each goal independently. In particular + it may be applied when no goals are left. This may cause tactics + such as "let rec t := constructor;t" to loop indefinitely. The + simple fix is to rewrite the recursive calls as follows: + "let rec t := constructor;[t..]" which recovers the earlier behavior + (source of rare incompatibilities). + * New tactic language feature "numgoals" to count number of goals. It is + accompanied by a "guard" tactic which fails if a Boolean test over + integers does not pass. * New tactical "[> ... ]" to apply tactics to individual goals. * New tactic "gfail" which works like "fail" except it will also fail if every goal has been solved. @@ -143,7 +143,7 @@ Tactics Unshelve command. * A variant shelve_unifiable only removes those goals which appear as existential variables in other goals. To emulate the old - refine, use (refine c;shelve_unifiable). This can still cause + refine, use "refine c;shelve_unifiable". This can still cause incompatibilities in rare occasions. * New "give_up" tactic to skip over a goal without admitting it. - Matching using "lazymatch" was fundamentally modified. It now behaves @@ -221,15 +221,15 @@ Tactics the relevant hypotheses). - New construct "uconstr:c" and "type_term c" to build untyped terms. - Binders in terms defined in Ltac (either "constr" or "uconstr") can - now take their names from identifier defined in Ltac. As a - consequence, a name cannot be used in a binder (constr:(fun x => - ...)) if an Ltac variable of that name already exists and does not + now take their names from identifiers defined in Ltac. As a + consequence, a name cannot be used in a binder "constr:(fun x => + ...)" if an Ltac variable of that name already exists and does not contain an identifier. Source of occasional incompatibilities. - The "refine" tactic now accepts untyped terms built with "uconstr" so that terms with holes can be constructed piecewise in Ltac. - New bullets --, ++, **, ---, +++, ***, ... made available. - More informative messages when wrong bullet is used. -- bullet suggestion when a subgoal is solved. +- Bullet suggestion when a subgoal is solved. - New tactic "enough", symmetric to "assert", but with subgoals swapped, as a more friendly replacement of "cut". - In destruct/induction, experimental modifier "!" prefixing the @@ -270,9 +270,9 @@ Notations (possible source of incompatibilities) - Notations accept term-providing tactics using the $(...)$ syntax. - "Bind Scope" can no longer bind "Funclass" and "Sortclass". -- A notation can be given a (compat "8.x") annotation, making - it behave like a (only parsing), but flags may active warning - or error when this notation is used. +- A notation can be given a (compat "8.x") annotation, making it behave + like a "only parsing" notation, but the annotation may lead to eventually + issue warnings or errors in further versions when this notation is used. - More systematic insertion of spaces as a default for printing notations ("format" still available to override the default). - In notations, a level modifier referring to a non-existent variable is @@ -305,14 +305,14 @@ Interfaces - CoqIDE supports asynchronous edition of the document, ongoing tasks and errors are reported in the bottom right window. The number of workers taking care of processing proofs can be selected with -async-proofs-j. -- CoqIDE highlight in yellow "unsafe" commands such as axiom +- CoqIDE highlights in yellow "unsafe" commands such as axiom declarations, and tactics like "admit". - CoqIDE supports Proof General like key bindings; to activate the PG mode go to Edit -> Preferences -> Editor. For the documentation see Help -> Help for PG mode. - CoqIDE automatically retracts the locked area when one edits the locked text. -- CoqIDE search and replace got regular expressions power. See the +- CoqIDE search and replace got regular expressions power. See the documentation of OCaml's Str module for the supported syntax. - Many CoqIDE windows, including the query one, are now detachable to improve usability on multi screen work stations. @@ -334,7 +334,7 @@ Internal Infrastructure initially does a "Require" of Prelude.vo (or nothing when given the options -noinit or -nois). - The format of vo files has slightly changed: cf final comments in - checker/cic.mli + checker/cic.mli. - The build system does not produce anymore programs named coqtop.opt and a symbolic link to coqtop. Instead, coqtop is now directly an executable compiled with the best OCaml compiler available. -- cgit v1.2.3 From c930010fc53531784485d5a190f9c0aeba1dfdbe Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 23 Jan 2015 14:40:57 +0100 Subject: Typos, grammar, layout in CHANGES (continued). --- CHANGES | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/CHANGES b/CHANGES index 6cba4f54f1..8c5b1c4a89 100644 --- a/CHANGES +++ b/CHANGES @@ -14,15 +14,14 @@ Logic parameters, i.e. [@p] is definitionally equal to [λ params r. r.(p)]. Records with primitive projections have eta-conversion, the canonical form being [mkR pars (p1 t) ... (pn t)]. - - New universe polymorphism (see reference manual) - New option -type-in-type to collapse the universe hierarchy (this makes the logic inconsistent). -- The guard condition for fixpoints is now a bit stricter. Propagation of -subterm value through pattern matching is restricted according to the return -predicate. Restores compatibility of Coq's logic with the propositional -extensionality axiom. May create incompatibilities in recursive programs heavily -using dependent types. +- The guard condition for fixpoints is now a bit stricter. Propagation + of subterm value through pattern matching is restricted according to + the return predicate. Restores compatibility of Coq's logic with the + propositional extensionality axiom. May create incompatibilities in + recursive programs heavily using dependent types. Vernacular commands @@ -44,7 +43,7 @@ Vernacular commands - Command "Search" has been renamed into "SearchHead". The command name "Search" now behaves like former "SearchAbout". The latter name is deprecated. -- "Search" "About" "SearchHead" "SearchRewrite" and "SearchPattern" +- "Search", "About", "SearchHead", "SearchRewrite" and "SearchPattern" now search for hypothesis (of the current goal by default) first. They now also support the goal selector prefix to specify another goal to search: e.g. "n:Search id". This is also true for @@ -63,13 +62,13 @@ Vernacular commands - New "Refine Instance Mode" option that allows to deactivate the generation of obligations in incomplete typeclass instances, raising an error instead. - "Collection" command to name sets of section hypotheses. Named collections - can be used in the syntax of "Proof using" to assert with section variables + can be used in the syntax of "Proof using" to assert which section variables are used in a proof. - The "Optimize Proof" command can be placed in the middle of a proof to - force the compaction the data structure used to represent the ongoing - proof (evar map). This may result in a lower memory footprint and speed up + force the compaction of the data structure used to represent the ongoing + proof (evar map). This may result in a lower memory footprint and speed up the execution of the following tactics. -- "Optimize Heap" command to tell the OCaml runtime to performa a major +- "Optimize Heap" command to tell the OCaml runtime to perform a major garbage collection step and heap compaction. Specification Language @@ -98,9 +97,9 @@ Tactics instantiation information of existential variables is always propagated to tactics, removing the need to manually use the "instantiate" tactics to mark propagation points. - * New tactical (a+b) insert a backtracking point. When (a+b);c fails + * New tactical (a+b) inserts a backtracking point. When (a+b);c fails during the execution of c, it can backtrack and try b instead of a. - * New tactical (once a) removes all the backtracking point from a + * New tactical (once a) removes all the backtracking points from a (i.e. it selects the first success of a). * Tactic "constructor" is now fully backtracking, thus deprecating the need of the undocumented "constructor " syntax which is -- cgit v1.2.3 From a9026275399a891d47f0d10f624a783a1afea05d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 23 Jan 2015 17:31:52 +0100 Subject: Fix previous commit on extraction. Since name clashes are discovered by side effects, the order of traversal of module structs cannot be changed. --- plugins/extraction/ocaml.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index ce88ea6d29..85f18a0933 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -634,10 +634,12 @@ and pp_module_type params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (mp, sign) -> push_visible mp params; - let try_pp_specif x l = + let try_pp_specif l x = try pp_specif x :: l with Failure "empty phrase" -> l in - let l = List.fold_right try_pp_specif sign [] in + (* We cannot use fold_right here due to side effects in pp_specif *) + let l = List.fold_left try_pp_specif [] sign in + let l = List.rev l in pop_visible (); str "sig " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ @@ -710,10 +712,12 @@ and pp_module_expr params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEstruct (mp, sel) -> push_visible mp params; - let try_pp_structure_elem x l = + let try_pp_structure_elem l x = try pp_structure_elem x :: l with Failure "empty phrase" -> l in - let l = List.fold_right try_pp_structure_elem sel [] in + (* We cannot use fold_right here due to side effects in pp_structure_elem *) + let l = List.fold_left try_pp_structure_elem [] sel in + let l = List.rev l in pop_visible (); str "struct " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ -- cgit v1.2.3 From f4d77142a6e1d298fadf4219c46fcc9ff8abe62a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 24 Jan 2015 09:59:27 +0100 Subject: Tentative workaround for bug #3798. Ultimately setoid rewrite should be written in the monad to fix it properly. --- proofs/pfedit.ml | 35 +++++++++++++++++++++++++++++++++++ proofs/pfedit.mli | 8 ++++++++ tactics/rewrite.ml | 4 +--- tactics/tacinterp.ml | 34 +--------------------------------- 4 files changed, 45 insertions(+), 36 deletions(-) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index fdc93bcb90..d1b6afe220 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -156,6 +156,41 @@ let build_by_tactic env ctx ?(poly=false) typ tac = assert(Univ.ContextSet.is_empty ctx); cb, status, univs +let refine_by_tactic env sigma ty tac = + (** Save the initial side-effects to restore them afterwards. We set the + current set of side-effects to be empty so that we can retrieve the + ones created during the tactic invocation easily. *) + let eff = Evd.eval_side_effects sigma in + let sigma = Evd.drop_side_effects sigma in + (** Start a proof *) + let prf = Proof.start sigma [env, ty] in + let (prf, _) = + try Proof.run_tactic env tac prf + with Logic_monad.TacticFailure e as src -> + (** Catch the inner error of the monad tactic *) + let (_, info) = Errors.push src in + iraise (e, info) + in + (** Plug back the retrieved sigma *) + let sigma = Proof.in_proof prf (fun sigma -> sigma) in + let ans = match Proof.initial_goals prf with + | [c, _] -> c + | _ -> assert false + in + let ans = Reductionops.nf_evar sigma ans in + (** [neff] contains the freshly generated side-effects *) + let neff = Evd.eval_side_effects sigma in + (** Reset the old side-effects *) + let sigma = Evd.drop_side_effects sigma in + let sigma = Evd.emit_side_effects eff sigma in + (** Get rid of the fresh side-effects by internalizing them in the term + itself. Note that this is unsound, because the tactic may have solved + other goals that were already present during its invocation, so that + those goals rely on effects that are not present anymore. Hopefully, + this hack will work in most cases. *) + let ans = Term_typing.handle_side_effects env ans neff in + ans, sigma + (**********************************************************************) (* Support for resolution of evars in tactic interpretation, including resolution by application of tactics *) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index edbc18a366..5e0fb4dd36 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -157,6 +157,14 @@ val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context +val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic -> + constr * Evd.evar_map +(** A variant of the above function that handles open terms as well. + Caveat: all effects are purged in the returned term at the end, but other + evars solved by side-effects are NOT purged, so that unexpected failures may + occur. Ideally all code using this function should be rewritten in the + monad. *) + (** Declare the default tactic to fill implicit arguments *) val declare_implicit_tactic : unit Proofview.tactic -> unit diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index a3914da153..0140f74f50 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -629,11 +629,9 @@ let solve_remaining_by env sigma holes by = | None -> sigma (** Evar should not be defined, but just in case *) | Some evi -> - let ctx = Evd.evar_universe_context sigma in let env = Environ.reset_with_named_context evi.evar_hyps env in let ty = evi.evar_concl in - let c, _, ctx = Pfedit.build_by_tactic env ctx ty solve_tac in - let sigma = Evd.set_universe_context sigma ctx in + let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in Evd.define evk c sigma in List.fold_left solve sigma indep diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 23de47d567..b1ff0e4014 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2349,39 +2349,7 @@ let _ = if has_type arg (glbwit wit_tactic) then let tac = out_gen (glbwit wit_tactic) arg in let tac = interp_tactic ist tac in - (** Save the initial side-effects to restore them afterwards. We set the - current set of side-effects to be empty so that we can retrieve the - ones created during the tactic invocation easily. *) - let eff = Evd.eval_side_effects sigma in - let sigma = Evd.drop_side_effects sigma in - (** Start a proof *) - let prf = Proof.start sigma [env, ty] in - let (prf, _) = - try Proof.run_tactic env tac prf - with Logic_monad.TacticFailure e as src -> - (** Catch the inner error of the monad tactic *) - let (_, info) = Errors.push src in - iraise (e, info) - in - (** Plug back the retrieved sigma *) - let sigma = Proof.in_proof prf (fun sigma -> sigma) in - let ans = match Proof.initial_goals prf with - | [c, _] -> c - | _ -> assert false - in - let ans = Reductionops.nf_evar sigma ans in - (** [neff] contains the freshly generated side-effects *) - let neff = Evd.eval_side_effects sigma in - (** Reset the old side-effects *) - let sigma = Evd.drop_side_effects sigma in - let sigma = Evd.emit_side_effects eff sigma in - (** Get rid of the fresh side-effects by internalizing them in the term - itself. Note that this is unsound, because the tactic may have solved - other goals that were already present during its invocation, so that - those goals rely on effects that are not present anymore. Hopefully, - this hack will work in most cases. *) - let ans = Term_typing.handle_side_effects env ans neff in - ans, sigma + Pfedit.refine_by_tactic env sigma ty tac else failwith "not a tactic" in -- cgit v1.2.3 From ef61bb05911d19c77d565d78dc57107d40c333e4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Jan 2015 11:54:00 +0100 Subject: Isolate a function for printing evar sets. --- printing/printer.ml | 10 ++++++++++ printing/printer.mli | 2 ++ toplevel/vernacentries.ml | 8 ++------ 3 files changed, 14 insertions(+), 6 deletions(-) diff --git a/printing/printer.ml b/printing/printer.ml index 3403fb9c3b..8a2d6e7bd1 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -446,6 +446,16 @@ let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ i let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs) +(* Display a list of evars given by their name, with a prefix *) +let pr_ne_evar_set hd tl sigma l = + if l != Evar.Set.empty then + let l = Evar.Set.fold (fun ev -> + Evar.Map.add ev (Evarutil.nf_evar_info sigma (Evd.find sigma ev))) + l Evar.Map.empty in + hd ++ pr_evars sigma l ++ tl + else + mt () + let default_pr_subgoal n sigma = let rec prrec p = function | [] -> error "No such goal." diff --git a/printing/printer.mli b/printing/printer.mli index 6b9c70815d..42ed2b6d9e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -137,6 +137,8 @@ val pr_nth_open_subgoal : int -> std_ppcmds val pr_evar : evar_map -> (evar * evar_info) -> std_ppcmds val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds val pr_evars : evar_map -> evar_info Evar.Map.t -> std_ppcmds +val pr_ne_evar_set : std_ppcmds -> std_ppcmds -> evar_map -> + Evar.Set.t -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fb12edfbc2..bb20730015 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1516,12 +1516,8 @@ let vernac_check_may_eval redexp glopt rc = let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in msg_notice (print_judgment env sigma' j ++ - (if l != Evar.Set.empty then - let l = Evar.Set.fold (fun ev -> Evar.Map.add ev (Evarutil.nf_evar_info sigma' (Evd.find sigma' ev))) l Evar.Map.empty in - (fnl () ++ str "where" ++ fnl () ++ pr_evars sigma' l) - else - mt ()) ++ - Printer.pr_universe_ctx uctx) + pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ + Printer.pr_universe_ctx uctx) | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in -- cgit v1.2.3 From 982b583efe9f657d76b4257200769fed55453623 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Jan 2015 20:41:13 +0100 Subject: Equality Schemes options: reverting commit ff9f94634 which is obviously inconsistent with the decisions taken in commits 2e8fb20e04da and 0bc569026048 about bugs #2550 and #3606. Now having options Boolean Equality Schemes and Decidable Equality Schemes. --- toplevel/indschemes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index e6b2382867..fbc45b4ae3 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -85,7 +85,7 @@ let _ = { optsync = true; optdepr = false; optname = "automatic declaration of boolean equality"; - optkey = ["Equality";"Schemes"]; + optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } let _ = (* compatibility *) -- cgit v1.2.3 From 14787df2ea09994151e886bf918aca0aecbd8ade Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Jan 2015 20:08:53 +0100 Subject: Reference Manual: Documenting new printing of evars and new effect of Set Printing Existential Instances (see bug report #3951). --- doc/refman/RefMan-ext.tex | 75 +++++++++++++++++++++++++++++++++-------------- doc/refman/RefMan-pro.tex | 2 +- doc/refman/RefMan-tac.tex | 10 +++---- 3 files changed, 59 insertions(+), 28 deletions(-) diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 2a976a07b3..193479cceb 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1929,30 +1929,60 @@ tools. The format is unspecified if {\str} doesn't end in \texttt{.dot} or \texttt{.gv}. \section[Existential variables]{Existential variables\label{ExistentialVariables}} +\label{evars} -Coq terms can include existential variables. An existential variable -is a placeholder intended to eventually be replaced by an actual -subterm though which subterm it will be replaced by is still unknown. +Coq terms can include existential variables which +represents unknown subterms to eventually be replaced by actual +subterms. Existential variables are generated in place of unsolvable implicit -arguments when using commands such as \texttt{Check} (see -Section~\ref{Check}) or in place of unsolvable instances when using -tactics such as \texttt{eapply} (see Section~\ref{eapply}). They can -only appear as the result of a command displaying a term and they are -represented by ``?'' followed by a number. They cannot be entered by -the user (though they can be generated from ``\_'' when the -corresponding implicit argument is unsolvable). - -A given existential variable name can occur several times in a term -meaning the corresponding expected instance is shared. Each -existential variable is relative to a context, as shown by {\tt Show - Existential} when in the process of proving a goal (see -Section~\ref{ShowExistentials}). Henceforth, each occurrence of an -existential variable in a term is subject to an instance of the -variables of its context of definition which is specific to this -occurrence. +arguments or ``{\tt \_}'' placeholders when using commands such as +\texttt{Check} (see Section~\ref{Check}) or when using tactics such as +\texttt{refine}~(see Section~\ref{refine}), as well as in place of unsolvable +instances when using tactics such that \texttt{eapply} (see +Section~\ref{eapply}). An existential variable is defined in a +context, which is the context of variables of the placeholder which +generated the existential variable, and a type, which is the expected +type of the placeholder. + +As a consequence of typing constraints, existential variables can be +duplicated in such a way that they possibly appear in different +contexts than their defining context. Thus, any occurrence of a given +existential variable comes with an instance of its original context. In the +simple case, when an existential variable denotes the placeholder +which generated it, or is used in the same context as the one in which +it was generated, the context is not displayed and the existential +variable is represented by ``?'' followed by an identifier. + +\begin{coq_example} +Parameter identity : forall (X:Set), X -> X. +Check identity _ _. +Check identity _ (fun x => _). +\end{coq_example} + +In the general case, when an existential variable ?{\ident} +appears outside of its context of definition, its instance, written under +the form \verb!@{id1:=term1; ...; idn:=termn}!, is appending to its +name, indicating how the variables of its defining context are +instantiated. The variables of the context of the existential +variables which are instantiated by themselves are not written, unless +the flag {\tt Printing Existential Instances} is on (see +Section~\ref{SetPrintingExistentialInstances}), and this is why an +existential variable used in the same context as its context of +definition is written with no instance. + +\begin{coq_example} +Check (fun x y => _) 0 1. +Set Printing Existential Instances. +Check (fun x y => _) 0 1. +\end{coq_example} + +\begin{coq_eval} +Unset Printing Existential Instances. +\end{coq_eval} \subsection{Explicit displaying of existential instances for pretty-printing +\label{SetPrintingExistentialInstances} \comindex{Set Printing Existential Instances} \comindex{Unset Printing Existential Instances}} @@ -1960,10 +1990,11 @@ The command: \begin{quote} {\tt Set Printing Existential Instances} \end{quote} -activates the display of how the context of an existential variable is -instantiated on each of its occurrences. +activates the full display of how the context of an existential variable is +instantiated at each of the occurrences of the existential variable. -To deactivate the display of the instances of existential variables, use +To deactivate the full display of the instances of existential +variables, use \begin{quote} {\tt Unset Printing Existential Instances.} \end{quote} diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index eabb376395..df707ce941 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -239,7 +239,7 @@ proof was edited. This command instantiates an existential variable. {\tt \num} is an index in the list of uninstantiated existential variables -displayed by {\tt Show Existentials.} (described in Section~\ref{Show}) +displayed by {\tt Show Existentials} (described in Section~\ref{Show}). This command is intended to be used to instantiate existential variables when the proof is completed but some uninstantiated diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 1b7adc2517..35da17d546 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -260,6 +260,7 @@ Defined. \subsection{\tt apply \term} \tacindex{apply} \label{apply} +\label{eapply} This tactic applies to any goal. The argument {\term} is a term well-formed in the local context. The tactic {\tt apply} tries to @@ -329,14 +330,13 @@ Section~\ref{pattern} to transform the goal so that it gets the form generated by {\tt apply} {\term$_i$}, starting from the application of {\term$_1$}. -\item {\tt eapply \term}\tacindex{eapply}\label{eapply} +\item {\tt eapply \term}\tacindex{eapply} The tactic {\tt eapply} behaves like {\tt apply} but it does not fail when no instantiations are deducible for some variables in the - premises. Rather, it turns these variables into so-called - existential variables which are variables still to instantiate. An - existential variable is identified by a name of the form {\tt ?$n$} - where $n$ is a number. The instantiation is intended to be found + premises. Rather, it turns these variables into + existential variables which are variables still to instantiate (see + Section~\ref{evars}). The instantiation is intended to be found later in the proof. \item {\tt simple apply {\term}} \tacindex{simple apply} -- cgit v1.2.3 From 0e06c54a9249477fdab5b135ffdac4bd3ea501a5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Jan 2015 21:27:54 +0100 Subject: Removed obsolete option "Legacy Partially Applied Elimination Argument" which I used temporarily in a branch to have "destruct eq_dec" working like in v8.4 and not like the "destruct (eq_dec _ _)" of 8.4. I finally made "destruct (eq_dec _ _)" working in 8.5 like "destruct eq_dec" was working in 8.4 (and is still working in 8.5). --- tactics/tactics.ml | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f1f1248d7c..07969c7d74 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -59,22 +59,7 @@ let dloc = Loc.ghost let typ_of = Retyping.get_type_of -(* Option for 8.4 compatibility *) open Goptions -let legacy_elim_if_not_fully_applied_argument = ref false - -let use_legacy_elim_if_not_fully_applied_argument () = - !legacy_elim_if_not_fully_applied_argument - || Flags.version_less_or_equal Flags.V8_4 - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "partially applied elimination argument legacy"; - optkey = ["Legacy";"Partially";"Applied";"Elimination";"Argument"]; - optread = (fun () -> !legacy_elim_if_not_fully_applied_argument) ; - optwrite = (fun b -> legacy_elim_if_not_fully_applied_argument := b) } (* Option for 8.2 compatibility *) let dependent_propositions_elimination = ref true -- cgit v1.2.3 From bb37153d90de103dabd02285d11b3c39e3e4f89c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Jan 2015 21:48:12 +0100 Subject: Updating CHANGES (grammar, thanks to AS for pointing it out) + a line on "Intuition Negation Unfolding". --- CHANGES | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index 8c5b1c4a89..a8411a2126 100644 --- a/CHANGES +++ b/CHANGES @@ -120,7 +120,7 @@ Tactics * New tactics "revgoals", "cycle" and "swap" to reorder goals. * The semantics of recursive tactics (introduced with "Ltac t := ..." or "let rec t := ... in ...") changed slightly as t is now - applied to every goals, not each goal independently. In particular + applied to every goal, not each goal independently. In particular it may be applied when no goals are left. This may cause tactics such as "let rec t := constructor;t" to loop indefinitely. The simple fix is to rewrite the recursive calls as follows: @@ -163,7 +163,9 @@ Tactics opposite side, new tactic "dtauto" is able to destruct any record-like inductive types, superseding the old version of "tauto". - Similarly, "intuition" has been made more uniform and, where it now - fails, "dintuition" can be used. (possible source of incompatibilities) + fails, "dintuition" can be used (possible source of incompatibilities). +- New option "Unset Intuition Negation Unfolding" for deactivating automatic + unfolding of "not" in intuition. - Tactic notations can now be defined locally to a module (use "Local" prefix). - Tactic "red" now reduces head beta-iota redexes (potential source of rare incompatibilities). -- cgit v1.2.3 From 27aec3933031ec5e87738965c25ffa51863c9400 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Jan 2015 22:25:01 +0100 Subject: Doc: Fixing some compilation problems with chapter Canonical Structures. Text mode + a "Require Import" in a module which provokes suspect warnings "Exception Not_found". --- doc/refman/CanonicalStructures.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index 28a6f69032..c8e36197ca 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -306,8 +306,8 @@ canonical structures. We need some infrastructure for that. \begin{coq_example} +Require Import Strings.String. Module infrastructure. - Require Import Strings.String. Inductive phantom {T : Type} (t : T) : Type := Phantom. Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 -> phantom t2. Definition id {T} {t : T} (x : phantom t) := x. @@ -318,8 +318,8 @@ Module infrastructure. End infrastructure. \end{coq_example} -To explain the notation $[find v | t1 \textasciitilde t2]$ lets pick one -of its instances: $[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]$. +To explain the notation \texttt{[find v | t1 \textasciitilde t2]} let us pick one +of its instances: \texttt{[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]}. It should be read as: ``find a class e such that its objects have type T or fail with message "T is not an EQ.type"''. -- cgit v1.2.3 From d3934986fb2ff0d563a1a2a89ba5fbbefb53f0fd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 24 Jan 2015 10:34:26 +0100 Subject: Test for bug #3798. --- test-suite/bugs/closed/3798.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/3798.v diff --git a/test-suite/bugs/closed/3798.v b/test-suite/bugs/closed/3798.v new file mode 100644 index 0000000000..623822e990 --- /dev/null +++ b/test-suite/bugs/closed/3798.v @@ -0,0 +1,11 @@ +Require Setoid. + +Parameter f : nat -> nat. +Axiom a : forall n, 0 < n -> f n = 0. +Hint Rewrite a using ( simpl; admit ). + +Goal f 1 = 0. +Proof. + rewrite_strat (topdown (hints core)). + reflexivity. +Qed. -- cgit v1.2.3 From 3fa1bf32ec323ce03a7fa818a8daccb78b862ca6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 25 Jan 2015 17:38:52 +0100 Subject: Fixing bug #3947. --- ide/wg_Find.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index b6f63a3ba1..b6b1ea6bcb 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -8,6 +8,8 @@ type mode = [ `FIND | `REPLACE ] +let b2c = Ideutils.byte_offset_to_char_offset + class finder name (view : GText.view) = let widget = Wg_Detachable.detachable @@ -85,8 +87,8 @@ class finder name (view : GText.view) = try let i = Str.search_backward regexp text (String.length text - 1) in let j = Str.match_end () in - Some(view#buffer#start_iter#forward_chars i, - view#buffer#start_iter#forward_chars j) + Some(view#buffer#start_iter#forward_chars (b2c text i), + view#buffer#start_iter#forward_chars (b2c text j)) with Not_found -> None method private forward_search starti = @@ -95,7 +97,7 @@ class finder name (view : GText.view) = try let i = Str.search_forward regexp text 0 in let j = Str.match_end () in - Some(starti#forward_chars i, starti#forward_chars j) + Some(starti#forward_chars (b2c text i), starti#forward_chars (b2c text j)) with Not_found -> None method replace_all () = -- cgit v1.2.3 From 3d6b9a7ab992559493b89e174549734dff401703 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 25 Jan 2015 17:49:35 +0100 Subject: Made replacing of text in CoqIDE atomic w.r.t. the undo/redo. --- ide/wg_Find.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index b6b1ea6bcb..a0949ca0c8 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -63,8 +63,10 @@ class finder name (view : GText.view) = method replace () = if self#may_replace () then let txt = self#get_selected_word () in + let () = view#buffer#begin_user_action () in let _ = view#buffer#delete_selection () in let _ = view#buffer#insert_interactive (self#replacement txt) in + let () = view#buffer#end_user_action () in self#find_forward () else self#find_forward () @@ -117,7 +119,9 @@ class finder name (view : GText.view) = let () = view#buffer#delete_mark (`MARK stop_mark) in replace_at next in - replace_at view#buffer#start_iter + let () = view#buffer#begin_user_action () in + let () = replace_at view#buffer#start_iter in + view#buffer#end_user_action () method private set_not_found () = find_entry#misc#modify_base [`NORMAL, `NAME "#F7E6E6"]; -- cgit v1.2.3