| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-21 | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-21 | Moving the last parts of the Ltac engine to hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacsubst to hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Relying on generic arguments to represent Extern hints. | Pierre-Marie Pédrot | |
| 2016-03-20 | Adding a new Ltac generic argument for forced tactics returing unit. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacenv to Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tactic_debug to Hightactic. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving the lowest parts of pretyping/ (Evarutil & Proofview) to engine/. | Pierre-Marie Pédrot | |
| Some functions exported by Evarutil essentially used by the unification engine were moved to a new file Evardefine. Their presence in Evarutil was not making much sense. Moreover, the Refine module of the Proofview file was turned into a proper file in pretyping/. This is because this part of the code was relying on the typing primitives from Pretyping. | |||
| 2016-03-20 | Documenting changes. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Evarutil and Proofview to engine/ | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Evarutil independent from Reductionops. | Pierre-Marie Pédrot | |
| 2016-03-20 | Splitting Evarutil in two distinct files. | Pierre-Marie Pédrot | |
| Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file. | |||
| 2016-03-20 | Pushing Proofview further down the dependency alley. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Proofview to pretyping/. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Refine to its proper module. | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Proofview independent of Logic. | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Proofview independent from Goal. | Pierre-Marie Pédrot | |
| 2016-03-20 | Extruding the code for the Existential command from Proofview. | Pierre-Marie Pédrot | |
| 2016-03-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-20 | Fixing the classification of Tactic Notation. | Pierre-Marie Pédrot | |
| 2016-03-20 | Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4. | Pierre-Marie Pédrot | |
| The interpretation of arguments of tactic notations were normalizing the goal beforehand, which incurred an important time penalty. We now do this argumentwise which allows to save time in frequent cases, notably tactic arguments. | |||
| 2016-03-20 | Moving most of Ltac code to Hightactics. | Pierre-Marie Pédrot | |
| This is a major step towards the pluginification of Ltac. The one important file that is out of reach for now is Tacsubst, as it is used in an intricate way to handle amongst other things auto hints. | |||
| 2016-03-20 | Moving Tacintern to Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving the Ltac definition command to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving the tactic related code from Metasyntax to a new file. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Print Ltac to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tactic Notation to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacinterp to Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving the use of Tactic_option from Obligations to G_obligations. | Pierre-Marie Pédrot | |
| 2016-03-19 | Fixing compilation with old versions of CAMLP5. | Pierre-Marie Pédrot | |
| 2016-03-19 | Fixing compilation with old versions of CAMLP5. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing dead code in Genarg. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing the untyped representation of genargs. | Pierre-Marie Pédrot | |
| 2016-03-19 | Simplifying the EXTEND macros and making them more self-contained. | Pierre-Marie Pédrot | |
| 2016-03-19 | EXTEND macros use their own internal representations. | Pierre-Marie Pédrot | |
| 2016-03-19 | Do not keep the argument type in ExtNonTerminal. | Pierre-Marie Pédrot | |
| 2016-03-19 | Further reducing the dependencies of the EXTEND macros. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing the VernacSolve entry of the vernacular AST. | Pierre-Marie Pédrot | |
| This is an important step into making Ltac a plugin. It also allows to see what the important entry points in the Coq codebase for a tactic language are. | |||
| 2016-03-19 | Moving VernacSolve to an EXTEND-based definition. | Pierre-Marie Pédrot | |
| 2016-03-19 | Replacing the interpretation of Proof using ... with a proper code. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving the parsing of the Ltac proof mode to G_ltac. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing the dependency in VernacSolve in the STM. | Pierre-Marie Pédrot | |
| Instead of mangling the AST in order to interpret par: we remember the goal position to focus on it first and evaluate then the underlying vernacular expression. | |||
| 2016-03-19 | Moving the proof mode parsing management to Pcoq. | Pierre-Marie Pédrot | |
| 2016-03-19 | Relying on Vernac classifier to flag tactics in the STM. | Pierre-Marie Pédrot | |
| 2016-03-19 | Cleaning up and extending the expressivity of Pcoq. | Pierre-Marie Pédrot | |
| 2016-03-19 | Allowing generalized rules in typed symbols. | Pierre-Marie Pédrot | |
| 2016-03-19 | Do not export entry_key from Pcoq anymore. | Pierre-Marie Pédrot | |
| 2016-03-19 | Simplifying the code of Entry. | Pierre-Marie Pédrot | |
| 2016-03-18 | Removing dead code in Pcoq. | Pierre-Marie Pédrot | |
| 2016-03-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |