aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Tacenv to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Tactic_debug to Hightactic.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving the lowest parts of pretyping/ (Evarutil & Proofview) to engine/.Gravatar Pierre-Marie Pédrot2016-03-20
|\
| * Documenting changes.Gravatar Pierre-Marie Pédrot2016-03-20
| * Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
| * Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
| * Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
| * Pushing Proofview further down the dependency alley.Gravatar Pierre-Marie Pédrot2016-03-20
| * Moving Proofview to pretyping/.Gravatar Pierre-Marie Pédrot2016-03-20
| * Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
| * Making Proofview independent of Logic.Gravatar Pierre-Marie Pédrot2016-03-20
| * Making Proofview independent from Goal.Gravatar Pierre-Marie Pédrot2016-03-20
|/
* Extruding the code for the Existential command from Proofview.Gravatar Pierre-Marie Pédrot2016-03-20
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-20
|\
* | Fixing the classification of Tactic Notation.Gravatar Pierre-Marie Pédrot2016-03-20
| * Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving most of Ltac code to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
|\ \
| * | Moving Tacintern to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
| * | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| * | Moving the tactic related code from Metasyntax to a new file.Gravatar Pierre-Marie Pédrot2016-03-20
| * | Moving Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| * | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| * | Moving Tacinterp to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
| * | Moving the use of Tactic_option from Obligations to G_obligations.Gravatar Pierre-Marie Pédrot2016-03-19
|/ /
* | Fixing compilation with old versions of CAMLP5.Gravatar Pierre-Marie Pédrot2016-03-19
* | Fixing compilation with old versions of CAMLP5.Gravatar Pierre-Marie Pédrot2016-03-19
* | Removing dead code in Genarg.Gravatar Pierre-Marie Pédrot2016-03-19
* | Removing the untyped representation of genargs.Gravatar Pierre-Marie Pédrot2016-03-19
* | Simplifying the EXTEND macros and making them more self-contained.Gravatar Pierre-Marie Pédrot2016-03-19
|\ \
| * | EXTEND macros use their own internal representations.Gravatar Pierre-Marie Pédrot2016-03-19
| * | Do not keep the argument type in ExtNonTerminal.Gravatar Pierre-Marie Pédrot2016-03-19
| * | Further reducing the dependencies of the EXTEND macros.Gravatar Pierre-Marie Pédrot2016-03-19
|/ /
* | Removing the VernacSolve entry of the vernacular AST.Gravatar Pierre-Marie Pédrot2016-03-19
|\ \
| * | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
| * | Replacing the interpretation of Proof using ... with a proper code.Gravatar Pierre-Marie Pédrot2016-03-19
| * | Moving the parsing of the Ltac proof mode to G_ltac.Gravatar Pierre-Marie Pédrot2016-03-19
| * | Removing the dependency in VernacSolve in the STM.Gravatar Pierre-Marie Pédrot2016-03-19
| * | Moving the proof mode parsing management to Pcoq.Gravatar Pierre-Marie Pédrot2016-03-19
| * | Relying on Vernac classifier to flag tactics in the STM.Gravatar Pierre-Marie Pédrot2016-03-19
|/ /
* | Cleaning up and extending the expressivity of Pcoq.Gravatar Pierre-Marie Pédrot2016-03-19
|\ \
| * | Allowing generalized rules in typed symbols.Gravatar Pierre-Marie Pédrot2016-03-19
| * | Do not export entry_key from Pcoq anymore.Gravatar Pierre-Marie Pédrot2016-03-19
| * | Simplifying the code of Entry.Gravatar Pierre-Marie Pédrot2016-03-19
|/ /
* | Removing dead code in Pcoq.Gravatar Pierre-Marie Pédrot2016-03-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\ \
* \ \ Rationalizing the use of the various EXTEND macros.Gravatar Pierre-Marie Pédrot2016-03-18
|\ \ \
| * | | Documenting the change of EXTEND macros.Gravatar Pierre-Marie Pédrot2016-03-18
| * | | Making the EXTEND macros almost self-contained.Gravatar Pierre-Marie Pédrot2016-03-18
| * | | ARGUMENT EXTEND made of only one entry share the same grammar.Gravatar Pierre-Marie Pédrot2016-03-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 21:49:53 +0000