aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | | | | | | | | | | | | | | * | | | | | Moving setting of "cleared" evar flag directly in Evd.restrict.Gravatar Hugo Herbelin2017-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further.
| | | | | | | | | | | | | | | | | | * | | | | | Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
| | | | | | | | | | | | | | | | | * | | | | | Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
* | | | | | | | | | | | | | | | | | | | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | | | | look for Obligation num or Next Obligation to start proofGravatar Paul Steckler2017-09-26
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | * | | | | | | | | Properly display the "only" prefix for selectors (bug #5760).Gravatar Guillaume Melquiond2017-09-26
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit also fixes range selectors being incorrectly displayed.
| | | | | | | | | | | * | | | | | | | | Fixing a little parsing bug with level 90 introduced in 3e70ea9c.Gravatar Hugo Herbelin2017-09-25
| | | | | | | | | | |/ / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unfortunately, some manual synchronization is needed between the constr parser and the table of constr/pattern levels. We do this synchronization which was missing in the commit moving "x -> y" to a user-level notation.
| | | | | | | | | | | | | | | * / / / [doc] Update INSTALL to match reality.Gravatar Emilio Jesus Gallego Arias2017-09-25
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [c.f] https://coq.inria.fr/bugs/show_bug.cgi?id=4270
* | | | | | | | | | | | | | | | | | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | inductive types)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | let-ins and non-recursively uniform parameters
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1079: Avoid generated names for html pages of the reference manual ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (bug #4742).
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 4e70791).
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1057: Reporting locations in error messages about notation formats.Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1060: An optimization of tactic constructorGravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1075: Re-enable checker error messagesGravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | * | | | | | | | | | | | | | | | | Discharge.ml: cosmetic renaming of some variables.Gravatar Hugo Herbelin2017-09-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The point is to emphasize stronglier when we are talking about contexts or about arguments.
| | | | | | | * | | | | | | | | | | | | | | | | Fixing #5755 (discharging of inductive types not correct with let-ins).Gravatar Hugo Herbelin2017-09-23
| |_|_|_|_|_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The number of effective parameters was used where the number of declarations in the signature of parameters should have been used.
| | | | | | | | | | | | | | | * | | | | | | | After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.Gravatar Hugo Herbelin2017-09-23
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Printing metas still happens relatively often. From the user point of view, no need to know that it is different from an evar, so the notation ?M42 as it was before is much lighter. As for developers looking for debugging information, they will easily suspect that it is internally a meta because of the "M". This reverts "Proposing meta names more distinguishable from evar names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead).
| | | | * | | | | | | | | | | | | | | | | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Gravatar Hugo Herbelin2017-09-23
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | * | | | | | | | | | | | | | | | Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Gravatar Hugo Herbelin2017-09-23
| |_|_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The bug was caused by an inconsistency in different part of the code for deciding where cutting the context in between recursively uniform parameters and non-recursively uniform ones when let-ins were in the middle. We fix it by using uniformly "context_chop".
| | | | | | | | | | | | * | | | | | | | | Remove some unused parts of the reference manual.Gravatar Guillaume Melquiond2017-09-22
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | | | Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
| |_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * | Himsg: Dropping nf_evars made obsolete by EConstr.Gravatar Hugo Herbelin2017-09-22
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * | Cannot unify message: improve preventing repeating twice the same message.Gravatar Hugo Herbelin2017-09-22
| | | | | |_|_|_|_|_|_|_|_|_|_|_|/ / | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Call to nf_betaiota was done on one side of the comparison preventing the same message to be repeated twice but not on the other side.
| | | | | | * | | | | | | | | | | | Make a test for coq_makefile portable.Gravatar Pierre-Marie Pédrot2017-09-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The validity of this test depended on Makefile issueing warnings in English. We simply force the global language of the shell to be C.
* | | | | | | | | | | | | | | | | | Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | expected.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | context obtained by ltac pattern-matching)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated.Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1070: Remove remaining occurrences of -just-parsing.Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdirGravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1063: [flags] Flag `open Flags`Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1061: Fix appveyor buildGravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | * | | | | Report missing arguments in error messageGravatar Tej Chajed2017-09-21
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753.
| | | | | | | | | | | | | | | | | | * | | | | | | Properly handle "coq_makefile -Q . Foo" (bug #5580).Gravatar Guillaume Melquiond2017-09-21
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | | | Fix -silent flag of coqchk after ff918e4.Gravatar Maxime Dénès2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | | | Adapt checker to change in locations.Gravatar Maxime Dénès2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | * | | | | | | | | | | | | | | | | | Proposing meta names more distinguishable from evar names than ?M42.Gravatar Hugo Herbelin2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability. Tough maybe it signals too much an unelegant debugging flavor?
| | | | | | * | | | | | | | | | | | | | | | | | A possible fix to BZ#5750 (ability to print context of ltac subterm match).Gravatar Hugo Herbelin2017-09-21
| | | | | | | |_|_|_|_|/ / / / / / / / / / / / | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1".
| | | | | | | | | * | | | | | | | | | | | | | [checker] Add missing Feedback printer (BZ#5587)Gravatar Emilio Jesus Gallego Arias2017-09-21
| |_|_|_|_|_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes longstanding bug likely introduced in the first `pp` to `Feedback` migration, namely the checker didn't register a feedback printer, thus no calls to `Feedback.msg_*` were printed in the checker. This closes bug: https://coq.inria.fr/bugs/show_bug.cgi?id=5587 We fix this by adding a custom printer to the checker, this is correct as the checker owns now the full console, however a cleanup should happen in any of these two directions: - all the calls to feedback are removed, and the checker always uses its own printing mechanism. - all the calls to `Format/Printf` are removed and the checker always uses the `Feedback` mechanism. Currently, I have no opinion on this.
| | | | | | | | | | | | | | | * | | | | | | Do not run Travis OS X packaging job on PRsGravatar Théo Zimmermann2017-09-21
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This job was useless anyway because the depoly and pre-deploy phases were not run.
| * | | | | | | | | | | | | | | | | | | | Do not reinstall preinstalled packages under AppVeyor.Gravatar Maxime Dénès2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It seems that reinstalling gcc can leave Cygwin in a strange state, where invocations of gcc fail suddenly. I haven't figure out exactly why, but this seems to fix it.
| * | | | | | | | | | | | | | | | | | | | Print Cygwin setup output rather than logging in to a file.Gravatar Maxime Dénès2017-09-21
|/ / / / / / / / / / / / / / / / / / / /
| | | | * / / / / / / / / / / / / / / / Mark "Set Tactic Compat Context" as deprecated.Gravatar Guillaume Melquiond2017-09-21
| |_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was introduced in 8.5 for compatibility with a 8.4 bug.
| | | * | | | | | | | | | | | | | | | Remove remaining occurrences of -just-parsing.Gravatar Guillaume Melquiond2017-09-21
| |_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * Improve support for "-w none" compatibility option.Gravatar Guillaume Melquiond2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | If coqtop was started with "-w none" yet the script used "Set Warnings Append", then all the warnings were turned back to their default value. This commit turns "none" (whatever its sign) into "-all" whenever some warning status is modified afterward, in order to prevent the issue.
| | | | | | | | | | | | | | | | | * Handle multiple -w options on command line (bug #5736).Gravatar Guillaume Melquiond2017-09-21
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | |
| | | | * | | | | | | | | | | | | In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gravatar Gaëtan Gilbert2017-09-20
| |_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | | coq_makefile: dont show errors from failed (ignored) rmdirGravatar Ralf Jung2017-09-20
| |/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | |
| | | | | | | | | | | | * | | ssr: fix canonical strucut key comparison with primproj onGravatar Enrico Tassi2017-09-20
| | | | | | | | |_|_|_|/ / / | | | | | | | |/| | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-15 06:21:07 +0000