| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Funind doesn't support polymorphism.
|
|
|
|
|
|
Having [map] means we can structure attributes when combining them, eg
get an attribute for [type universe_data = { poly : bool option; template : bool
option }] from 2 [bool option] attributes.
Using the previous representation we would have had to provide the
inverse function [universe_data -> bool option * bool option] as well.
An alternate way to get (++) is
let (++) (x:'a t) (y:'b t) : ('a*'b) t =
x >>= fun xv ->
y >>= fun yv ->
return (xv,yv)
Not sure if that would be cleaner.
|
|
|
|
Commands need to request the attributes they use, with the API
encouraging them to error on unsupported attributes.
|
|
|
|
|
|
It was never set, because it makes no sense.
|
|
|
|
|
|
|
|
Ltac_plugin.Taccoerce.CannotCoerceTo.
|
|
Clenv.make_evar_clause.
|
|
custom entries.
|
|
|
|
an environment
|
|
|
|
Coercions were missing.
|
|
|
|
|
|
|
|
Adressed comments by Guillaume and Jason
Updated according to Zimmi48's input.
Better link to custom entries
Fix typesetting
|
|
|
|
This is a step towards limiting calls to the global environment.
Incidentally unify naming evd -> sigma in Termops.
|
|
|
|
|
|
This is because the env contains typing flags (such as sharing
strategy).
|
|
|
|
We also stop passing dummy env and evar maps.
|
|
We can then avoid passing an empty env.
|
|
|
|
|
|
|
|
members when it changes.
|
|
|
|
|
|
|
|
|
|
|
|
Fixes most of #8822.
|
|
|
