aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2016-06-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-12Another fix to #4782 (a typing error not captured when dealing with bindings).Hugo Herbelin
2016-06-11Fixing #4782 (a typing error not captured when dealing with bindings).Hugo Herbelin
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-06-08proofs/proofs.mllib: no more proof_errors !Pierre Letouzey
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-26Pfedit.get_current_context refinement (fix #4523)Matthieu Sozeau
2016-05-17Removing some compatibility layers in Tactics.Pierre-Marie Pédrot
2016-05-16Put the "cofix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-05-16Fix bug #4737: cycle tactic doesn't like zero goals.Pierre-Marie Pédrot
2016-05-10Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Enrico Tassi
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-25Univs: fix get_current_context (bug #4603, part I)Matthieu Sozeau
2016-03-23Revert "refine: do check all unif problems are solved (Close: #4415, #4532)"Enrico Tassi
2016-03-23refine: do check all unif problems are solved (Close: #4415, #4532)Enrico Tassi
2016-03-20Moving Proofview to pretyping/.Pierre-Marie Pédrot
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-20Making Proofview independent of Logic.Pierre-Marie Pédrot
2016-03-20Making Proofview independent from Goal.Pierre-Marie Pédrot
2016-03-20Extruding the code for the Existential command from Proofview.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-19Removing the dependency in VernacSolve in the STM.Pierre-Marie Pédrot
2016-03-14Fix the comment of Refine.refineMatthieu Sozeau
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-06Moving Ltac traces to Tacexpr and Tacinterp.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-17Fixing the Proofview.Goal.goal function.Pierre-Marie Pédrot
2016-02-17CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-02-17CLEANUP: Renaming "Util.compose" function to "%"Matej Kosik
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-20Fixing Not_found on unknown bullet behavior.Hugo Herbelin
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-02Use streams rather than strings to handle bullet suggestions.Guillaume Melquiond
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Remove some useless module opening.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 17:10:06 +0000