index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
comProgramFixpoint.ml
Age
Commit message (
Expand
)
Author
2019-12-04
Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.
Hugo Herbelin
2019-09-16
Fix #10757: Program Fixpoint uses "exists" for telescopes
Gaëtan Gilbert
2019-08-08
Emit Feedback.AddedAxiom in Declare instead of higher layers
Gaëtan Gilbert
2019-07-23
[vernacexpr] Remove duplicate fixpoint record.
Emilio Jesus Gallego Arias
2019-07-23
[vernacexpr] Refactor fixpoint AST.
Emilio Jesus Gallego Arias
2019-07-08
[api] Deprecate GlobRef constructors.
Emilio Jesus Gallego Arias
2019-07-01
[declare] Separate kinds from entries in constant declaration
Emilio Jesus Gallego Arias
2019-07-01
[api] Refactor most of `Decl_kinds`
Emilio Jesus Gallego Arias
2019-06-26
[declare] Fine tuning of Hook type.
Emilio Jesus Gallego Arias
2019-06-24
[lemmas] [proof] Split proof kinds into per-layer components.
Emilio Jesus Gallego Arias
2019-06-24
Duplicate the type of constant entries in Proof_global.
Pierre-Marie Pédrot
2019-06-20
Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...
Pierre-Marie Pédrot
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-17
[proof] Move declaration hooks to DeclareDef.
Emilio Jesus Gallego Arias
2019-06-17
[proof] Unify obligation proof save path: Part I, declareObl
Emilio Jesus Gallego Arias
2019-05-13
Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.
Hugo Herbelin
2019-05-13
Moving Evd.evars_of_term from constr to econstr + consequences.
Hugo Herbelin
2019-04-16
Clean the representation of recursive annotation in Constrexpr
Maxime Dénès
2019-03-30
[program] Allow evars in type of fixpoints.
Emilio Jesus Gallego Arias
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-02-28
Implement a method for manual declaration of implicits.
Jasper Hugunin
2019-02-23
[vernac] Unify declaration hooks.
Emilio Jesus Gallego Arias
2019-02-05
Make Program a regular attribute
Maxime Dénès
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-11-30
[vernac] [hooks] Refactor towards optional hooks.
Emilio Jesus Gallego Arias
2018-11-12
Merge PR #8892: Fix part of #8224: grounding open term in fixpoints
Pierre-Marie Pédrot
2018-11-09
Remove remnants of polymorphic instance name registration.
Pierre-Marie Pédrot
2018-11-06
[program] extend obligation to give back a mapping from obligations to
Matthieu Sozeau
2018-11-02
Fixing one instance of bug #8224 (grounding term w/o knowing if it has evars).
Hugo Herbelin
2018-10-30
Switch to using the obligation_evar flag instead of the evar source
Matthieu Sozeau
2018-10-15
Correct some spelling errors
Benjamin Barenblat
2018-10-11
[vernac] Remove unused abstraction from declaration_hook type.
Emilio Jesus Gallego Arias
2018-10-10
[coqlib] Rebindable Coqlib namespace.
Emilio Jesus Gallego Arias
2018-07-17
change into QuestionMark default
Siddharth Bhat
2018-07-17
Change QuestionMark for better record field missing error message.
Siddharth Bhat
2018-06-18
Remove reference name type.
Maxime Dénès
2018-05-31
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-17
Split off Universes functions dealing with names.
Gaëtan Gilbert
2018-05-14
Deprecate Typing.e_* functions
Gaëtan Gilbert
2018-03-31
[econstr] Forbid calling `to_constr` in open terms.
Emilio Jesus Gallego Arias
2018-03-09
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
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
