| Age | Commit message (Collapse) | Author |
|---|
|
"This function is deprecated: the runtime system is now able to print
uncaught exceptions as precisely as Printexc.catch does. Moreover, calling
Printexc.catch makes it harder to track the location of the exception
using the debugger or the stack backtrace facility. So, do not use
Printexc.catch in new code."
|
|
|
|
|
|
|
|
Before this commit, coq-tex was reading the .v file and was guessing how
many lines from the coqtop output it should display. Now, it reads the
coqtop output and it guesses how many lines from the .v file it should
display. That way, coq-tex no longer needs to embed a parser; it relies
on coqtop for parsing.
This is much more robust and makes it possible to properly handle script
such as the following one:
Goal { True }
+ { False }.
{ left. exact I. }
As before, if there is a way for a script to produce something that looks
like a prompt (that is, a line that starts with "foo < "), coq-tex will be
badly confused.
|
|
|
|
|
|
|
|
|
|
The universe instance of the constant was simply dropped by the function
interpreting generalizing binders.
|
|
|
|
We postpone the rewriting of hypothesis until we actually commit to one
branch instead of doing it upfront.
|
|
This is only a heuristic and it might cause the tool to become awfully
confused if a line ends with "}" yet this is not the end of a tactic
block. Fixing it would require a full-blown Coq parser inside coq-tex.
Example of crazy output:
Coq < Goal { True }
Coq < 1 subgoal
============================
{True} + {False}
Coq < + { False }.
|
|
|
|
|
|
|
|
|
|
|
|
Commit dc438047 was a bit overlooked as it introduced a wrong comparison function
on term patterns in dnets. Strangely enough, it seems not to have wreaked havoc
that much compared to the severity of the error.
|
|
File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.
There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
|
|
|
|
|
|
When set, search results only display symbol names, instead of
displaying full terms with types. This is useful when the list of
symbols is needed by an external program, in particular for doing
completion in IDEs.
|
|
abbreviation not bound to an applied constructor as itself but rather
as a binding variable as it was the case for non-applied
constructor). This was broken by e5c02503 while fixed #3483 (Not_found
uncaught with a notation to a non-constructor).
|
|
|
|
This should actually probably be an anomaly, but I'm unsure the code
for decidability schemes is robust enough to dare it.
|
|
decidability scheme).
Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:
Set Decidable Equality Schemes.
Inductive a := A with b := B.
which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
|
|
|
|
|
|
|
|
"Print Module command shows module type expression incorrectly".
|
|
This patch implements the traversal of inductive definitions in the
traverse function of toplevel/assumptions.ml which recursively
collects references in terms. In my opinion, this fixes a bug (but it
could be argued that inductive definitions were not traversed on
purpose). I think that is not possible to use this bug to hide a
meaningful use of an axiom.
You can try the patch with the following coq script:
Axiom n1 : nat.
Axiom n2 : nat.
Axiom n3 : nat.
Inductive I1 (p := n1) : Type := c1.
Inductive I2 : let p := n2 in Type := c2.
Inductive I3 : Type := c3 : let p := n3 in I3.
Inductive J : I1 -> I2 -> I3 -> Type :=
| cj : J c1 c2 c3.
Inductive K : I1 -> I2 -> I3 -> Type := .
Definition T := I1 -> I2 -> I3.
Definition C := c1.
Print Assumptions I1.
Print Assumptions I2.
Print Assumptions I3.
Print Assumptions J.
Print Assumptions K.
Print Assumptions T.
Print Assumptions C.
Print Assumptions c1.
Print Assumptions c2.
Print Assumptions c3.
Print Assumptions cj.
The patch is a bit more complicated that I would have liked due to
the feature introduced in commit 2defd4c. Since this commit,
Print Assumptions also displays the type proved when one destruct
an axiom inhabiting an empty type. This provides more information
about where the old implementation of the admit tactic is used.
I am not a big fan of this feature, especially since the change in
the admit tactic.
PS: In order to write some tests, I had to change the criteria for
picking which axiom destruction are printed. The original
criteria was :
| Case (_,oty,c,[||]) ->
(* non dependent match on an inductive with no constructor *)
begin match Constr.(kind oty, kind c) with
| Lambda(Anonymous,_,oty), Const (kn, _)
when Vars.noccurn 1 oty &&
not (Declareops.constant_has_body (lookup_constant kn)) ->
and I replaced Anonymous by _. Indeed, an Anonymous name here could
only be built using the "case" tactic and the pretyper seems to always
provide a name when compiling "match axiom as _ with end". And I
wanted to test what happened when this destruction occurs in
inductive definitions (which is of course weird in practice), for
instance:
Inductive I4 (X : Type) (p := match absurd return X with end)
: Type -> Type :=
c4 : forall (q := match absurd return X with end)
(Y : Type) (r := match absurd return Y with end), I4 X Y.
The ability of "triggering" the display of this information only when
using the "case" tactic (and not destruct or pattern matching written
by hand) could have been a feature. If so, please feel free to
change back the criteria to "Anonymous".
|
|
The .png was ugly (less than 400px wide) and did not match the content of
the .fig file (e.g. presence of '$'). To improve things a bit, text is now
rendered by latex.
|
|
|
|
The quadratic behaviour of list searching probably appears with small
enough samples. With the advent of usable libraries in Coq, and thus many
possible dependencies, better be safe than sorry.
|
|
|
|
On Fedora, `which 2>&1 >/dev/null` doesn't silence stderr, while `which >/dev/null 2>&1` does.
|
|
|
|
|
|
The file seems to have been reintroduced by error by commit 012fe1a96, but
it was not compiled anyway.
|
|
|
|
|
|
Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
|
|
I was not seeing the warning due to the 10 deprecation warnings before
it...
|
|
|
|
|
|
|
|
unification in tactics.
The relaxing of occur-check was ok but was leading trivial problems of
the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into
?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems
was not any more able to deal with.
Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way,
so that it behaves as if the occur-check had not been restricted.
|
|
using closer naming strategies for naming variables in make_all_name_different
and when contracting trivial letins.
Not sure what the best policy is. Maybe the contraction process should
not invent names at al and let make_all_name_different do the job.
Maybe pretyping should name all rels which it pushes to environment
(with cases.ml paying attention to avoid clash).
The problem shows for instance with a PretypeError (... env, ... ,
ActualTypeNotCoercible (NotClean (... env ...)) message with two
copies of env which we don't if they are the same but which have to
share same names for similar rendering of the rels!
This was revealed e.g. by the error message of #4177.
|
|
This is a bug in a pretty old code, showing also in 8.3 and 8.4.
|
