| Age | Commit message (Collapse) | Author |
|---|
|
Pretype_errors.PretypeError.
Instad of trying to print the exception, we raise it in the tactic monad.
|
|
|
|
This disables colors in emacs compilation buffer, which does not
support ansi colors by default.
|
|
|
|
coqc by default uses colors, this allows to disable it. Moreover,
colors are not yet correctly disabled when compiling from emacs (emacs
bugs?), making this option even more useful.
|
|
negated into -native-compiler.
|
|
Instead of checking if the native compiler directory exists before creating it,
we simply create it by default and catch the potential exception due to its
presence.
|
|
|
|
negated into -native-compiler.
|
|
expected lowercase/uppercase spelling (based on a patch by Pierre B.).
This should fix #2554 (and see also discussion on coq-club, May 2015).
|
|
|
|
It enhances bug #3527, as instead of raising an anomaly "Uncaught
exception Coercion.NoCoercion(_)", it now fails with a typing error.
|
|
|
|
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
|
|
|
|
|
|
|
For now, warnings are still ignored by default, but this may change. This
commit at least allows to print them whenever desired. The -w syntax is
also opened to future additions to further control the display of
warnings.
|
|
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
|
Internal error: Anomaly: Uncaught exception Not_found. Please report.
An evarmap was lost because of an unsound typing primitive.
|
|
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
|
|
|
|
|
level of details, and this option should certainly disappear
eventually).
|
|
the predicate, thus respecting the visual left-to-right top-down order
(see a45bd5981092).
This fixes CFGV.
|
|
|
|
List.nth_error and List.hd_error were the only remaining places in
the whole stdlib to use type "Exc" instead of "option" directly.
So let's simplify things and use option everywhere. In particular,
during teaching sessions about lists, we won't have anymore to explain
the (lack of) difference between Exc,value,error and option,Some,None.
This might cause a few incompatibilities in proof scripts, if they
syntactically expect "value" or "error" to occur, but this should
hopefully be very rare and quite easy to fix.
|
|
|
|
Oups, sorry, I should have compiled the stdlib in full. Not only
the ~polyprop wasn't propagated properly, but Matthieu made it be
false by default somewhere instead of true. Argl...
|
|
It accepts three distinct flags:
- "Lax", which is the default one, sets the old behaviour, i.e. a non-imported
hint behaves the same as an imported one.
- "Warn" outputs a warning when a non-imported hint is used. Note that this is
an over-approximation, because a hint may be triggered by an eauto run that
will eventually fail and backtrack.
- "Strict" changes the behaviour of an unloaded hint to the one of the fail
tactic, allowing to emulate the hopefully future import-scoped hint mechanism.
|
|
|
|
The ~polyprop argument wasn't propagated properly anymore,
leading the extraction to try to operate on situations it cannot
handle (yet). Cf Table.error_singleton_become_prop for more details.
Regression test added.
|
|
|
|
|
|
|
|
In compiler mode, only vernac.ml knows the current file name.
Stm.process_error_hook moved from Vernacentries to Vernac to
be bale to properly enrich the exception with the current file
name (if any).
|
|
|
|
|
|
We beta-iota normalize the type of the rewriting predicate to ensure that the
non-dependency in the arrow argument is meaningful. Otherwise, terms of the
form "forall x : A, (fun _ : A => P) x" generated by the retyping would confuse
the non-dependency heuristic.
|
|
|
|
|
|
|
|
preserving compatibility of subst after #4214 being solved.
|
|
(see #3695).
|
|
TACTIC EXTEND (based on user-given name).
|
|
|
|
Improving treatment of recursive equations compared to 8.4 (see test-suite).
Experimenting not to unfold local defs ever in subst.
(+ Slight simplification in checking reflexive equalities only once).
|
|
allow reusability of the implementation throughout the Coq codebase.
We effectively feature a generalized version of the logical monad where the
input state, the output state and the inner exception can be arbitrarily chosen.
This will allow for more efficient implementations of close variants of the
monad.
|
|
after patch for #4214 on subst needed to be repeated (see
857e82b2ca0d1).
|
|
|
