index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
himsg.ml
Age
Commit message (
Expand
)
Author
2018-10-26
[typeclasses] functionalize typeclass evar handling
Matthieu Sozeau
2018-10-26
Cleanup evar_extra: remove evar_info's store and add maps to evar_map
Matthieu Sozeau
2018-09-28
Functionalizing calls to the environment in Himsg.
Hugo Herbelin
2018-09-27
Merge PR #8475: Centralize the reliance on abstract universe context internals
Gaëtan Gilbert
2018-09-21
Removing calls to AUContext.instance.
Pierre-Marie Pédrot
2018-09-19
Fix Numeral Notations (2/4 - exceptions, usr_err)
Jason Gross
2018-09-03
Merge PR #891: Check universes are declared
Gaëtan Gilbert
2018-07-26
Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...
Pierre-Marie Pédrot
2018-07-25
In "redundant clause" pattern-matching error, show also the pattern (#7777).
Hugo Herbelin
2018-07-25
kernel: missing check that all universes are declared.
Matthieu Sozeau
2018-07-25
Remove himsg.pr_puniverses, use @{} for universe printing in errors
Maxime Dénès
2018-07-17
Change QuestionMark for better record field missing error message.
Siddharth Bhat
2018-06-22
Remove hack skipping comparison of algebraic universes in subtyping.
Gaëtan Gilbert
2018-05-31
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-25
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-23
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-17
Split off Universes functions dealing with names.
Gaëtan Gilbert
2018-04-13
Evar maps contain econstrs.
Gaëtan Gilbert
2018-03-31
[econstr] Forbid calling `to_constr` in open terms.
Emilio Jesus Gallego Arias
2018-03-24
Slightly refining some error messages about unresolvable evars.
Hugo Herbelin
2018-03-09
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values
Maxime Dénès
2018-03-08
Fix SR breakage due to allowing fixpoints on non-rec values
Matthieu Sozeau
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-02
Reductionops.nf_* now take an environment.
Gaëtan Gilbert
2017-11-22
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-21
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-13
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-09-22
Himsg: Dropping nf_evars made obsolete by EConstr.
Hugo Herbelin
2017-09-22
Cannot unify message: improve preventing repeating twice the same message.
Hugo Herbelin
2017-09-15
Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.
Maxime Dénès
2017-09-12
Port is_Set and is_Type to EConstr, as was is_Prop already.
Guillaume Melquiond
2017-08-30
Fixing a capitalization in the middle of the sentence of an error message.
Hugo Herbelin
2017-08-01
Detyping functions are now operating on EConstr.t.
Pierre-Marie Pédrot
2017-07-26
Remove a few useless evar-normalizations in printing code.
Pierre-Marie Pédrot
2017-07-13
The only abstraction-breaking function in Univ is now AUContext.instance.
Pierre-Marie Pédrot
2017-07-11
Properly handling polymorphic inductive subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-16
Clean up universes of constants and inductives
Amin Timany
2017-05-31
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-02-15
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
