aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
| | | | | Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file.
* 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
| | | | | | | | | | | | 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.
* | Moving most of Ltac code to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
|\ \ | | | | | | | | | | | | | | | 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.
| * | 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
|\ \ | | | | | | | | | | | | | | | 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.
| * | 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
| | | | | | | | | | | | | | | | | | 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.
| * | 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
|\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Those macros used to handle in a special way the grammar entries and generic arguments known statically from Coq, i.e. defined before Pcoq. This was hardly predictible and very implementation-dependent. We made the EXTEND macros much more light-weight by treating in a uniform way all entries and arguments. Now, they are all produced by outputing the name as-is for entries and as "wit_$name" for genargs, thus letting the scope of the ML code decide which entrie is going to be taken. This is documented in the dev/ changelog. This also allows to get rid of a lot of dependencies in the grammar preprocessor, reducing it to a small functional shell. It is still depending on Compat, but it is most probably possible to reduce the code size even more.
| * | | 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
| | | | | | | | | | | | | | | | This fixes parsing conflicts with the [fix ... with] tactic.
| * | | Removing the special status of generic arguments defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro.
| * | | Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there.
| | | * Fix bug #4627: records with no declared arity can be template polymorphic.Gravatar Matthieu Sozeau2016-03-17
| | | | | | | | | | | | | | | | | | | | As if we were adding : Type. Consistent with inductives with no declared arity.
| | | * Test file for #4623.Gravatar Maxime Dénès2016-03-17
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 16:19:33 +0000