| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We force the STM to finish after the initialization request so as to raise
exceptions that may have been generated by the initialization process. Likewise,
we simply die when the initialization request fails in CoqIDE instead of just
printing an error message.
This is the fix for the underlying issue of bug #4591, but it does not solve
the bug yet.
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.
Some missing comments were added to the *.mli file.
The output of ocamldoc was checked whether it looks in a reasonable way.
"TODO: cleanup" was removed
The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)
The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)
The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)
The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})
The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.
Thrown exceptions are now documented.
Naming of formal parameters was made more consistent across different functions.
Comments of similar functions in different modules are now consistent.
Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
we can see the comments also there and do not need to open a different file if we want to see it.)
When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)
"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)
An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
|
| | | | |
|
| | | | |
|
| |\ \ \
| | |/
| |/|
| | |
| | | |
Conflicts:
lib/cSig.mli
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
bug #4477)
The bug was a bit subtle. Function process_cmd_line can be called in three
different ways:
1. tail-recursively to accumulate parsed options in reverse order,
2. directly to parse a file (coqide) or a command line (coq_makefile),
3. recursively to handle a "-f" option.
Once its execution finished, the function reversed its accumulator so
that the parsed options are in correct order. Due to the third case, this
means that the final local order of options was depending on the parity of
the depth of "-f" options. This commit fixes it by changing the function so
that the recursive call gets the actual accumulator rather than its
reversed version.
Warning: this will break all the projects that were inadvertently (or not)
relying on the bug. This might also require a further commit if
coq_makefile itself was relying on the bug.
|
| | | |
| | |
| | |
| | |
| | | |
Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |/
|/| |
|
| |\| |
|
| | |
| |
| |
| |
| | |
Force failing when reaching end of file with unterminated comment when
parsing Make (project) file.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the
fix to trunk instead.
This reverts commits:
490160d25d3caac1d2ea5beebbbebc959b1b3832.
ef8718a7fd3bcd960d954093d8c636525e6cc492.
6f9cc3aca5bb0e5684268a7283796a9272ed5f9d.
901a9b29adf507370732aeafbfea6718c1842f1b.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
This removes 109 Obj.magic in one patch!
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
These options can be set to a string value, but also unset.
Internal data is of type string option.
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
On most systems (including Windows, according to the bug report), shortcuts
Ctrl+Alt+Arrows are preempted by the window manager by default. So don't
use them for navigation in Coqide by default. Note that this change only
has an impact when installing on a fresh system; it won't change anything
for existing users.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
There is no remaining hook in the preferences. In particular, the
refresh_editor_hook is gone.
|
| | |
| |
| |
| |
| | |
There is no remaining global preference record anymore, every preference
is now defined in the new event-based style.
|
| |\| |
|
Pierre-Marie Pédrot
Enrico Tassi
Matej Kosik
Maxime Dénès
Guillaume Melquiond
Hugo Herbelin