index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
rewrite.ml
Commit message (
Expand
)
Author
Age
*
Rename some universe minimizing "normalize" functions to "minimize"
Gaëtan Gilbert
2018-03-06
*
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
*
\
Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.
Maxime Dénès
2018-03-04
|
\
\
*
\
\
Merge PR #6676: [proofview] goals come with a state
Maxime Dénès
2018-03-04
|
\
\
\
|
|
*
|
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-28
|
|
/
/
|
/
|
|
|
|
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
|
/
|
/
|
*
|
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
|
*
proofview: goals come with a state
Enrico Tassi
2018-02-20
|
/
*
Reductionops.nf_* now take an environment.
Gaëtan Gilbert
2018-02-02
*
Remove the local polymorphic flag hack.
Maxime Dénès
2017-12-27
*
Merge PR #6419: [vernac] Split `command.ml` into separate files.
Maxime Dénès
2017-12-18
|
\
|
*
[flags] Make program_mode a parameter for commands in vernac.
Emilio Jesus Gallego Arias
2017-12-17
*
|
Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.
Maxime Dénès
2017-12-14
|
\
\
*
|
|
[proof] Embed evar_map in RefinerError exception.
Emilio Jesus Gallego Arias
2017-12-11
|
|
/
|
/
|
|
*
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-12-09
|
/
*
Use Entries.constant_universes_entry more.
Gaëtan Gilbert
2017-11-24
*
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-24
*
Stop exposing UState.universe_context and its Evd wrapper.
Gaëtan Gilbert
2017-11-24
*
Separate checking univ_decls and obtaining universe binder names.
Gaëtan Gilbert
2017-11-24
*
[plugin] Remove LocalityFixme über hack.
Emilio Jesus Gallego Arias
2017-11-22
*
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.
Emilio Jesus Gallego Arias
2017-10-05
*
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
*
Don't lose names in UState.universe_context.
Gaëtan Gilbert
2017-09-19
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-17
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Dualize the unsafe flag of refine into typecheck and make it mandatory.
Pierre-Marie Pédrot
2017-06-13
*
Remove (useless) aliases from the API.
Matej Košík
2017-06-10
*
Put all plugins behind an "API".
Matej Kosik
2017-06-07
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Ltac cleanup: no more constr_of_global calls
Matthieu Sozeau
2017-05-29
*
Merge PR#512: [cleanup] Unify all calls to the error function.
Maxime Dénès
2017-05-29
|
\
|
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
|
[coqlib] Move `Coqlib` to `library/`.
Emilio Jesus Gallego Arias
2017-05-27
|
/
*
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
|
*
Post-rebase warnings (unused opens and 2 unused values)
Gaetan Gilbert
2017-04-27
|
*
Fix 4.04 warnings
Gaetan Gilbert
2017-04-27
*
|
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Use located in tactics.
Emilio Jesus Gallego Arias
2017-04-24
*
|
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-24
|
*
Removing various tactic compatibility layers in core tactics.
Pierre-Marie Pédrot
2017-04-24
|
/
*
Actually exporting delayed universes in the EConstr implementation.
Pierre-Marie Pédrot
2017-04-01
*
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
*
Ltac as a plugin.
Pierre-Marie Pédrot
2017-02-17