| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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?
|
|
|
|
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
|
|
and 8388851 non-constant constructor.
|
|
|
|
change the representation of inductive constructor
when there is too many non constant constructors in the inductive type
Conflicts:
kernel/cbytegen.ml
|
|
|
|
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.
|
|
more than 245 constructors (unsupported by OCaml's runtime).
|
|
Module substitution is made nodewise, allowing to drop it for opaque terms
in the VM. This saves a few useless substitutions.
|
|
|
|
|
|
|
|
presence of let-ins and recursively non-uniform parameters).
The bug was in the List.chop of Inductiveops.get_arity which was wrong
in the presence of let-ins and recursively non-uniform parameters.
The bug #3491 showed up because, in addition to have let-ins, it was
wrongly detected as having recursively non-uniform parameters.
Also added some comments in declarations.mli.
|
|
number of recursively uniform parameters in the presence of let-ins.
In practice, more recursively non-uniform parameters were assumed and
this was used especially for checking positivity of nested types,
leading to refusing more nested types than necessary (see Inductive.v).
|
|
bug #4133)
Note that, if someone was purposely modifying the user name of a type in
order to disable a coercion, it no longer works. Hopefully, no one did.
|
|
|
|
|
|
|
|
|
|
presence of let-ins. This fixes #3491.
|
|
Parameters were missing in the context, apparently without negative
effects because the context was used only for whd normalization of
types, while reduction (in closure.ml) was resistant to unbound rels.
See however next commit for an indirect effect on the wrong
computation of non recursively uniform parameters producing an anomaly
when computing _rect schemas.
|
|
This gives more safety in object manipulation, as we delimit the uses
of Obj functions, and allows for an alternative implementation of the
representation of OCaml structures.
|
|
|
|
|
|
This reverts commit 124734fd2c523909802d095abb37350519856864.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
It was detecting only the per-lemma Polymorphic flag,
but not the global one.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(Fix for bugs #3470 and #3694)
|
|
In PG there are shortcuts that perform on the fly "Set Printing
All"/"Unset Printing All" in pg. For example if you type C-u before
some shortcut for print (check/About/Show), it performs:
Set Printing All.
Print foo.
Unset Printing All.
But if the "Unset" prints a goal, then pg interprets the output of
Print as a command applied on a previous line, and thus hides it.
So for emacs mode I would prefer no goal printing when options are
set/unset. In the situation where this should be done (when setting
durably the option probably), I'd rather program a "Show" explicitely.
|
|
|
|
|
|
|
|
|
|
It is still present in the libstack, though.
|
|
We explicit the fact that we only need the name of the library in most of the
summaries.
|
|
`.tar.gz`.
|
|
Cherry-picked from v8.4 ( c1aabb104122ead02fa289339a42815373338222 ).
|
