| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
reason, Ltac interpretation does not allow tactics of the following
shape : let x := bla in TacGeneric tac. Hence we force genargs to be
tactics and build the resulting hole tactic from scratch.
|
|
05d5f8b9065b0f5e0349cf3d39dd62ab99f30369
|
|
I restored this in the kernel, and added it to the checker. There is one last
source of non-uniformity, which is the Sort case in the checker (was not
present in the kernel). I don't know what this case covers, so it should be
reviewed.
|
|
Also, we need :=, so that it's evaluated immediately, rather than
becoming a self-recursive variable. This fixes the "Undefined variable
'C'" error that make keeps spewing.
|
|
|
|
|
|
hypothesis.
|
|
I should have updated everyone who committed since the migration to git (giving me a canonical email).
I've search git shortlog -s to ensure the best I could that there are no duplicate. I discovered that email addresses from the mailmap are uncapitalised whereas the unmodified addresses are not, creating two different authors for no reason. So, I've added some record to normalise the canonical email addresses when needed.
|
|
and #3204: Failure of hygiene condition.
It was sufficient to tweak a flag in the constr externalization...
|
|
mechanism of coqdep.
|
|
|
|
code checking allowed sorts for elimination.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The exact filename has to be written. This is coherent with the RefMan.
|
|
|
|
Made a synonymous of it ("Print Options").
Also reorganized a bit the section about flags and options in reference manual.
|
|
|
|
|
|
|
|
Omega now reuse the same inner variable names (Zvar0, Zvar1, ...)
at each run. This way, the obtained proof-terms on
two identical omega runs should be the same.
This wasn't always the case earlier:
- the two proofs were almost always convertible, but with distinct
variable names.
- in very rare situations, the two proofs could even be non-convertible.
Indeed, the omega engine use hash-tables which may be sensible to
the names in the (in)equality system and hence lead to different
solutions. Example of this behavior (with ocaml 4, whose default hash
function is different from ocaml 3.12, leading to a different behavior
here !) :
--------------------------------------------------------------------
Require Import Omega.
Lemma test1 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test2 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test3 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test4 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Check (eq_refl : test1 = test2). (* OK *)
Check (eq_refl : test1 = test3). (* OK *)
Check (eq_refl : test1 = test4). (* KO, test4 is different !! *)
--------------------------------------------------------------------
The old behavior could be restored with "Unset Stable Omega".
Thanks to Frédéric Loulergue for spotting this sensibility to
the underlying ocaml versions...
|
|
|
|
|
|
|
|
md5sum check remains not portable.
|
|
|
|
|
|
Thanks again Maximes.
This time the C value was stored in the env_(named|rel)_val of
the environment
|
|
considered files.
Original patch by Guillaume Allais.
|
|
|
|
|
|
|
|
|
|
Kudos to Maximes for finding the culprit in no time!
Values of type 'Pre_env.key' store in the OCaml state the 'address'
of an already evaluated constant in the VM's C state. Such values
are not sent to work processes. The worker is going to re-evaluate the
constant, but just once, since the cache is cleared only when the env is
marshalled (via ephemerons).
|
|
|
|
|
|
without"
This reverts commit bfe1141026da70d8f59cf47b5fe61ffc20a29f3c.
Conflicts:
proofs/proofview_monad.ml
This is potentially a temporary commit until a final decision is taken on hand-written versus extracted ocaml for the tactic monad. The hand-written implementation has a bug where the + tactical would not behave properly (I tried to find why, but couldn't: the hand-written implementation looks fine, but it isn't. Beats me).
There is a conflict with Pierre-Marie's commit 4832692: Fixing backtrace registering of various tactic-related try-with blocks.
|
|
|
|
|
|
Proof using can be followed by:
- All : all variables
- Type : all variables occurring in the type
- expr:
- (a b .. c) : set
- expr + expr : set union
- expr - expr : set difference
- -expr : set complement (All - expr)
Exceptions:
- a singleton set can be written without parentheses. This also allows
the implementation of named sets sharing the same name space of
section hyps ans write
- bla - x : where bla is defined as (a b .. x y) elsewhere.
- if expr is just a set, then parentheses can be omitted
This module also implements some AI to tell the user how he could
decorate "Proof" with a "using BLA" clause.
Finally, one can Set Default Proof Using "str" to any string that is
used whenever the "using ..." part is missing. The coding of this
sucks a little since it is the parser that applies the default.
|
|
|
|
It is not possible to add shortcuts with arbitrary modifiers and to
save into a state some data, like the line offset for C-n and the
killed text for C-k and C-y.
If you see that your favorite Emacs/PG shortcut is missing,
please tell me!
Currently supported shortcuts:
C-_ Undo
C-g Esc
C-s Search
C-e Move to end of line
M-e Move to end of sentence
M-a Move to beginning of sentence
C-n Move to next line
C-p Move to previous line
C-f Forward char
C-b Backward char
M-f Forward word
M-b Backward word
C-k Kill untill the end of line
M-d Kill next word
M-k Kill until sentence end
M-DELBACK Kill word before cursor
C-d Delete next character
C-y Yank killed text back
C-c C-RET Go to
C-c C-n Advance 1 sentence
C-c C-u Retract 1 sentence
C-c C-b Advance
C-c C-r Restart
C-c C-c Stop
C-c C-a C-p Print
C-c C-a C-c Check
C-c C-a C-b About
C-c C-a C-a Search About
C-c C-a C-o Search Pattern
C-c C-a C-l Locate
C-c C-a C-RET match template
C-x C-s Save
C-x C-c Quit
C-x C-f Open
|
|
The original idea was to send not the kernel name, but the file/line
to that CoqIDE could make the text an hyperlink to the file, exactly
as coqdoc generated HTML.
|
