| Age | Commit message (Collapse) | Author |
|---|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
Cf CHANGES for details.
|
|
|
|
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
|
This reverts commit 9e038688af8f7f054c1c2acdb2fe65d78cccdd81.
|
|
This reverts commit cbb917476e3920641352c108ec9ffaf6d1682217.
|
|
|
|
|
|
Notation "## c" := (S c) (at level 0, c at level 100).
which break the stratification of precedences. This works for the case
of infix or suffix operators which occur in only one grammar rule,
such as +, *, etc. This solves the "constr" part of #3709, even though
this example is artificial.
The fix is not complete. It puts extra parenthesese even when it is
end of sentence, as in
Notation "# c % d" := (c+d) (at level 3).
Check fun x => # ## x % ## (x * 2).
(* fun x : nat => # ## x % (## x * 2) *)
The fix could be improved by not always using 100 for the printing
level of "## c", but 100 only when not the end of the sentence.
The fix does not solve the general problem with symbols occurring in
more than one rule, as e.g. in:
Notation "# c % d" := (c+d) (at level 1).
Notation "## c" := (S c) (at level 0, c at level 5).
Check fun x => # ## x % 0.
(* Parentheses are necessary only if "0 % 0" is also parsable *)
I don't see in this case what better approach to follow than
restarting the parser to check reversibility of the printing.
|
|
|
|
|
|
|
|
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.
|
|
For instance, calling only Id.print is faster than calling both str and
Id.to_string, since the latter performs a copy. It also makes the code a
bit simpler to read.
|
|
|
|
For instance, #4447 is now printed:
λ Ca Da : ℕAlg,
let (ℕ, ℕ0) := (Ca, Da) in
let (C, p) := ℕ in
let (c₀, cs) := p in
let (D, p0) := ℕ0 in
let (d₀, ds) := p0 in
{h : C → D & ((h c₀ = d₀) * (∀ c : C, h (cs c) = ds (h c)))%type}
: ℕAlg → ℕAlg → Type
|
|
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
|
Fixes bug 3936
This closes #73
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
They should be rather sensible, but de gustibus & coloribus...
|
|
reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.
In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
head symbol is written "+" (in the toplevel scope); idem for
vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
native_compute with functor application should now work (i.e.
vm_compute and native_compute are now taken into account in
tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.
By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").
|
|
|
|
|
|
|
|
printing/RichPrinter: Rename into Richprinter.
printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp.
printing/Richprinter: Cosmetics.
|
|
|
|
A combinator to introduce tags.
printing/{Ppconstr, Ppvernac}: Use it.
|
|
printing/{Ppconstr, Ppvernac}: Use it.
|
|
Define the annotations stored in semi-structured pretty-prints.
Ppconstrsig: New.
Contains the signature of a pretty-printer for ppconstr.
Ppconstr: Export a new rich pretty-printer for constr_expr and co.
|
|
- Functorize Ppconstr with respect to a set of tagging functions.
- These functions are meant to introduce tags to produce semistructured
pretty printings.
printing/Ppconstr:
Preserve the previous behaviour of this module by instantiating Make
with tagging functions that do nothing.
|
|
Make evaluation order explicit.
(Do not rely anymore on ocaml evaluation order, which is unspecified.)
|
|
|
|
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.
|
|
|
|
in instances.
|
|
|
|
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
|
|
|
change of printing format of forall (need more thinking).
|
|
|
|
|
|
Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
|
|
foo@{(ident|Prop|Set|Type|' ')*}
(user given names are still write only).
- Add test-suite file for named universes.
|
