aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
...
* CoqIdE configuration file won't pollute your home anymoreGravatar pboutill2011-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for XDG_DATA_HOME and XDG_DATA_DIRS.Gravatar pboutill2011-11-20
| | | | | | From Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For instance, consider this inductive type: Inductive Ind := A | B | C | D. For detecting "match" on this type, one was forced earlier to write code in Ltac using "match goal" and/or "context [...]" and long patterns such as: match _ with A => _ | B => _ | C => _ | D => _ end After this patch, this pattern can be shortened in many alternative ways: match _ with A => _ | _ => _ end match _ with B => _ | _ => _ end match _ in Ind with _ => _ end Indeed, if we want to detect a "match" of a given type, we can either leave at least one branch where a constructor is explicit, or use a "in" annotation. Now, we can also detect any "match" regardless of its type: match _ with _ => _ end Note : this will even detect "match" over empty inductive types. Compatibility should be preserved, since "match _ with end" will continue to correspond only to empty inductive types. Internally, the constr_pattern PCase has changed quite a lot, a few elements are now grouped into a case_info_pattern record, while branches are now lists of given sub-patterns. NB: writing "match" with missing last branches in a constr pattern was actually tolerated by Pattern.pattern_of_glob_constr earlier, since the number of constructor per inductive is unknown there. And this was triggering an uncaught exception in a array_fold_left_2 in Matching later. Oups. At least this patch fixes this issue... Btw: the code in Pattern.pattern_of_glob_constr was quadratic in the number of branch in a match pattern. I doubt this was really a problem, but having now linear code instead cannot harm ;-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Equality.injectable which did not detect an equality withoutGravatar herbelin2011-10-22
| | | | | | | | | | | | | | | constructors as non relevant for injection. Also made injection failing in such situation. Incidentally, this fixes a loop in Invfun.reflexivity_with_destruct_cases (observed in the compilation of CoinductiveReals.LNP_Digit). The most probable explanation is that this loop was formerly protected by a failing rewrite which stopped failing after revision 14549 made second-order pattern-matching more powerful. Also suppressed dead code in Invfun.intros_with_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedGravatar herbelin2011-10-11
| | | | | | | | | | | second-order matching) which was not working correctly in the general case. Also made that second-order matching for tactics (abstract_list_all) uses this algorithm, along the lines of a proposal first experimented by Dan Grayson (see unification.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14549 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
| | | | | | Tactics set/remember and destruct/induction take benefit of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
* auto with nocore : disable the use of the core database (wish #2188)Gravatar letouzey2011-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Omega: for non-arithmetical goals, try proving False from context (wish #2236)Gravatar letouzey2011-09-16
| | | | | | | | | | | | | | | | | | This way, no more error messages like "Unrecognized predicate". Some code simplification and reorganization on the way, in particular a few tests like "is_Prop ..." or "closed0 ..." were actually useless. Also add support for the situation H:~Zne x y for uniformity. Beware: scripts relying negatively on the strength of omega may have to be adapted (e.g. "try omega. some_more_tactics_in_case_omega_fails."). For instance, one line deletion in PermutSetoid.v Probably more cumbersome : "auto with *" becomes stronger since it may call omega. Todo : check the impact on contribs tomorrow. Btw, this commit seems to solve a bug where omega was to be guided by some (set foo:= ...) before being able to succeed (cf PermutSetoid.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using ↵Gravatar aspiwack2011-09-12
| | | | | | the uid returned by Goal.uid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2577: Second attempt to be correct.Gravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14424 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updates in CHANGESGravatar letouzey2011-08-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14416 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | that the kernel conversion solves the delta/delta critical pair the same way the tactics did. This allows to improve Qed time when slow down is due to conversion having (arbitrarily) made the wrong choice. Propagation is done thanks to a new kind of cast called REVERTcast. Notes: - Vm conversion not modified - size of vo generally grows because of additional casts - this remains a heuristic... for the record, when a reduction tactic is applied on the goal t leading to new goal t', this is translated in the kernel in a conversion t' <= t where, hence, reducing in t' must be preferred; what the propagation of reduction cast to the kernel does not do is whether it is preferable to first unfold c or to first compare u' and u in "c u' = c u"; in particular, intermediate casts are sometimes useful to solve this kind of issues (this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the combination "simpl;red" needs the intermediate cast to ensure Qed answers quickly); henceforth the merge of nested casts in mkCast is deactivated - for tactic "change", REVERTcast should be used when conversion is in the hypotheses, but convert_hyp does not (yet) support this (would require e.g. that convert_hyp overwrite some given hyp id with a body-cleared let-binding new_id := Cast(old_id,REVERTCast,t)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made CHANGES more uniformly writtenGravatar herbelin2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less ambitious application of a notation for eq_rect. We proposedGravatar herbelin2011-08-10
| | | | | | | | | | | | | | | | | | "rewrite Heq in H" but "rewrite" is sometimes used by users and I don't want to have to change their file. The solution to put the notations in a module does not work with name "rewrite" because loading the module would change the status of "rewrite" from simple ident to keyword (and we cannot declare "rewrite" as an ident, as shown in previous commit). Then we come back on notation "rew" (this name is also used by some users), in a module. This continues commit r14366 and r14390 and improves on the level of the notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo of bug 2577Gravatar pboutill2011-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14303 85f007b7-540e-0410-9357-904b9bb8a0f7
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
| | | | | | | | | | | that forces a given type to always be printed as a record, or with a constructor, regardless of the setting of 'Printing Records'. And this is that patch that controls printing by type. (patch from Tom Prince) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
* This option disables the use of the '{| field := ... |}' notationGravatar herbelin2011-07-16
| | | | | | | | when printing. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)Gravatar herbelin2011-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> ↵Gravatar herbelin2011-07-16
| | | | | | and <- when a variable is about to be substituted (subst_one rewrite the whole context at once, while multi_rewrite rewrites each hyp independently, what may break typing in case of dependencies). Also generalize "dependent rewrite" to "sig" (to be done: generalize it to eq_dep, eq_dep1, and any dependent tuple). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14279 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensured that the transparency state is used when flag betaiota is on for apply.Gravatar herbelin2011-06-19
| | | | | | | + small typo fix in r14217 + added compatibility of betaiota flag with 8.3 when "-compat 8.3" is given git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14223 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
| | | | | | | | | | | evars when rewriting. Use it for autorewrite and subst. Accept evars instantiation in multi_rewrite so that rewrite alone remains compatible (it is used in contribs, e.g. Godel, in places where it does not seem absurd to allow it), but there are no good reason for it. Comments welcome. + addition of some tests for rewriting (one being related to commit 14217) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
| | | | | | | | | | use_pattern_unification common for evars and metas. As a compensation, add a flag use_meta_bound_pattern_unification to restore the old mechanism of pattern unification for metas applied to rels only (this is used e.g. by auto). Not sure yet, what could be the most appropriate set of flags. Added documentation of the flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in CHANGESGravatar herbelin2011-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14216 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated CHANGES (info, Show Script, rephrasing).Gravatar herbelin2011-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14187 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing another bug with "_" intro pattern.Gravatar herbelin2011-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14185 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES updateGravatar pboutill2011-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: try to properly send interrupts to coqtop on Win32Gravatar letouzey2011-04-28
| | | | | | | | | | | | | | | We use GenerateConsoleCtrlEvent(CTRL_C_EVENT,...) after having attached coqide to the console of the coqtop we want to interrupt. Two caveats: - This code isn't compatible with Windows < XP SP1. - It relies on the fact that coqide is now a true GUI app, without console by default. If for some reason the console of coqide is restored (for instance via mkwinapp -unset), strange behavior of the interrupt button is to be expected, at the very least all instances of coqtop will get Ctrl-C instead of a precise one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14077 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating CHANGESGravatar herbelin2011-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug of destruct which was sometimes forgetting local definitions ↵Gravatar herbelin2011-04-24
| | | | | | behind it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
| | | | | | | | This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395Gravatar pboutill2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update documentation concerning proofs loading (cf last commit)Gravatar letouzey2011-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13954 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: a word about recent changes in coqide, about Ctrl-C in vmGravatar letouzey2011-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of the timeout tactical (cf r13917)Gravatar letouzey2011-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13921 85f007b7-540e-0410-9357-904b9bb8a0f7
* An option "Set Default Timeout n."Gravatar letouzey2011-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: mentionning quickly Separate ExtractionGravatar letouzey2011-03-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13892 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: update of syntax for annotations of functor applicationGravatar letouzey2011-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13871 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: improved indentation of extracted code (fix #2497)Gravatar letouzey2011-03-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For Haskell, we still try to provide readable indentation, but we now avoid relying on this indentation for correctness. Instead, we use layout-independant syntax with { } when necessary (after "case of" and "let"). It is much safer this way, even if the syntax gets a bit more cumbersome. For people allergic to {;}, they can most of the time do a tr -d "{;}" without changing the meaning of the program. Be careful nonetheless: since "case of" is now delimited, some parenthesis that used to be mandatory are now removed. Note also that the initial "module ... where" is still without { }: even when Format goes crazy it doesn't tamper with column 0. Other modifications: - Using "Set Printing Width" now affects uniformly the extraction pretty-printers. You can set a greater value than the default 78 before extracting a program that you know to be "really deep". - In ocaml (and also a bit in Haskell), we now try to avoid abusing of 2-char-right-indentation. For instance | is now aligned with the "m" of match. This way, max_indent will be reached less frequently. - As soon as a pretty-print box contains an explicit newline, we set its virtual size to a big number, in order to prevent this box to be part of some horizontal arrangement. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update changelogsGravatar glondu2011-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13834 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixpoints are traverse during implicits arguments search to toplevelGravatar pboutill2011-02-10
| | | | | | registration (& CHANGES update) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13826 85f007b7-540e-0410-9357-904b9bb8a0f7
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As said in CHANGES: << The inlining done during application of functors can now be controlled more precisely. In addition to the "!F G" syntax preventing any inlining, we can now use a priority level to select parameters to inline : "<30>F G" means "only inline in F the parameters whose levels are <= 30". The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. >> Nota : the syntax "Parameter Inline(30) foo" is equivalent to "Set Inline Level 30. Parameter Inline foo.", and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G." For instance, in ZBinary, eq is @Logic.eq and should rather be inlined, while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined. We could achieve this behavior by setting a level such as 30 to the parameter eq, and then tweaking the current level when applying functors. This idea of levels might be too restrictive, we'll see, but at least the implementation of this change was quite simple. There might be situation where parameters cannot be linearly ordered according to their "inlinablility". For these cases, we would need to mention names to inline or not at a functor application, and this is a bit more tricky (and might be a pain to use if there are many names). No documentation for the moment, since this feature is experimental and might still evolve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
| | | | | | | | | | | | | | | | According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGESGravatar pboutill2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13772 85f007b7-540e-0410-9357-904b9bb8a0f7
* First release of Vector library.Gravatar pboutill2010-12-10
| | | | | | | | | | To avoid names&notations clashs with list, Vector shouldn't be "Import"ed but one can "Import Vector.VectorNotations." to have notations. SetoidVector at least remains to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2Gravatar letouzey2010-12-09
| | | | | | | | | | | | | | | Now we have: - Zdiv and Zdiv2 : round toward bottom, no easy sign rule, remainder of a/2 is 0 or 1, operations related with two's-complement Zshiftr. - Zquot and Zquot2 : round toward zero, Zquot2 (-a) = - Zquot2 a, remainder of a/2 is 0 or Zsgn a. Ok, I'm introducing an incompatibility here, but I think coherence is really desirable. Anyway, people using Zdiv on positive numbers only shouldn't even notice the change. Otherwise, it's just a matter of sed -e "s/div2/quot2/g". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13695 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
| | | | | | | | | | | | | | | | | | | | | | | See NatInt/NZBits.v for the common axiomatization of bitwise functions over naturals / integers. Some specs aren't pretty, but easier to prove, see alternate statements in property functors {N,Z}Bits. Negative numbers are considered via the two's complement convention. We provide implementations for N (in Ndigits.v), for nat (quite dummy, just for completeness), for Z (new file Zdigits_def), for BigN (for the moment partly by converting to N, to be improved soon) and for BigZ. NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in the reversed order (for consistency with the rest of the world): for instance BigN.shiftl 1 10 is 2^10. NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2) on negative numbers. For the moment I've kept it intact, and have just added a Zdiv2' which is truly equivalent to (Zdiv _ 2). To reorganize someday ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document new tactics in CHANGESGravatar glondu2010-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13666 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: mention some changes in trunk since the 8.3 forkGravatar letouzey2010-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13655 85f007b7-540e-0410-9357-904b9bb8a0f7
* SearchAbout: who has never been annoyed by the [ ] syntax ?Gravatar letouzey2010-11-19
| | | | | | | | | | | | | | Well, hopefully, that belongs to the past: you should now be able to do the very same queries as before, without typing the [ ]. For instance: SearchAbout plus mult. This removal of [ ] is optional, the old syntax is still legal: - for compatibility reasons - for square bracket lovers - for those that have "inside" or "outside" as legal identifier in their development and want to search about them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13654 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: small re-sync with the one of branch v8.3Gravatar letouzey2010-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13653 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 20:35:26 +0000