index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
comFixpoint.ml
Age
Commit message (
Expand
)
Author
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-05-23
Fixing typos - Part 3
JPR
2019-05-21
Remove definition-not-visible warning
Gaëtan Gilbert
2019-04-16
Clean the representation of recursive annotation in Constrexpr
Maxime Dénès
2019-03-27
[vernac] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-02-05
Make Program a regular attribute
Maxime Dénès
2018-11-30
[vernac] [hooks] Refactor towards optional hooks.
Emilio Jesus Gallego Arias
2018-11-21
Make initial evar map argument to check_evars_are_solved optional.
Gaëtan Gilbert
2018-11-02
Fixing one instance of bug #8224 (grounding term w/o knowing if it has evars).
Hugo Herbelin
2018-10-16
{Univops -> Vars}.universes_of_constr
Gaëtan Gilbert
2018-10-10
[coqlib] Rebindable Coqlib namespace.
Emilio Jesus Gallego Arias
2018-10-07
Adding missing header to comFixpoint.ml.
Hugo Herbelin
2018-06-26
universes_of_constr don't include universes of monomorphic constants
Gaëtan Gilbert
2018-06-12
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-06-04
Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.
Matthieu Sozeau
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-14
Deprecate Typing.e_* functions
Gaëtan Gilbert
2018-04-17
Deprecate mixing univ minimization and evm normalization functions.
Gaëtan Gilbert
2018-03-31
[econstr] Forbid calling `to_constr` in open terms.
Emilio Jesus Gallego Arias
2018-03-29
Fix #6770: fixpoint loses locality info in proof mode.
Gaëtan Gilbert
2018-03-05
Allow universe declarations for [with Definition].
Gaëtan Gilbert
2018-02-28
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-22
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2017-12-17
[vernac] Split `command.ml` into separate files.
Emilio Jesus Gallego Arias
