| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
It used not to be the case when the proof contains Sideff, since
the code was picking the last known state and not necessarily the
first one. Because of side effects the last known state could be
the one corresponding to the side effect (that was executed to, say,
change the parser). This is also related to bug #4530
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Originally, rel-context was represented as:
Context.rel_context = Names.Name.t * Constr.t option * Constr.t
Now it is represented as:
Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
| LocalDef of Names.Name.t * Constr.t * Constr.t
Originally, named-context was represented as:
Context.named_context = Names.Id.t * Constr.t option * Constr.t
Now it is represented as:
Context.Named.t = LocalAssum of Names.Id.t * Constr.t
| LocalDef of Names.Id.t * Constr.t * Constr.t
Motivation:
(1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
function which looked like this:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
Suppose that you do not know about rel-context and named-context.
(that is the case of people who just started to read the source code)
Merlin would tell you that the type of the value you are destructing
by "match" is:
'a * 'b option * Constr.t (* worst-case scenario *)
or
Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *)
To me, this is akin to wearing an opaque veil.
It is hard to figure out the meaning of the values you are looking at.
In particular, it is hard to discover the connection between the value
we are destructing above and the datatypes and functions defined
in the "kernel/context.ml" file.
In this case, the connection is there, but it is not visible
(between the function above and the "Context" module).
------------------------------------------------------------------------
Now consider, what happens when the reader see the same function
presented in the following form:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
to jump to the corresponding definition and learn more.
In this case, the connection is there, and it is directly visible
(between the function above and the "Context" module).
(2) Also, if we already have the concepts such as:
- local declaration
- local assumption
- local definition
and we describe these notions meticulously in the Reference Manual,
then it is a real pity not to reinforce the connection
of the actual code with the abstract description we published.
|
| |\| |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Originally, "VernacTime" and "VernacRedirect" were defined like this:
type vernac_expr =
...
| VernacTime of vernac_list
| VernacRedirect of string * vernac_list
...
where
type vernac_list = located_vernac_expr list
Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:
| VernacTime of located_vernac_expr
| VernacRedirect of string * located_vernac_expr
which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.
|
| | |
| |
| |
| |
| |
| | |
Actually, we never mix the various uses of each dynamic type created through
the Dyn module. To enforce this statically, we functorize the Dyn module so
that we recover a fresh instance at each use point.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
The "master" label used to be reset to the wrong id
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
involving Futures.
|
| | |
| |
| |
| | |
universes are declared correctly in the enclosing proofs evar_map's.
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
The splines=ortho option seems to make dot crash sometimes, so this commit
removes it from the STM debugging output
|
| | |
| |
| |
| | |
PIDEtop needs these to implement its new transaction mechanism
|
| | |
| |
| |
| |
| | |
This lets hooks treat different exceptions in different ways; in
particular, user interrupts can now be safely ignored
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
| | | |
|
| | | |
|
| |/
|
|
|
|
| |
The evar counter has been moved from Evarutil to Evd, and all functions in
Evarutil now go through a dedicated primitive to create a fresh evar from
an evarmap.
|
| |
|
|
|
| |
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
It showed up at the CoqCS.
|
| |
|
|
| |
Hence we reuse the ones in master.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
The command [Redirect "filename" (...)] redirects all the output of
[(...)] to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
No "read-only" terminator. If no terminator is present the UI
complains. If the terminator is different, STM warns but
continues. The STM warns that the "check the document" button
will not honor the terminator change, and what to do to avoid
that.
Technically, one cannot turn (a posteriori) an axiom into a theorem
and vice versa. Could be done, but not with a small patch.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
When a worker sends back a system state to master, it tries to
just send a delta. If the command is a simple tactic, then only
the proof state changes.
Now, what is a simple tactic?
1. a tactic
2. that does not change the environment
Check 1. was surely incomplete. Now it is:
VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _
Is it complete?
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is likely to make nested proofs containing proof modes switch
broken, but fixes the problems Arnaud has in his branch.
It is possible that the classification function we have today
is not fine grained enough.
If a command that changes the proof mode has as the only global
effect changing the proof mode, then the current code is fine.
If it has a more global effect that persists after the proof is over
but has no impact on the proof itself, then the old code is fine.
As far as I can get, the proof mode switching commands have
a global effect (changing parser) but also a proof effect
(un/focusing). We don't have a classification for these.
Today a command having a global effect is played twice:
on the proof branch an on master. Of course if such command
cannot work on master (where there is no finished proof for
example) we need a special treatment for it.
|
| | |
|
| |
|
|
|
| |
It was detecting only the per-lemma Polymorphic flag,
but not the global one.
|
Enrico Tassi
Matej Kosik
Pierre-Marie Pédrot
Maxime Dénès
Guillaume Melquiond
Matthieu Sozeau
Hugo Herbelin
Alec Faithfull
Matthieu Sozeau
Clément Pit--Claudel