| Age | Commit message (Collapse) | Author |
|---|
|
Since commit 2f521670fbd, the Require "file" syntax was not used anymore by
coqtop but the code handling it was still there in coqdep. We finish the work
by erasing the remnant code.
|
|
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
|
Tracing with gdb by Alec Faithfull
|
|
|
|
|
|
|
|
In case we need to backtrack on universe inconsistencies when converting
two (incompatible) instances of the same constant and unfold them.
Bug reported by Amin Timany.
|
|
|
|
|
|
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
|
|
- Proper [family] implementation
- Use the tailor made hash function for Sorts.t in two places.
|
|
|
|
|
|
|
|
There are still two items I do not undertand fully (the last one about
-extra-phony, and the removal of external libraries at make clean time,
that I could not reproduce on a toy example.
|
|
|
|
|
|
|
|
This allows fatal_error to be used for printing anomalies at loading time.
|
|
May still be wrong on Windows, though.
|
|
|
|
We lambda-lift by hand the graph traversal functions in Univ to allocate
less closures.
|
|
Fixes bug 3936
This closes #73
|
|
|
|
This interface is promoted by the operf-macro tool
https://github.com/OCamlPro/operf-macro
which allows to run benchmarks of time and memory usage
of various OCaml programs.
Coq already has two ways to get Gc infos:
- the -m|--memory command-line flag prints the total heap words allocated
- the "Print Debug Gc" command prints much more information,
but in a Coq-implementation-defined format that is not suitable
for across-programs comparison
(also an environment variable allows to profile Coq runs on any .v,
in an non-intrusive way)
Note to the Github Robot:
This closes #75
|
|
Marshalled libraries are only loaded when needed and dropped thereafter.
This might be costly for Require inside modules, but such a practice is
discouraged anyway.
|
|
The first part only contains the summary of the library, while the second
one contains the effective content of it.
|
|
A worker should never have to access the still-to-be-proved
obligations. If that happens, raise an informative anomaly.
|
|
This type contains a few unmarshallable fields, which can cause STM
workers to break in unpleasant ways when running queries
|
|
maybe ca71714).
Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.
was working in 8.4 but was failing in 8.5beta2.
Note: Changes in tacintern.ml are otherwise purely cosmetic.
|
|
|
|
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
|
I used a low-level function, now changed to `msg_notice`.
|
|
|
|
|
|
|
|
|
|
|
|
Message to the github robot:
This closes #63
|
|
|
|
Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show
Intros] at the end of a proof:
Goal True. trivial. Show Intros.
|
|
This mirrors the existing extraction libraries for OCaml.
One wart: the extraction for [string] requires that the Haskell code
imports Data.Bits and Data.Char. Coq has no way to add extra import
statements to the extracted code. So we have to rely on the user to
somehow import these libraries (e.g., using the -pgmF ghc option).
See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189
Message to github robot: this commit closes #65
|
|
|
|
Ideally, the code should be shared between the various toplevels, but this
is a lot more work than just fixing a few strings.
|
|
|
|
|
|
"Conjecture" (see #4252).
|
|
Was making the study of bugs like #4139 painful.
Now printing a better error message when a compiled file is missing.
|
|
|
|
|
