| Age | Commit message (Collapse) | Author |
|---|
|
|
|
When generating the OS X Coq + CoqIDE bundle, hdiutil often produces error
5341. This seems to be a known bug on Apple's side, occurring for some sizes of
dmg files. We try to change the current (problematic) size by adding a file
full of random bits.
|
|
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
|
CQQ -> COQ
|
|
|
|
|
|
Function is_constructor was not properly fixed. Additionally, this fixes
a problem with the 8.5 interpretation of in-pattern (see Cases.v).
|
|
CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
|
|
"dev/printers.cma" to be loadable within "ocamldebug".
|
|
|
|
|
|
|
|
about the prehistory of Coq.
|
|
|
|
|
|
presence of hints modifying the context and of a "using" clause.
Incidentally opening Hints by default in debugger.
|
|
- Universes are now represented in the VM by a structured constant containing the
global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
constructor arguments, which has to be prevented.
Was showing up for instance when evaluating [cons _ list (nil _)] with
a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.
Patch written with Benjamin Grégoire.
|
|
polymorphic definitions.
- This implementation passes universes in separate arguments and does not
eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
|
|
|
|
Instead of brutally merging the whole evarmap coming from the clenv,
we remember the context associated to the hint and we only merge that tiny
part of constraints. We need to be careful for polymorphic hints though,
as we have to refresh them beforehand.
|
|
|
|
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
|
|
|
|
Adding Gérard's history file about V1-V5 versions.
|
|
|
|
|
|
The theories/ directory contains no cmi/cmxs files when native_compute is
disabled, so do not try to ship them.
|
|
|
|
too many of them).
|
|
|
|
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
|
|
|
|
This allows fatal_error to be used for printing anomalies at loading time.
|
|
|
|
This is actually not so perfect because of the lambdas in the return
clause which we would not like to look in.
|
|
for which there corresponding tag are greater than max_variant_tag.
The code is a merge with the patch proposed by Bruno on
github barras/coq
commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c
|
|
|
|
|
|
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
|
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
|
|
|
|
|
|
printing functions touched in the kernel).
|
|
|
|
|
|
|
|
|
|
|
|
Still unsure about .o file (should they be shipped for the native_compute
machinery or .cmxs suffice?)
|
|
|
