| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| | |
This API is a bit strange, I expect it will change at some point.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.
Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.
This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
|
| |
|
|
| |
Normalization sounds like it should be semantically noop.
|
| |
|
|
|
| |
The "Stream.Error" printer does add a period, so, the messages
themselves should not.
|
| |
|
|
|
|
|
| |
Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were
declared twice for all records.
Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an
observable error for monomorphic records.
|
| |\
| |
| |
| | |
a record.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.
The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.
We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.
In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.
Also, the new return type of `Pretyping.understand` should undergo
careful review.
We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.
Some TODOs are:
- impargs was calling whd_all, the Econstr equivalent can be either
+ Reductionops.whd_all [which does refolding and no sharing]
+ Reductionops.clos_whd_flags with all as a flag.
|
| |/ / |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
| | |
| |
| |
| | |
This was for autoinstance.
|
| |/
|
|
| |
Was raised by Jason on Gitter.
|
| |
|
|
|
| |
This ensures by construction that we never infer constraints outside
the variance model.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
| |
|
|
|
| |
This datatype enforces stronger invariants, e.g. that we only have in the
substitution codomain a connex interval of variables from 0 to n - 1.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
Typeclasses.typeclass
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.
We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.
This patch depends on #6413.
|
| | |
| |
| |
| |
| | |
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.
E.g mono@{i} := Type@{i} is printed as
mono@{mono.i} := Type@{mono.i}.
There can be a name clash if there's a module and a constant of the
same name. It is detected and is an error if the constant is first
but is not detected and the name for the constant not
registered (??) if the constant comes second.
Accept VarRef when registering universe binders
Fix two problems found by Gaëtan where binders were not registered properly
Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs
Fix an issue of the stronger restrict universe context + no evd leak
This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
|
| |/ |
|
| |
|
|
|
|
| |
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
| |
|
|
|
|
|
|
| |
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
| |
|
|
|
| |
I think this only affects printing (in the new test you would get
[Var (0)] when printing runwrap) but is still ugly.
|
| | |
|
| | |
|
| |
|
|
| |
Before sometimes there were lists and strings.
|
| |
|
|
|
|
|
| |
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
| | |
|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| | |
|
| |\
| |
| |
| | |
clause of an inductive definitions
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This allows e.g. the following to work:
Reserved Notation "* a" (at level 70).
Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m).
We seize this opportunity to make main calls to Metasyntax to depend
on an arbitrary env rather than on Global.env.
Incidentally, this fixes a little coqdoc bug in classifying the
inductive type referred to in the "where" clause.
|
| |/
|
|
|
| |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| |
|
|
|
| |
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
|
| |
|
|
|
| |
This essentially means storing the abstract universe context in the typeclass
data, and abstracting it when necessary.
|
| | |
|
| |
|
|
|
|
| |
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Fix a mistake in record declaration
|
| | |
|
| | |
|
| |
|
|
| |
Also reinferred after sections discharge
|
| |
|
|
|
|
|
|
|
| |
It stores both universe constraints and subtyping information for
blocks of inductive declarations.
At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
|
Pierre-Marie Pédrot
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Hugo Herbelin
Maxime Dénès
Théo Zimmermann
Matthieu Sozeau
Amin Timany