| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
|
|
|
|
| |
A priori considered to be a good programming style.
|
|\ |
|
| |
| |
| |
| | |
Mostly documentation and making a couple of local flags, local.
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
|
| |
| |
| |
| |
| |
| | |
Previously a union type was used for externing.
In particular, moving extended_glob_local_binder to glob_constr.ml.
|
| |
| |
| |
| | |
RawLocal -> CLocal
|
| | |
|
|/
|
|
|
|
| |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
|\ |
|
| |\ |
|
|\| | |
|
| | |
| | |
| | |
| | | |
(It should apply also interactively.)
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
#4363)."
This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402.
This fixes bug #4874. We fallback to the original error message of v8.4.
The fallback printer introduced in this commit only gave unqualified names,
which is what this bug reports.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The new name makes it more obvious what is meant here by "kind". We leave
Decl_kinds.binding_kind as a deprecated alias for plugin
compatibility.
We also replace bool with implicit_status in a few places in the
codebase.
|
| | |
| | |
| | |
| | | |
Suggested by @ppedrot
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- typo in notation_ops.ml
- factorization of patterns in ppconstr.ml
- update of test-suite
- printing of cast of a binding pattern if in mode "printing all"
The question of whether or not to print the type of a binding pattern
by default seems open to me.
|
| |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |
| |
| |
| | |
Cf CHANGES for details.
|
| |
| |
| |
| | |
implicit arguments when in beautification mode.
|
|\| |
|
| |
| |
| |
| |
| | |
We delay the externalization of application arguments in Constrextern,
so that they only get computed when they are actually explicitly displayed.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
functions about interpretation, internalization, externalization of
notations.
Main syntactic changes:
- subst_aconstr_in_glob_constr -> instantiate_notation_constr
(because aconstr has been renamed to notation_constr long time ago)
- extern_symbol -> extern_notation
(because symbol.ml has been renamed to notation.ml long time ago)
- documentation of notations_ops.mli
Main semantic changes:
- Notation_ops.eq_glob_constr which was partial eq disappears: use
glob_constr_eq instead
- In particular, this impacts a change on funind which now use the
(fully implemented) glob_constr_eq
Somehow, instantiate_notation_constr should be in notation_ops.ml for
symmetry with match_notation_constr but it is bit painful to do.
|
| |
| |
| |
| | |
This reverts commit 2211eeda012477b26081738fccc59aa31fb0a565.
|
| |
| |
| |
| | |
implicit arguments when in beautification mode.
|
|\ \
| | |
| | |
| | | |
into JasonGross-trunk-function_scope
|
| | | |
|
| | | |
|
|\ \ \ |
|
|\ \ \ \
| | |_|/
| |/| | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
|\| | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
I have removed the second field of the "Constrexpr.CRecord" variant
because once it was set to "None"
it never changed to anything else.
It was just carried and copied around.
|
| | |
| | |
| | |
| | |
| | | |
Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
|
|/ / |
|
| |
| |
| |
| | |
using dot notation.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The nametab in which the error message is printed is not the one in
which the error message happens.
This reveals a weakness in the fix_exn code: the fix_exn function should
be pure, while in some cases (like this one) uses the global state (the
nametab) to print a term in a pretty way (the shortest non-ambiguous name
for constants).
This patch makes the externalization phase (used by term printing)
resilient to an incomplete nametab, so that printing a term in the
wrong nametab does not mask the original error.
|
|/ |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
to display by default (see bc8a5357889 - 17 Oct 2014):
- not printing instances for let-in anymore even when expanded (since
they are canonical up to conversion)
- still printing x:=x in [x:=x;x':=x] when x is directly an instance
of another var, but not in [x:=x;x':=S x]
This can be discussed, but if ever this is to be changed, it should
not be printed in [x:=x;x:=?n] with ?n implicitly depending on x
(otherwise said, variables which are not displayed in instances of
internal evars should not contribute to the decision of writing
x:=x in the instance).
|
|
|
|
| |
printing functions touched in the kernel).
|
| |
|
|
|
|
| |
full instances.
|
|
|
|
| |
The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure.
|
|
|
|
|
|
|
|
|
|
|
| |
but the internal representation dropped let-in.
Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.
To do, there is still an extra @ in the constructor name that does not
need to be there.
|
|
|
|
|
|
|
|
| |
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
|