aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
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
2015-10-02Changed status of Info messages from notice to info.Pierre Courtieu
2015-09-27Removing meta_with_name from Evd.Pierre-Marie Pédrot
2015-09-27Removing uselessly duplicated function in Evd.Pierre-Marie Pédrot
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
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-17Fix previous merge.Maxime Dénès
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-09-08Opacifying the proof_terminator type.Pierre-Marie Pédrot
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-29Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 01:49:11 +0000