aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
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
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-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-23Fix `Pp` function used by the `Info` command.Arnaud Spiwack
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
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-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 08:11:12 +0000