aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-03-25Test suite file for a bug in int31 arithmetic fixed a while ago.Maxime Dénès
2016-03-25Remove int64 emulation in bytecode interpreter.Maxime Dénès
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-03-21Moving the last parts of the Ltac engine to hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tacsubst to hightactics.Pierre-Marie Pédrot
2016-03-20Relying on generic arguments to represent Extern hints.Pierre-Marie Pédrot
2016-03-20Adding a new Ltac generic argument for forced tactics returing unit.Pierre-Marie Pédrot
2016-03-20Moving Tacenv to Hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tactic_debug to Hightactic.Pierre-Marie Pédrot
2016-03-20Moving the lowest parts of pretyping/ (Evarutil & Proofview) to engine/.Pierre-Marie Pédrot
2016-03-20Documenting changes.Pierre-Marie Pédrot
2016-03-20Moving Evarutil and Proofview to engine/Pierre-Marie Pédrot
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-03-20Splitting Evarutil in two distinct files.Pierre-Marie Pédrot
2016-03-20Pushing Proofview further down the dependency alley.Pierre-Marie Pédrot
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-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-20Fixing the classification of Tactic Notation.Pierre-Marie Pédrot
2016-03-20Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Pierre-Marie Pédrot
2016-03-20Moving most of Ltac code to Hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tacintern to Hightactics.Pierre-Marie Pédrot
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving the tactic related code from Metasyntax to a new file.Pierre-Marie Pédrot
2016-03-20Moving Print Ltac to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tacinterp to Hightactics.Pierre-Marie Pédrot
2016-03-19Moving the use of Tactic_option from Obligations to G_obligations.Pierre-Marie Pédrot
2016-03-19Fixing compilation with old versions of CAMLP5.Pierre-Marie Pédrot
2016-03-19Fixing compilation with old versions of CAMLP5.Pierre-Marie Pédrot
2016-03-19Removing dead code in Genarg.Pierre-Marie Pédrot
2016-03-19Removing the untyped representation of genargs.Pierre-Marie Pédrot
2016-03-19Simplifying the EXTEND macros and making them more self-contained.Pierre-Marie Pédrot
2016-03-19EXTEND macros use their own internal representations.Pierre-Marie Pédrot
2016-03-19Do not keep the argument type in ExtNonTerminal.Pierre-Marie Pédrot
2016-03-19Further reducing the dependencies of the EXTEND macros.Pierre-Marie Pédrot
2016-03-19Removing the VernacSolve entry of the vernacular AST.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-19Replacing the interpretation of Proof using ... with a proper code.Pierre-Marie Pédrot
2016-03-19Moving the parsing of the Ltac proof mode to G_ltac.Pierre-Marie Pédrot
2016-03-19Removing the dependency in VernacSolve in the STM.Pierre-Marie Pédrot
2016-03-19Moving the proof mode parsing management to Pcoq.Pierre-Marie Pédrot
2016-03-19Relying on Vernac classifier to flag tactics in the STM.Pierre-Marie Pédrot
2016-03-19Cleaning up and extending the expressivity of Pcoq.Pierre-Marie Pédrot
2016-03-19Allowing generalized rules in typed symbols.Pierre-Marie Pédrot
2016-03-19Do not export entry_key from Pcoq anymore.Pierre-Marie Pédrot
2016-03-19Simplifying the code of Entry.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 20:35:14 +0000