| Age | Commit message (Collapse) | Author |
|---|
|
instances and forgeting about the evars and universes that could appear
there... dirty hack gone, using the evar map properly and avoiding
needless constructions/deconstructions of terms.
|
|
pattern_of_constr in an evar_map, as they can appear in the context
of said named metas, which is used by change. Not sure what to do in
the PEvar case, which never matches anyway according to Constr_matching.matches.
|
|
|
|
|
|
|
|
|
|
of plugins.
|
|
|
|
|
|
|
|
|
|
|
|
Of course such proofs cannot be processed asynchronously
|
|
|
|
typecheck with definitions and thread it accordingly when typechecking
module expressions.
|
|
This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
|
|
|
|
|
|
|
|
|
|
The ring ASTs were put in a separate interface, and only the
extension-related code was put in a dedicated G_newring file.
|
|
Since name clashes are discovered by side effects, the order of traversal of
module structs cannot be changed.
|
|
|
|
The control flow of extraction is hard to read due to exceptions. When meeting
an inlined constant extracted to custom code, they could desynchronize some
tables in charge of detecting name clashes, leading to an anomaly.
|
|
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
|
|
|
|
|
|
|
|
After this commit, module_type_body is a particular case of module_type.
For a [module_type_body], the implementation field [mod_expr] is
supposed to be always [Abstract]. This is verified by coqchk, even
if this isn't so crucial, since [mod_expr] is never read in the case
of a module type.
Concretely, this amounts to the following rewrite on field names
for module_type_body:
- typ_expr --> mod_type
- typ_expr_alg --> mod_type_alg
- typ_* --> mod_*
and adding two new fields to mtb:
- mod_expr (always containing Abstract)
- mod_retroknowledge (always containing [])
This refactoring should be completely transparent for the user.
Pros: code sharing, for instance subst_modtype = subst_module.
Cons: a runtime invariant (mod_expr = Abstract) which isn't
enforced by typing. I tried a polymorphic typing of mod_expr,
to share field names while not having mtb = mb, but the OCaml
typechecker isn't clever enough with polymorphic mutual fixpoints,
and reject code sharing (e.g. between subst_modtype and subst_module).
In the future (with ocaml>=4), some GADT could maybe help here,
but for now the current solution seems good enough.
|
|
In the case of an inner module without explicit signature,
(and not used later in a functor application), we now extract
only the needed items (used later or asked by the user),
instead of blindly extracting all fields as earlier.
|
|
Since type variables are local to the definition, we simply rename
them in case of unicode chars. We also get rid of any ' to avoid
Ocaml illegal 'a' type var (clash with char litteral).
|
|
|
|
- Common.get_native_char instead of just a pp function of this char
- Enrich the record projection table
|
|
|
|
Removing unused argument and fixing bug #3899, now warning when a record
cannot be made primitive in Set Primitive Projections mode because it
has no projection or at least one undefinable projection.
|
|
|
|
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
right-hand side of a "change with": the rhs lives in the toplevel
environment.
|
|
for Functional Induction was failing because of minus now an alias).
Knowing that minus is an alias for Sub.nat, there are still two bugs in
Functional Induction (Pierre or Julien?):
"Functional Scheme minus_ind := Induction for minus Sort Prop." is
failing when Nat is not imported.
"functional induction (minus n m)" is failing because looking for
sub_ind while the scheme is named minus_ind.
|
|
|
|
|
|
This new implementation now allows for simultaneous replacing of hypotheses,
thus fixing bug #2149.
|
|
|
