| Age | Commit message (Collapse) | Author |
|---|
|
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
|
Substitution on bound modules was incorrectly extended without sequential
composition.
|
|
|
|
This was because the traversal algorithm used canonical names instead of user
names, confusing which term was defined and which term was an axiom.
|
|
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
|
This allows to reduce the dependencies of subproofs generated by any sequence
of tactics. Grants wish #4327.
|
|
Let-bindings were not taken into account, resulting in proof-terms way too
huge.
|
|
|
|
|
|
This commit is chiefly about moving code around to ease readability.
|
|
This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)). It is
useful to have function_scope for, e.g., function composition. This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.
Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax. (The scope type_scope
should not be special-cased; this change is coming up next.)
Also explicitly define [function_scope] in theories/Init/Notations.v.
This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]
We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.
|
|
|
|
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
|
in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.
As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
|
|
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
|
command line. Documenting only the former for simplicity and
uniformity with predating option -with-geoproof.
|
|
|
|
File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.
There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
|
|
When set, search results only display symbol names, instead of
displaying full terms with types. This is useful when the list of
symbols is needed by an external program, in particular for doing
completion in IDEs.
|
|
This should actually probably be an anomaly, but I'm unsure the code
for decidability schemes is robust enough to dare it.
|
|
decidability scheme).
Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:
Set Decidable Equality Schemes.
Inductive a := A with b := B.
which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
|
|
This patch implements the traversal of inductive definitions in the
traverse function of toplevel/assumptions.ml which recursively
collects references in terms. In my opinion, this fixes a bug (but it
could be argued that inductive definitions were not traversed on
purpose). I think that is not possible to use this bug to hide a
meaningful use of an axiom.
You can try the patch with the following coq script:
Axiom n1 : nat.
Axiom n2 : nat.
Axiom n3 : nat.
Inductive I1 (p := n1) : Type := c1.
Inductive I2 : let p := n2 in Type := c2.
Inductive I3 : Type := c3 : let p := n3 in I3.
Inductive J : I1 -> I2 -> I3 -> Type :=
| cj : J c1 c2 c3.
Inductive K : I1 -> I2 -> I3 -> Type := .
Definition T := I1 -> I2 -> I3.
Definition C := c1.
Print Assumptions I1.
Print Assumptions I2.
Print Assumptions I3.
Print Assumptions J.
Print Assumptions K.
Print Assumptions T.
Print Assumptions C.
Print Assumptions c1.
Print Assumptions c2.
Print Assumptions c3.
Print Assumptions cj.
The patch is a bit more complicated that I would have liked due to
the feature introduced in commit 2defd4c. Since this commit,
Print Assumptions also displays the type proved when one destruct
an axiom inhabiting an empty type. This provides more information
about where the old implementation of the admit tactic is used.
I am not a big fan of this feature, especially since the change in
the admit tactic.
PS: In order to write some tests, I had to change the criteria for
picking which axiom destruction are printed. The original
criteria was :
| Case (_,oty,c,[||]) ->
(* non dependent match on an inductive with no constructor *)
begin match Constr.(kind oty, kind c) with
| Lambda(Anonymous,_,oty), Const (kn, _)
when Vars.noccurn 1 oty &&
not (Declareops.constant_has_body (lookup_constant kn)) ->
and I replaced Anonymous by _. Indeed, an Anonymous name here could
only be built using the "case" tactic and the pretyper seems to always
provide a name when compiling "match axiom as _ with end". And I
wanted to test what happened when this destruction occurs in
inductive definitions (which is of course weird in practice), for
instance:
Inductive I4 (X : Type) (p := match absurd return X with end)
: Type -> Type :=
c4 : forall (q := match absurd return X with end)
(Y : Type) (r := match absurd return Y with end), I4 X Y.
The ability of "triggering" the display of this information only when
using the "case" tactic (and not destruct or pattern matching written
by hand) could have been a feature. If so, please feel free to
change back the criteria to "Anonymous".
|
|
|
|
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
|
|
verbose flag.
|
|
|
|
|
|
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
|
|
|
|
|
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
|
|
|
|
|
|
This allows fatal_error to be used for printing anomalies at loading time.
|
|
the interfaces.
|
|
Makes sure not to generate inductive schemes of assumed positive types.
|
|
The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.
|
|
|
|
|
|
This interface is promoted by the operf-macro tool
https://github.com/OCamlPro/operf-macro
which allows to run benchmarks of time and memory usage
of various OCaml programs.
Coq already has two ways to get Gc infos:
- the -m|--memory command-line flag prints the total heap words allocated
- the "Print Debug Gc" command prints much more information,
but in a Coq-implementation-defined format that is not suitable
for across-programs comparison
(also an environment variable allows to profile Coq runs on any .v,
in an non-intrusive way)
Note to the Github Robot:
This closes #75
|
|
The first part only contains the summary of the library, while the second
one contains the effective content of it.
|
|
A worker should never have to access the still-to-be-proved
obligations. If that happens, raise an informative anomaly.
|
|
This type contains a few unmarshallable fields, which can cause STM
workers to break in unpleasant ways when running queries
|
|
This allows fatal_error to be used for printing anomalies at loading time.
|
|
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
|
|
|
|
|
Message to the github robot:
This closes #63
|
|
|
|
Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show
Intros] at the end of a proof:
Goal True. trivial. Show Intros.
|
