aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
* Revert "refine: do check all unif problems are solved (Close: #4415, #4532)"Gravatar Enrico Tassi2016-03-23
* refine: do check all unif problems are solved (Close: #4415, #4532)Gravatar Enrico Tassi2016-03-23
* Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* Fixing the Proofview.Goal.goal function.Gravatar Pierre-Marie Pédrot2016-02-17
* Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fixing Not_found on unknown bullet behavior.Gravatar Hugo Herbelin2016-01-20
* Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
* Univs: Fix bug #4363, nested abstract.Gravatar Matthieu Sozeau2015-12-11
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 11:40:59 +0000