aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_global.mli
Commit message (Expand)AuthorAge
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
* Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
* [proof] [api] Rename proof types in preparation for functionalization.Gravatar Emilio Jesus Gallego Arias2017-11-29
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * [proof] Move bullets to their own module.Gravatar Emilio Jesus Gallego Arias2017-06-12
|/
* [proof] Deprecate "proof mode" APIGravatar Emilio Jesus Gallego Arias2017-05-31
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Making Proof_global terminator generic in external tactics.Gravatar Pierre-Marie Pédrot2016-09-08
* CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
* Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Gravatar Enrico Tassi2016-05-10
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Use streams rather than strings to handle bullet suggestions.Gravatar Guillaume Melquiond2016-01-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Univs: correctly register universe binders for lemmas.Gravatar Matthieu Sozeau2015-11-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|\|
| * Handle side-effects of Vernacular commands inside proofs better, so thatGravatar Matthieu Sozeau2015-10-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
| * Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* | Opacifying the proof_terminator type.Gravatar Pierre-Marie Pédrot2015-09-08
|/
* Fixing what seems to be a typo.Gravatar Hugo Herbelin2015-07-29
* STM: states coming from workers have no proof terminators (Close #4246)Gravatar Enrico Tassi2015-06-09
* Admitted does not drop poly-univ constraints (Fix #4244)Gravatar Enrico Tassi2015-06-03
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Proof using: call "clear" to remove from sight the vars not selectedGravatar Enrico Tassi2014-12-28
* Vi2vo: fix handling of univ constraints coming from the bodyGravatar Enrico Tassi2014-12-23
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Fix handling of universes at the end of proofs, esp. for async proof processing.Gravatar Matthieu Sozeau2014-07-25
* Proof_global.start_dependent_proof: properly threads the sigma through the te...Gravatar Arnaud Spiwack2014-07-23
* Change the interface of proof_global to take an evar_map instead of a univers...Gravatar Arnaud Spiwack2014-07-23
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 15:14:43 +0000