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