| Age | Commit message (Collapse) | Author |
|---|
|
This allows building SerAPI and jsCoq using ocamlbuild.
|
|
Was PR#337: Fix arguments
|
|
Type annotations in unrelated binders were badly interfering with
detection of recursive binders in notations.
|
|
|
|
Instead of circumventing the problem on the caller's side, as was done
in Arguments, we simply avoid failing as there was no real reason for
this anomaly to be triggered. If the list of renamings is shorter than
the one of implicits, we simply interpret the remaining arguments as not
renamed.
|
|
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
|
|
|
It used to be Stateid.initial by default. That is indeed a valid
state id but very likely not the very best one (that would be
the tip of the document).
|
|
|
|
Was PR#338: Remove warning now that info_auto is fixed.
|
|
Removes a warning dating from 8.5 signaling that info_auto
and info_trivial are broken and advising to use Info 1 auto
instead. Now, these tactics are fixed and thus they can be
used again. They do not do exactly the same thing as
Info 1 auto and may be more useful for the learner.
|
|
|
|
|
|
This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6.
This behavior of refine has changed three times in recent years, so
let's take the time to make up our mind and wait for a major release.
Btw, onhyps=None is not a sane way to express that a tactic should be
applied to all hypotheses.
|
|
Was PR#334: Fix bug 5031 : should not be an anomaly
|
|
not an anomaly
|
|
|
|
|
|
Was PR#233: Fix a bug in error printing of unif constraints
|
|
Was PR#329: Fix #5127 Memory corruption with the VM
|
|
|
|
|
|
|
|
Was PR#301: Update .gitignore with new names for psatz caches.
|
|
Was PR#326: Extend documentation of auto
|
|
|
|
The bytecode interpreter ensures that the stack space available at some
points is above a static threshold. However, arbitrary large stack space
can be needed between two check points, leading to segmentation faults
in some cases.
We track the use of stack space at compilation time and add
an instruction to ensure greater stack capacity when required. This is
inspired from OCaml's PR#339 and PR#7168.
Patch written with Benjamin Grégoire.
|
|
+ a few improvements on 5f1dd4c40 (lexing of { and }).
|
|
This old compatibility hint database can be safely removed
now that coq-contribs do not depend on it anymore.
|
|
|
|
|
|
|
|
|
|
|
|
New fix. A bit less consistent with the spirit of this Makefile as we
list prerequisite files explicitly, but avoid to redo subsystems at
each call to "make" as with previous fix.
Other solutions from experts are welcome.
|
|
|
|
This assertion checked that two arguments in the same position were equal,
but in fact, since one might have already been reduced, they are only
convertible (which is too costly to check in an assertion).
|
|
When inserting a character in an already processed buffer, a message is
sent to Coq so that the proof is backtracked and the character is
inserted. If a second character is inserted while Coq is still busy with
the first message, the action is canceled, but the signal is no longer
dropped so that the second character is properly inserted.
|
|
|
|
|
|
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
|
|
|
|
Refine fix for bug #4763, fixing #5149
Tactic [Refine.solve_constraints] and global option
Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.
Fix test-suite files too.
|
|
Conversion problems are in a de Bruijn environment that may
include references to unbound rels (because of the way evars
are created), we patch the env to named all de Bruijn variables
so that error printing does not raise an anomaly. Also fix a minor
printing bug in unsatisfiable constraints error reporting.
HoTT_coq_117.v tests all of this.
|
|
Adds a compatibility flag so that the behavior of 8.5 can be obtained too.
Original commit:
unification.ml: fix for bug #4763, unif regression
Do not force all remaining conversions problems to be solved after
the _first_ solution of an evar. This was hell to track down, thanks
for the help of Maxime. contribs pass and HoTT too.
|
|
|
|
|
|
|
|
This is useful for debugging purposes.
|
|
This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a.
A good fix requires to review a bit the design of unification constraint
postponement, which we do in 8.6. We leave things as they are in 8.5 for
compatibility.
|
