| Age | Commit message (Collapse) | Author |
|---|
|
years and no one complained (fixes #10580).
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
for integers and natural nums
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
Reviewed-by: silene
|
|
|
|
|
|
|
|
|
|
complained (fixes #10580).
|
|
Underscores are used as prefix for accelerators in gtk. In particular,
double underscores are used to escape them. So, when applying a template,
underscores should be cleaned from the inserted text.
|
|
Reviewed-by: MSoegtropIMC
|
|
|
|
|
|
reductions (fixes #10560).
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
It has been deprecated since 8.4. The documentation was incorrect since
at least 8.5 (the last two arguments were ignored).
`Backtrack m n p` was a synonym for `BackTo m`
We also move `BackTo` handling to coqtop, since it is not meant to be
part of the document.
|
|
This lemma is lsl_add_distr (about “<<” rather than “>>”).
See lemmas bit_add_or and lor_lsr for related properties.
|
|
The documentation states:
- Norm means the term is fully normalized and cannot create a redex
when substituted
- Cstr means the term is in head normal form and that it can
create a redex when substituted (i.e. constructor, fix, lambda)
|
|
|
|
rewrite
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
The hang is caused by a failure in the interpretation by coqtop of the
command line option "-topfile filename" (this happens before a proper
XML communication is set up between coqtop and coqide).
The fix is a bit ad hoc. We copy in coqide the code for checking the
validity of a filename. We copy it to avoid adding a dependency in
either Names.check_valid or Stm.dirpath_of_file. We do a minimal check
(on the basename) while (if it hadn't added extra depencencies or code
duplication) it would have been more consistent to do the exact same
check as in Stm.dirpath_of_file.
|
|
Reviewed-by: Zimmi48
|
|
Simple cleanup: we make use of the `obligation_info` type alias in the
function generating it.
|
|
We make the interface to this function simpler, as a step towards
trying to remove the duplication of this function with the code in
`DeclareDef`.
|
|
We localize functions for constant saving that were used before in the
start hooks, but now they are called in the saving path in direct style.
No functional change.
|
|
Reviewed-by: gares
|
|
Pointed out by Gaëtan Gilbert.
|
|
We continue over the previous commit and remove redundant
`structured_fixpoint_expr` record in favor of the one used in the AST.
This removes some term-shuffling, tho we still have discrepancies
related to adjustments on the recursive annotation.
|
|
We turn the tuples used for (co)-fixpoints into records, cleaning up
their users.
More cleanup is be possible, in particular a few functions can now
shared among co and fixpoints, also `structured_fixpoint_expr` could
like be folded into the new record.
Feedback on the naming of the records fields is welcome.
This is a step towards cleaning up code in `funind`, as it is the main
consumer of this data structure, as it does quite a bit of fixpoint
manipulation.
cc: #6019
|
|
We register the ML tactics by hand using the low-level API.
|
|
href: coq/coq#9651
|
|
Ack-by: ejgallego
|
|
Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are
implemented in the kernel so that they can be used by OCaml code (e.g.,
extracted code) as the other primitives.
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: jfehrle
|
|
The ExtrOCamlInt63 module can be required to map primitives from the Int63
module to their OCaml implementation (module Uint63 from the kernel).
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: mattam82
|
|
Reviewed-by: gares
|
|
Gappa)
Reviewed-by: vbgl
|
|
Fixes #10300 and #10285.
|
|
We only want stdout, so if there's something in stderr it will both
make a wrong output and make it harder to debug.
|
|
The issue could be reproduced by doing "dune build
test-suite/misc/universes/all_stdlib.v" (from a clean build) which
would error 127 with no message.
- only redirect stdout so that in the future we will see error
messages
- put the script as a dependency (I guess it sometime succeeded when
copying the deps for the test suite happened before running it)
|
|
files and insert it into .rst files
Ack-by: Zimmi48
Ack-by: gares
Ack-by: ppedrot
|
|
The internal interpretation functions have been not used by funind
since some time.
|
|
and inserting it into the .rst files
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
