| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
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).
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
|
| |
|
|
| |
Note that even "Load Verbose" is not supposed to display them.
|
| |
|
|
|
|
|
|
|
|
| |
The -verbose family of options is only meant to echo sentences as they are
processed. The patch below broke this, while fixing another issue. That
other issue will be fixed in the next commit.
Revert "Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its"
This reverts commit 2a28c677c3c205ff453b7b5903e4c22f4de2649b.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Goal 0=0 -> true=true.
intro H; rewrite H1.
was highlighting H1 but
Goal 0=0 -> true=true.
intro H; rewrite H.
was only highlighting the whole "intro H; rewrite H".
|
| |\ |
|
| | |
| |
| |
| | |
non-recursive notations (#4815).
|
| | |
| |
| |
| |
| |
| |
| | |
conversion on closed terms.
This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
g I. (* Was printing Top.Top#<>#1 *)
idtac; f I. (* Was not properly locating error *)
This is a "a minima" fix.
This a different fix than in trunk, so the merge will have to take the
trunk version.
|
| | |
| |
| |
| | |
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
|
| | |
| |
| |
| |
| |
| |
| | |
- In Program, a check_evars_are_solved was introduced
too early. Program does it's checking of evars by itself.
- In Function, the universe environments were not threaded
correctly.
|
| |/ |
|
| |
|
|
| |
obligations".
|
| | |
|
| | |
|
| |
|
|
| |
Also register properly the kind of definition.
|
| |
|
|
|
|
|
|
| |
When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
|
| |
|
|
| |
so that they are not silently computed when not in debugging mode.
|
| |
|
|
|
|
| |
Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
|
| |
|
|
| |
The user-provided sort was ignored for them.
|
| |
|
|
|
| |
As if we were adding : Type. Consistent with inductives with no
declared arity.
|
| |
|
|
| |
Forcefully equating it to the inferred level is not always desirable or possible.
|
| | |
|
| |
|
|
| |
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
| | |
|
| |
|
|
| |
multiple patterns.
|
| | |
|
| |
|
|
|
|
| |
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
|
| |
|
|
| |
Fixpoint/Definition.
|
| |
|
|
|
|
|
| |
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The previous behavior was to include the interface of such a functor,
possibly leading to the creation of unexpected axioms, see bug report #3746.
In the case of non-functor module with restricted signature, we could
simply refer to the original objects (strengthening), but for a functor,
the inner objects have no existence yet. As said in the new error message,
a simple workaround is hence to first instantiate the functor, then include
the local instance:
Module LocalInstance := Funct(Args).
Include LocalInstance.
By the way, the mod_type_alg field is now filled more systematically,
cf new comments in declarations.mli. This way, we could use it to know
whether a module had been given a restricted signature (via ":"). Earlier,
some mod_type_alg were None in situations not handled by the extraction
(MEapply of module type).
Some code refactoring on the fly.
|
| | |
|
| |
|
|
|
| |
The name in the return clause has no semantic meaning, we must not
look at it.
|
| |
|
|
|
| |
constraints at the time of Next Obligation/Solve Obligations so that
interleaving definitions and obligation solving commands works properly.
|
| |
|
|
|
|
|
| |
using the wrong context.
This is very bad style but currently unavoidable, at least we don't
throw an anomaly anymore.
|
| | |
|
| | |
|
| |
|
|
|
| |
non-polymorphic definitions, original universes might be substituted
later on due to constraints.
|
| | |
|
| |
|
|
|
|
| |
instances for each of the inductive in the same block but reuse the
original universe context shared by all of them. Also do not force
schemes to become universe polymorphic.
|
| |
|
|
|
| |
definition, if they manipulate structures depending on the initial state
of the context.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
When a future is fully forced (joined), the fix_exn is dropped,
since joined futures are values (hence they cannot raise exceptions).
When a future for a transparent definition enters the environment
it is joined. If one needs to pick its fix_exn, he should do it
before that.
|
| |
|
|
| |
involving Futures.
|
Hugo Herbelin
Guillaume Melquiond
Matthieu Sozeau
Pierre-Marie Pédrot
Matthieu Sozeau
Maxime Dénès
Pierre Letouzey
Enrico Tassi