| Age | Commit message (Collapse) | Author |
|---|
|
This (at least technically) solves the issue #4113 (see also #4329).
|
|
|
|
clause in pattern-matching or not.
|
|
|
|
This allows to reduce the dependencies of subproofs generated by any sequence
of tactics. Grants wish #4327.
|
|
|
|
|
|
Let-bindings were not taken into account, resulting in proof-terms way too
huge.
|
|
|
|
Previously, the kernel would silently fall back to standard conversion.
|
|
On 64 bits architectures, integers could have some of their 32 msb set to 1
internally in the VM. When read back to a Coq term, this was not observable. But
an equality test would fail. From the user point of view, the symptom was that
vm_compute; reflexivity would succeed but the subsequent Qed would fail.
Bug reported by Tahina Ramananandro.
|
|
ADDMULDIVINT31 was missing pops in some cases
|
|
|
|
The target creation process should eventually be automated, because it
is tedious and error-prone as witnessed by this commit.
|
|
"Fetching opaque proofs" notices are not printed by default anymore.
|
|
|
|
|
|
The previous extraction of [Z.div] for Haskell did not properly handle
divide-by-zero. Fix it by introducing an explicit [if] statement in the
generated Haskell code.
Also, introduce a similar extraction rule for [Z.modulo], with the same
check for modulo-by-zero.
|
|
The previous extraction of [Nat.div] for Haskell did not properly handle
divide-by-zero. Fix it by introducing an explicit [if] statement in the
generated Haskell code.
Also, introduce a similar extraction rule for [Nat.modulo], with the same
check for modulo-by-zero.
|
|
Hugo Herbelin proposed to modify directly the function
"check_correct_par" to simplify commit c12b430
(see the pullrequest's discussion).
Note that the constructor "LocalNonPar" has now three arguments (instead
of two). In LocalNonPar (n,i,l) n denotes the position among real
arguments (ie. ignoring letins), i is the rel index of the expecting argument
in the context of parameters and l is the index of the inductive.
|
|
|
|
I do not think that this information is worth displaying without
the verbose flag.
|
|
Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d
were generated by a call to coqdep using the argument -c (for ocaml
code). While doing some finetuning of the generation of implicit rules,
this commit removed (I think by mistake) this "-c". And without this
-c argument coqdep output nothing on mllib files leading to incorrect
linking of mllibs.
|
|
In PIDE based UIs queries can be delegated too, hence to speed up
things I was saving a shallow state. Unfortunately a shallow state
breaks section/modules commands, and a query can be the last entry
of a section/module. (A shallow state does essentially drop the libstack).
The easy solution is to save a complete state.
A better one would be to refine the static analysis of the document and
decide which kind of saved state one needs.
|
|
There is no remaining hook in the preferences. In particular, the
refresh_editor_hook is gone.
|
|
|
|
(48d611ff2a).
|
|
There is no remaining global preference record anymore, every preference
is now defined in the new event-based style.
|
|
This commit is chiefly about moving code around to ease readability.
|
|
|
|
Grants wish #2098.
|
|
|
|
I don't know what was the intent of Pierre B here. In 8.4, it was not
supported, raising with an error at parsing time. I changed the
anomaly into an error at interpretation time, so it is still not
supported but we could support it if some legitimate use of it
eventually appears.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
A lot of legacy code has been removed in the process in favour of
signal-based interactions.
|
|
We use uniform functions instead of code duplication.
Likewise, we disentangle the hook mechanisms by using
callbacks connected to preferences instead.
Only the easy hook bits were removed. The most awing one,
the editor refreshing hook, is still alive.
|
|
Some old style references remain because all type converters are not
implemented yet.
|
|
We use a class-based system instead of the old record-based system. This
allows for more uniformity and the possibility to define complex
interactions with preferences based on GTK signals. This will allow to
simplify some architectural choices.
|
|
Correcting the code w.r.t. to the API was not the right solution. Instead,
the API comment had to be corrected.
|
|
We ensure statically by typing that the tags used by the rich printer
are integers. Furthermore, we also expose through typing that tags are
irrelevants in the returned XML.
|
|
|
|
|
|
Contrarily to what was described in the API, nodes without annotations
were not ignored by the printer but left there instead.
|
|
|
|
This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)). It is
useful to have function_scope for, e.g., function composition. This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.
Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax. (The scope type_scope
should not be special-cased; this change is coming up next.)
Also explicitly define [function_scope] in theories/Init/Notations.v.
This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]
We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.
|
