aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* The unshelve tactical now takes future goals into account.Gravatar Pierre-Marie Pédrot2015-12-09
* Adding an unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-09
* Univs: correctly register universe binders for lemmas.Gravatar Matthieu Sozeau2015-11-28
* Performance fix for destruct.Gravatar Pierre-Marie Pédrot2015-11-17
* Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Gravatar Pierre-Marie Pédrot2015-11-12
* Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionGravatar Matthieu Sozeau2015-11-04
* Made that the syntax [id]:tac also applies to the shelve, which is after all ...Gravatar Hugo Herbelin2015-11-02
* Handle side-effects of Vernacular commands inside proofs better, so thatGravatar Matthieu Sozeau2015-10-29
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Fixed (and changed) infoH.Gravatar Pierre Courtieu2015-10-21
* Categorizing debug messages as such + NonLogical uses loggers.Gravatar Pierre Courtieu2015-10-19
* Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Fix LemmaOverloadingGravatar Matthieu Sozeau2015-10-14
* Remove misleading warning (Close #4365)Gravatar Enrico Tassi2015-10-09
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* Fixing emacs output in debugging mode.Gravatar Pierre Courtieu2015-10-06
* Univs: fix handling of evd's universes and side effects in build_by_tacticGravatar Matthieu Sozeau2015-10-02
* Univs: fix handling of side effects/delayed proofsGravatar Matthieu Sozeau2015-10-02
* Changed status of Info messages from notice to info.Gravatar Pierre Courtieu2015-10-02
* Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-09-23
* Proof: suggest Admitted->Qed only if the proof is really complete (#4349)Gravatar Enrico Tassi2015-09-20
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-08-02
* Fixing what seems to be a typo.Gravatar Hugo Herbelin2015-07-29
* Slightly improving line break formatting in Info command.Gravatar Hugo Herbelin2015-07-27
* Fix `Pp` function used by the `Info` command.Gravatar Arnaud Spiwack2015-06-23
* 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
* STM/Univ: save initial univs (the ones in the statement) in Proof.proofGravatar Enrico Tassi2015-05-29
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Gravatar Pierre-Marie Pédrot2015-05-18
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Slightly more efficient implementation of the logic monad.Gravatar Pierre-Marie Pédrot2015-04-19
* typoGravatar Enrico Tassi2015-03-22
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* [Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Gravatar Arnaud Spiwack2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Granting wish #4008.Gravatar Pierre-Marie Pédrot2015-02-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Tentative workaround for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-24
* Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it wasGravatar Maxime Dénès2015-01-18
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 09:03:23 +0000