| Age | Commit message (Collapse) | Author |
|---|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
Ack-by: JasonGross
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: tchajed
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
|
|
Remove the 2nd premise "(E[Γ_P ] ⊢ A_j : s_j)_(j=1...k)".
Also, "Γ" in "c_i ∉ Γ ∪ E" is changed to "Γ_I".
"E[Γ_P ] ⊢ A_j : s_j" contradicts with a side condition
"A_j is an arity of sort s_j".
The latter means that A_j is ∀ x1:T1, ... ∀ xm:Tm, s_j.
So, "(∀ x1:T1, ..., s_j) : s_j)" is required.
Using Prod-{Prop,Set,Type}, it needs "s_j : s_j" which cannot be proved.
This problem is introduced at 2018-07-22:
https://github.com/coq/coq/commit/f25c1d252ad61b4dc4321e3a11f33b1e6d4e3dff
Before that, the premise describes "A_j : s'_j".
And "s'_j" is not explained anywhere.
I think "A_j : s'_j" describes that A_j is a type (a value of a sort).
Thus, "A_j is an arity of sort s_j" imply "A_j : s'_j".
So, I removed the 2nd premise.
Also, a side condition describes "c_i ∉ Γ ∪ E" but "Γ" is not explained.
I think that Γ should be Γ_I.
Γ should include Γ_I because a constructor, c_i, and inductive types are
both defined in global environment and it cannot accept duplicate name.
Actually, such definition fails:
```
Fail Inductive X := X : X.
(* The following names are used both as type names and constructor names: X.*)
```
Γ doesn't include Γ_P because parameters are not defined in global
environment.
Actually, a parameter can be same name as a constructor name:
```
Inductive I (X : nat) := X : I X.
Check X. (* X : forall X : nat, I X *)
```
|
|
Cic description doesn't describe the lowest universe level clearly.
- "Type(i) for any integer i" seems Type(-1) is possible
- "S = {Prop,Set,Type(i)| i ∈ ℕ }" depends on the definition of "ℕ"
which is not described.
It is well known that there are two definitions that ℕ includes 0 or not.
In Coq, it is natural that ℕ includes 0 because the inductive type
nat includes 0.
- "Prop:Type(1), Set:Type(1)" suggests the lowest level is 1.
- AX-Prop and AX-Set describes Prop:Type(1) and Set:Type(1).
So, Prop and Set are not belongs to Type(0).
Also, CPDT describes that "The type of Set is Type(0)".
http://adam.chlipala.net/cpdt/html/Universes.html
I think the lowest universe level is 1 because AX-Prop and AX-Set.
I'm not certain to fix this problem but
my idea to fix this problem is changing
"Type(i) for any integer i" to
"Type(i) for any integer i ≥ 1".
|
|
Fixes #9453
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
The former is more succinct and intuitive.
|
|
c can be non-function since c:U.
So, c c' is not typeable.
|
|
|
|
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
This commit basically ajusts spaces as
- ∀x:T,t to ∀x:T,~t
- λx:T.t to λx:T.~t
- E;c:T to E;~c:T
x and T are more related than T and t.
So, T and t should not positioned closely than x and T.
Unfortunately, they are formatted that T and t are positioned closely
without "~".
(Similary, c and T are more related than E and c.)
|
|
The former is more succinct and consistent with most of
other parts in cic.rst.
|
|
Add :math:`...` for mathematical expressions.
|
|
|
|
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort" is changed to
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S" because
\Sort is not a term.
"S" is choosen to be consistent with the description of
Inductive Definitions.
|
|
|
|
|
|
|
|
Exchange a closing parenthesis and a :math: closing backquote.
|
|
In the note about η-reduction,
two lambda-abstraction used "," instead of ".".
|
|
After #9435 (Use \mathcal instead of \cal), \Sort doesn't have
font changing effect.
So, {\Sort} is same as \Sort now and the former is changed to latter in
cic.rst.
|
|
|
|
|
|
|
|
This corresponds to "Module TreeExample." removed at
2018-04-24 bcf5352cc7a26a672e719f7dad4021c69d723833.
|
|
Reviewed-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: vbgl
|
|
|
|
Use default OCaml version (4.06.1).
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
This PR deprecates the use of `coqtop` as a compiler.
There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.
We adapt the documentation and adapt the test-suite.
Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.
The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
|
|
|
|
Fix #8076.
|
|
|
|
Make lazy_match! goal actually lazy
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
It now removes the outdated `CompatOldOldFlag.v` file on `--release`,
and it now correctly updates `bug_9166.v` which seems to specifically be
about the compat flag behavior.
Additionally, it inserts an "autogenerated" notice at top of the two bug
files, and makes them read-only.
|
|
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
This makes the display consistent wrt `TEST`:
```
TEST failure/Case7.v
CHECK Case7
```
vs
```
TEST failure/Case7.v
CHECK failure/Case7.v
```
|
|
Apparently it's deprecated / doesn't always work, see
https://tex.stackexchange.com/questions/84041/why-does-calm-n-give-m
See #9429 (we also need to fix the distributed file on the server).
|
