aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-03-28
* Updating .gitignore.Gravatar Pierre-Marie Pédrot2016-03-28
* Fixing an evar leak in Rewrite introduced by 968dfdb15.Gravatar Pierre-Marie Pédrot2016-03-28
* Was too restrictive in syntactic definitions, not imagining that theyGravatar Hugo Herbelin2016-03-28
* Moving back some tactics not essentially related to Ltac into the tactics/ fo...Gravatar Pierre-Marie Pédrot2016-03-25
|\
| * Moving Autorewrite back to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
| * Making Autorewrite independent from Ltac.Gravatar Pierre-Marie Pédrot2016-03-25
| * Moving Eqdecide to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
| * Making Eqdecide independent of Extratactics.Gravatar Pierre-Marie Pédrot2016-03-25
| * Moving Eauto and Class_tactics to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
| * Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
|/
* Test suite file for a bug in BigQ arithmetic fixed a while ago.Gravatar Maxime Dénès2016-03-25
* Test suite file for a bug in int31 arithmetic fixed a while ago.Gravatar Maxime Dénès2016-03-25
* Remove int64 emulation in bytecode interpreter.Gravatar Maxime Dénès2016-03-25
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
* Moving the last parts of the Ltac engine to hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
|\
| * Moving Tacsubst to hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
| * Relying on generic arguments to represent Extern hints.Gravatar Pierre-Marie Pédrot2016-03-20
| * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 12:24:19 +0000