aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-11Univs: Fix bug #4363, nested abstract.Matthieu Sozeau
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
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-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-28Univs: correctly register universe binders for lemmas.Matthieu Sozeau
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-18Inlining the only use of Clenv.connect_clenv.Pierre-Marie Pédrot
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-12Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Pierre-Marie Pédrot
2015-11-07Implementing assert and cut with LetIn rather than using a beta-redex.Hugo Herbelin
2015-11-05Merge branch 'v8.5'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-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau
2015-10-29Removing the evar_map argument from s_enter.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-21Fixed (and changed) infoH.Pierre Courtieu
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-20Renaming Goal.enter field into s_enter.Pierre-Marie Pédrot
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19Categorizing debug messages as such + NonLogical uses loggers.Pierre Courtieu
2015-10-19Adding a monotonic variant of Goal.enter and Goal.nf_enter.Pierre-Marie Pédrot
2015-10-18Making Evarutil.new_evar monotonous.Pierre-Marie Pédrot
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-10-18Miscellaneous typos, spacing, US spelling in comments or variable names.Hugo Herbelin
2015-10-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
2015-10-16Merge branch 'v8.5' into trunkMaxime Dénès
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Fix LemmaOverloadingMatthieu Sozeau
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
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-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-06Fixing emacs output in debugging mode.Pierre Courtieu
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 17:18:44 +0000