| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
|
|
|
|
We used to recompute all fresh named contexts for evars before this patch in
the push_rel_context_to_named_context function. This was incurring a linear
penalty and a memory explosion due to the reallocation of many arrays. Now, we
rather remember the context between evar creations by sharing it in the pretyping
environment.
This can be considered as a fix for bug #4964 even though we might do better.
|
|
|
|
This saves a quadratic allocation by replacing arrays with maps.
|
|
In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
|
|
|
|
We remove in particular a dubious use of an environment in fresh name
generation. The code was using the wrong environment in a function only
depending on the rel context which was resetted most of the time. This
might change the generated names in extremely rare occurences.
|
|
|
|
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
|
|
For better error messages. The API change is
backwards compatible, using a new optional argument.
|
|
Take advantage that the provided term is always a variable in Equality.is_eq_x.
|
|
We do not allocate a closure in the main loop, and do so only when needed.
|
|
We do not check for presence of a variable in a global definition when we know
that this variable was not present in the section.
|
|
We do not recompute shortest name identifier for global references that were
already traversed. Furthermore, we share the computation of identifiers
between invokations of the name generating function.
This drastically speeds up detyping for huge goals, further mitigating the
shortcomings of the fix for bug #4777.
|
|
|
|
unshelve_goals is used to correctly register dependent
subgoals that have to be solved. Resolution may fail to
do so using hints, so we have to put them back as goals
in that case. The shelf is a good interface for doing that.
unifiable can be used outside proofview to detect dependencies
between goals. This might be better in another module.
|
|
Fix typo in proofview
|
|
|
|
This is the "error resiliency" mode for STM
|
|
|
|
|
|
|
|
|
|
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
|
|
|
|
|
|
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.
|
|
|
|
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.
|
|
|
|
|
|
|
