aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-03-28Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
2016-03-28Updating .gitignore.Pierre-Marie Pédrot
2016-03-28Fixing an evar leak in Rewrite introduced by 968dfdb15.Pierre-Marie Pédrot
2016-03-28Was too restrictive in syntactic definitions, not imagining that theyHugo Herbelin
2016-03-25Moving back some tactics not essentially related to Ltac into the tactics/ fo...Pierre-Marie Pédrot
2016-03-25Moving Autorewrite back to tactics/.Pierre-Marie Pédrot
2016-03-25Making Autorewrite independent from Ltac.Pierre-Marie Pédrot
2016-03-25Moving Eqdecide to tactics/.Pierre-Marie Pédrot
2016-03-25Making Eqdecide independent of Extratactics.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
2016-03-25Moving type_uconstr to Pretyping.Pierre-Marie Pédrot
2016-03-25Test suite file for a bug in BigQ arithmetic fixed a while ago.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:14:09 +0000