aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
| | | | | | | | | | | | | | | | | | | | | The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add *a lot* of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs.
* Fix bug #5139: Anomalies should not be caught by || / try.Gravatar Pierre-Marie Pédrot2016-10-14
| | | | | There was a catch-all clause in the tclORELSE0 function. We now only catch noncritical exceptions.
* Fixing English typography for colon.Gravatar Hugo Herbelin2016-10-14
|
* Using "simple apply" and "simple eapply" in the trace of auto.Gravatar Hugo Herbelin2016-10-14
| | | | | This is more precise and probably clearer (see e.g. thread "Understanding auto" on coq-club).
* Completing reverting generalization and cleaning of the return clause inference.Gravatar Hugo Herbelin2016-10-13
| | | | | Revert "Inference of return clause: giving uniformly priority to "small inversion"." This reverts commit 980b434552d73cb990860f8d659b64686f6dbc87.
* Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2016-10-12
|
* Merge PR #224 into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\
* \ Merge PR #289 into v8.6.Gravatar Pierre-Marie Pédrot2016-10-12
|\ \
* \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \ \
* \ \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \ \ \
* | | | | Tentatively preparing to add changes specific to v8.7 (see PR #275).Gravatar Hugo Herbelin2016-10-12
| | | | |
* | | | | Little addition to 6eede071 for consistency of style in OrdersFacts.v.Gravatar Hugo Herbelin2016-10-12
| | | | |
| | * | | Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-10-12
| | | | | | | | | | | | | | | | | | | | | | | | | This happens when recursive notations are used to define recursive notations.
| | * | | Merge remote-tracking branch 'github/pr/286' into v8.5Gravatar Maxime Dénès2016-10-12
| | |\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | Was PR#286: Fix the definition of if_then_else for tactics with multiple success.
* | | | | | Fix bug #5116: [Print Ltac] should be able to print strategies.Gravatar Pierre-Marie Pédrot2016-10-12
| | | | | |
* | | | | | Fix git recognition when in worktrees.Gravatar Théo Zimmermann2016-10-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | git worktrees have a .git file instead of a .git directory. Using Sys.file_exists is a more general solution which gives true in both cases.
* | | | | | Fix bug #4958: [debug auto] should specify hint databases.Gravatar Pierre-Marie Pédrot2016-10-12
| | | | | |
* | | | | | Shorter message for "Test Asymmetric Patterns".Gravatar Hugo Herbelin2016-10-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | But maybe it is that how the "Test" message is elaborated is not intuitive...
| | * | | | Merge remote-tracking branch 'git/bug5123' into v8.5Gravatar Matthieu Sozeau2016-10-12
| |/| | | |
* | | | | | Fixing a few confusions on the name of the beautify flag.Gravatar Hugo Herbelin2016-10-12
| | | | | | | | | | | | | | | | | | | | | | | | (It should apply also interactively.)
| | * | | | Fix test-suite file 5123 to fail in case of regressionGravatar Matthieu Sozeau2016-10-11
| | | | | |
| * | | | | Merge remote-tracking branch 'github/bug4863' into v8.5Gravatar Matthieu Sozeau2016-10-11
| |\ \ \ \ \
| | | * | | | Fix bug #5123: mark all shelved evars unresolvableGravatar Matthieu Sozeau2016-10-11
| | |/ / / / | |/| | | | | | | | | | | | | | | | | | | | | | Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
* | | | | | Reverting generalization and cleaning of the return clause inference in v8.6.Gravatar Hugo Herbelin2016-10-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The move to systematically trying small inversion first bumps sometimes as feared to the weakness of unification (see #5107). ---- Revert "Posssible abstractions over goal variables when inferring match return clause." This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94. Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given." This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548. Revert "Trying a no-inversion no-dependency heuristic for match return clause." This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
| | * | | | Fix for bug #4863, update the Proofview's env withGravatar Matthieu Sozeau2016-10-11
| |/ / / / | | | | | | | | | | | | | | | | | | | | side_effects. Partial solution to the handling of side effects in proofview.
* | | | | Fixing #5133 (error reporting delayed).Gravatar Hugo Herbelin2016-10-10
| | | | | | | | | | | | | | | | | | | | | | | | | I wrongly moved call to the function interpreting commands within a different try-with block in 8a8caba36e.
| * | | | Add test file for #4416.Gravatar Maxime Dénès2016-10-10
| | | | |
| * | | | Fix #4416: - Incorrect "Error: Incorrect number of goals"Gravatar Arnaud Spiwack2016-10-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
* | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-09
|\| | | |
| * | | | A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).Gravatar Hugo Herbelin2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | More precisely, commands that calls parse_entry put the lexer in an inconsistent state, breaking the lexing of bullet which relies on it. (Not to be pushed to v8.6 which has a better fix).
* | | | | Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | done by the Ppcmd_comment token) and so that lexing/parsing side-effects are collected at the same place, i.e. in CLexer.
* | | | | Attaching all extra imperative components of the lexer/parser state toGravatar Hugo Herbelin2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | the state of parsable streams, so that different lexing/parsing processes can be started independently without conflicting. Note however that these different lexing/parsing processes cannot be run concurrently as they still work on the same piece of global memory (i.e. calls to entry_parse should remain atomic). To go further, one would typically need to be able to functionally pass the lexing state to each call to the lexer. Note that currently the beautifier is also running in the context of a lexer/parser state (for the mapping of location to comments). In particular, this fixes #5102 (parsing/lexing of bullets depending on the lexing state which was global).
* | | | | Fixing beautification to file.Gravatar Hugo Herbelin2016-10-09
| | | | |
* | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-08
|\| | | |
* | | | | Adding debugging printer for Genarg.ArgT.t.Gravatar Hugo Herbelin2016-10-08
| | | | |
* | | | | Report about changes of semantics of auto as an ltac argument (see #4966).Gravatar Hugo Herbelin2016-10-08
| | | | |
* | | | | Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.Gravatar Pierre-Marie Pédrot2016-10-08
| | | | |
* | | | | Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We defactorize the in_clause grammar entry to allow parsing of the "symmetry" tactic when it has no arguments. Beforehand, the clause_dft_concl entry accepted the empty stream, preventing the definition of symmetry as a mere identifier.
* | | | | Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Gravatar Pierre-Marie Pédrot2016-10-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We simply catch the RetypeError raised by the retyping function and translate it into a user error, so that it is captured by the tactic monad instead of reaching toplevel.
* | | | | Fix bug #5125: Bad error message when attempting to use where with Class.Gravatar Pierre-Marie Pédrot2016-10-07
| | | | |
* | | | | Do not add "Append" as a lexer keyword.Gravatar Pierre-Marie Pédrot2016-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was introduced to implement the Append feature on options. As usual when messing with predefined keywords, this broke code in the wild. In order not to create a new keyword, we do the string analysis on the production branch of parsing.
* | | | | Disable compatibility notations warnings.Gravatar Maxime Dénès2016-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Enablnig them would give a system that tells the user to replace e.g.: le_n_Sn with Nat.le_succ_diag_r lt_S with Nat.lt_lt_succ_r (on other types like R and and positive, the same lemma is called lt_lt_succ) In many cases, the new names will be too painful for intensive users.
| * | | | evarconv.ml: Fix bug #4529, primproj unfoldingGravatar Matthieu Sozeau2016-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that.
* | | | | Removing a slow access to a named environment.Gravatar Pierre-Marie Pédrot2016-10-06
| | | | |
| * | | | w_merge: Add a comment about the (List.rev evars)Gravatar Matthieu Sozeau2016-10-06
| | | | | | | | | | | | | | | | | | | | This change exposed bug #4763
* | | | | Remove the -no-compat-notations flag.Gravatar Maxime Dénès2016-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This option was not doing anything... Today, one can turn the compatibility notations warning into an error, if ever that was the intended semantics.
* | | | | Remove the Set Verbose Compat option and turn the warning on by default.Gravatar Maxime Dénès2016-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | These warnings can now be configured like any other, so we don't need a specific option anymore.
| * | | | unification.ml: fix for bug #4763, unif regressionGravatar Matthieu Sozeau2016-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too.
* | | | | Fixing unexpected "noise" introduced in commit 24d5448c.Gravatar Hugo Herbelin2016-10-06
| | | | | | | | | | | | | | | | | | | | A file was introduced by mistake in theories/Logic.
* | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-05
|\| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 22:02:09 +0000