| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-16 | Less type-unsafety in Pcoq. | Pierre-Marie Pédrot | |
| 2016-01-15 | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. | Maxime Dénès | |
| 2016-01-14 | Removing constr generic argument. | Pierre-Marie Pédrot | |
| 2016-01-14 | Continuing 003fe3d5e on parsing positions. | Hugo Herbelin | |
| - Being stricter on the ordinal suffix accepted (only st for 1, 21, etc, nd for 2, 22, etc., etc.) - Reporting when the suffix is not the expected one (rather than considering that, e.g. 2st, is two tokens, a number then an identifier). | |||
| 2016-01-11 | CLEANUP: removing unused field | Matej Kosik | |
| I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around. | |||
| 2016-01-02 | Remove some useless type declarations. | Guillaume Melquiond | |
| 2016-01-02 | Simplification of grammar_prod_item type. | Pierre-Marie Pédrot | |
| Actually the identifier was never used and just carried along. | |||
| 2016-01-02 | Separation of concern in TacAlias API. | Pierre-Marie Pédrot | |
| The TacAlias node now only contains the arguments fed to the tactic notation. The binding variables are worn by the tactic representation in Tacenv. | |||
| 2015-12-30 | External tactics and notations now accept any tactic argument. | Pierre-Marie Pédrot | |
| This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant. | |||
| 2015-12-28 | Removing unused parsing entries. | Pierre-Marie Pédrot | |
| 2015-12-28 | Removing the special status of open_constr generic argument. | Pierre-Marie Pédrot | |
| We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state. | |||
| 2015-12-25 | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.ml | Hugo Herbelin | |
| to g_tactic.ml4 so as to leave room for "IntroPattern []" to mean "no introduction". | |||
| 2015-12-25 | Fixing non exhaustive pattern-matching in 003fe3d5e60b. | Hugo Herbelin | |
| 2015-12-24 | Removing auto from the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-23 | Partial backtrack on commit 20641795624. | Pierre-Marie Pédrot | |
| The parsing rules were broken and disallowed tactic replacement of the form Ltac ident ::= expr. | |||
| 2015-12-18 | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified | Matej Kosik | |
| 2015-12-18 | CLEANUP: Vernacexpr.VernacDeclareTacticDefinition | Matej Kosik | |
| The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that. | |||
| 2015-12-18 | ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file | Matej Kosik | |
| 2015-12-18 | CLEANUP: Vernacexpr.vernac_expr | Matej Kosik | |
| Originally, "VernacTime" and "VernacRedirect" were defined like this: type vernac_expr = ... | VernacTime of vernac_list | VernacRedirect of string * vernac_list ... where type vernac_list = located_vernac_expr list Currently, that list always contained one and only one element. So I propose changing the definition of these two variants in the following way: | VernacTime of located_vernac_expr | VernacRedirect of string * located_vernac_expr which covers all our current needs and enforces the invariant related to the number of commands that are part of the "VernacTime" and "VernacRedirect" variants. | |||
| 2015-12-15 | Adding a token "index" representing positions (1st, 2nd, etc.). | Hugo Herbelin | |
| 2015-12-15 | Tactics: Generalizing the use of the experimental clearing modifier to | Hugo Herbelin | |
| all cases of rewrite. | |||
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-10 | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin | |
| Marking it as experimental. | |||
| 2015-12-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-05 | Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction) | Hugo Herbelin | |
| based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal. | |||
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-02 | Improving syntax of pat/constr introduction pattern so that | Hugo Herbelin | |
| pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat. Open to other suggestions of syntax though. | |||
| 2015-12-02 | Dead code from August 2014 in apply in. | Hugo Herbelin | |
| 2015-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | |
| 2015-11-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-26 | Fixing the "parsing rules with idents later declared as keywords" problem. | Hugo Herbelin | |
| The fix was actually elementary. The lexer comes with a function to compare parsed tokens against tokens of the parsing rules. It is enough to have this function considering an ident in a parsing rule to be equal to the corresponding string parsed as a keyword. | |||
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-02 | Adding syntax "Show id" to show goal named id (shelved or not). | Hugo Herbelin | |
| 2015-10-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-30 | Manually expand red_tactic so that notations do not break reduction tactics. ↵ | Guillaume Melquiond | |
| (Fix bug #3654) | |||
| 2015-10-29 | Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392) | Guillaume Melquiond | |
| Without this expansion, camlp4 fails to properly factor a user notation starting with either "trivial" or "auto". | |||
| 2015-10-28 | Fixing the return type of the Atoken symbol. | Pierre-Marie Pédrot | |
| 2015-10-27 | Removing unused code in Pcoq. | Pierre-Marie Pédrot | |
| 2015-10-27 | Type-safe Egramml.grammar_prod_item. | Pierre-Marie Pédrot | |
| 2015-10-27 | Finer type for Pcoq.interp_entry_name. | Pierre-Marie Pédrot | |
| 2015-10-27 | Getting rid of most uses of unsafe_grammar_extend. | Pierre-Marie Pédrot | |
| 2015-10-27 | Type-safe Egramml.make_rule. | Pierre-Marie Pédrot | |
| 2015-10-27 | Indexing existentially quantified entries returned by interp_entry_name. | Pierre-Marie Pédrot | |
| 2015-10-27 | Type-safe grammar extensions. | Pierre-Marie Pédrot | |
| 2015-10-26 | Pcoq entries are given a proper module. | Pierre-Marie Pédrot | |
| Entries defined in the Pcoq AST of symbols must be marshallable, because they are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as they contain functional values. This is why the Pcoq module used a pair [string * string] to describe entries. It is obviously type-unsafe, so we define a new abstract type in its own module. There is a little issue though, which is that our entries and CAMLP4/5 entries must be kept synchronized through an association table. The Pcoq module tries to maintain this invariant. | |||
| 2015-10-25 | Getting rid of the Atactic entry. | Pierre-Marie Pédrot | |
| 2015-10-25 | Getting rid of the Agram entry. | Pierre-Marie Pédrot | |
| 2015-10-21 | Pcoq.prod_entry_key now uses a GADT to statically enforce typedness. | Pierre-Marie Pédrot | |
| 2015-10-21 | Turn Pcoq into a regular ML file. | Pierre-Marie Pédrot | |
| 2015-10-21 | Expanding the grammar extensions of Pcoq. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |