| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
there is an ocamlopt compiler.
|
|
compiler. In any case, try to build a cmo file.
|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
effects
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
We take inspiration and code from the Evil plugin.
|
|
following the model of `pose (x:=t)`.
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
"where"-based notation
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
constants.
Reviewed-by: herbelin
|
|
Reviewed-by: vbgl
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
This PR refactors the handling of ML loadpaths to get it closer to
what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does.
This is motivated as I am leaning toward letting the standard OCaml
machinery handle OCaml includes; this has several benefits [for
example plugins become regular OCaml libs] It will also help in
improving dependency handling in plugin dynload.
The main change is that "recursive" ML loadpaths are no longer
supported, so Coq's `-I` option becomes closer to OCaml's semantics.
We still allow `-Q` to extend the OCaml path recursively, but this may
become deprecated in the future if we decide to install the ML parts
of plugins in the standard OCaml location.
Due to this `Loadpath` still hooks into `Mltop`, but other than that
`.v` location handling is actually very close to become fully
independent of Coq [thus it can be used in other tools such coqdep,
the build system, etc...]
In terms of vernaculars the changes are:
- The `Add Rec ML Path` command has been removed,
- The `Add Loadpath "foo".` has been removed. We now require that the
form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used.
We did modify `fake_ide` as not to add a directory with the empty
`Prefix`, which was not used. This exposed some bugs in the
implementation of the document model, which relied on having an
initial sentence; we have workarounded them just by adding a dummy one
in the two relevant cases.
|
|
- zify_iter_specs is entirely in OCaml
- zify_op has been improved
* The generation of proof-terms is more direct
* It does not `rewrite` but instead either performs
a `pose proof` or a `change`
* The support for `and`, `or`, `not`, arrow is hardcoded
* Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x
- zify_elim_let is entirely in OCaml (no Ltac callback)
[micromega] fix stack overflow
Less naive computation of bounds (online elimination of duplicates)
|
|
|
|
This is to be consistent with "pose (x:=a)" (and an alternative to
"assert (x:=a)").
This was suggested by
"https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962".
|
|
|
|
The previous code was only doing that when either in debug or toplevel mode.
Unfortunately, when dealing with open modules the constants might not have
been registered yet, leading to printing failure. I do not see a reason
why this code should fail when used with globals without a user facing name
when the only goal is to compute a set of identifiers that might clash. Thus,
the above failsafe behaviour is now systematic.
Fixes #8206: Module signature error sometimes prints ??.
|
|
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
|
|
|
|
Fixes #11608.
This means -vos doesn't skip proofs for definitions that end with Qed
but don't include Proof and rely on a Set Default Proof Using. However,
this fixes the bug where this pattern would instead hang, due to #11564.
|
|
See "https://github.com/coq/coq/pull/10008#discussion_r382899607".
|
|
Compile buffer, and with building from a path containing spaces.
Updated CHANGES.md
Now using Filename.quote instead of enclosing in single quotes.
Fixed rebasing problems.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: herbelin
|
|
We avoid redundant notations for the same concepts and make sure
notations do not break Ltac parsing for users of these libraries.
|
|
This gives IMO slightly nicer errors when the type cannot be inferred,
ie
~~~coq
Type (forall x, x = x).
~~~
says "cannot infer the implicit parameter A of eq" instead of "cannot
infer this placeholder".
|
|
On the principle that a notation to a constant inherits the implicit
arguments of the constant, a non-applied notation should inherit its
next maximal implicit arguments.
|
|
Reviewed-by: tchajed
|
|
Reviewed-by: tchajed
|
|
(inconsistencies in parsing/printing notations to partial applications)
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
|
|
Fix #11552: Ltac2 breaks query commands during proofs.
|
|
|
|
|
|
This is a case which conventionally deactivates implicit arguments.
|
|
Exception: when the notation is to some @id.
Formerly, this was ignored for all kinds of string notations.
|
|
Also apply the same conditions for printing constructors as record
instances in both terms and patterns.
|
|
This is a change of semantics.
|
|
This was done for abbreviations but not string notations. This adopts
the policy proposed in #11091 to make parsing and printing consistent.
|
|
This is to match the parsing policy (see #11091).
In particular, we deactivate also argument scopes, consistently with
what is done at parsing time.
|
|
The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[])
encoding of @f was lost.
It remains to let printing match parsing wrt the deactivation of
implicit arguments and argument scopes in such case. See next commit.
|
|
When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
|
|
We fix also an index error in deciding when to explicit print a
non-inferable implicit argument.
|
|
Reviewed-by: ejgallego
|
|
pattern-matching problem
Reviewed-by: ejgallego
|
