| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-19 | Merge branch 'master' into ltac2-hooks | Pierre-Marie Pédrot | |
| 2017-05-16 | Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND. | Hugo Herbelin | |
| 2017-05-16 | Adding support for using grammar entries returning no value in EXTEND. | Hugo Herbelin | |
| 2017-05-11 | Merge PR#201: Transparent abstract | Maxime Dénès | |
| 2017-05-04 | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵ | Hugo Herbelin | |
| batch mode. | |||
| 2017-05-03 | Generalizing the tactic-in-term embedding to any generic argument. | Pierre-Marie Pédrot | |
| 2017-05-03 | Allowing to pass arbitrary data in internalization environments. | Pierre-Marie Pédrot | |
| 2017-04-27 | Post-rebase warnings (unused opens and 2 unused values) | Gaetan Gilbert | |
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Add [_] prefix to unused values which maybe should be kept | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-27 | Fix omitted labels in function calls | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [rec] keywords | Gaetan Gilbert | |
| 2017-04-25 | Add transparent_abstract tactic | Jason Gross | |
| 2017-04-24 | Removing various tactic compatibility layers in core tactics. | Pierre-Marie Pédrot | |
| 2017-04-21 | Remove VernacError | Gaetan Gilbert | |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-12 | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | |
| 2017-04-12 | [stm] Remove edit_id. | Emilio Jesus Gallego Arias | |
| We remove `edit_id` from the STM. In PIDE they serve a different purpose, however in Coq they were of limited utility and required many special cases all around the code. Indeed, parsing is not an asynchronous operation in Coq, thus having feedback about parsing didn't make much sense. All clients indeed ignore such feedback and handle parsing in a synchronous way. XML protocol clients are unaffected, they rely on the instead on the Fail value. This commit supersedes PR#203. | |||
| 2017-04-11 | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | |
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot | |
| 2017-04-07 | [camlpX] Remove camlp4 compat layer. | Emilio Jesus Gallego Arias | |
| We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes. | |||
| 2017-04-06 | Merge PR#508: Optimize pending evars | Maxime Dénès | |
| 2017-04-06 | Fix a normalization hotspot in computation of constr keys. | Pierre-Marie Pédrot | |
| Getting a key only needs to observe the root of a term. This hotspot was observed in HoTT. | |||
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-04-03 | Merge PR#417: No cast surgery in let in | Maxime Dénès | |
| 2017-04-01 | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | |
| The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. | |||
| 2017-04-01 | Declaring ltac plugin, so that static linking works. | Hugo Herbelin | |
| 2017-04-01 | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | |
| For now we only normalize sorts, and we leave instances for the next commit. | |||
| 2017-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-03-24 | Unifying standard "constr_level" names for constructors of local_binder_expr. | Hugo Herbelin | |
| RawLocal -> CLocal | |||
| 2017-03-24 | Renaming local_binder into local_binder_expr. | Hugo Herbelin | |
| This is a bit long, but it is to keep a symmetry with constr_expr. | |||
| 2017-03-23 | Fast path for implicit tactic solving. | Pierre-Marie Pédrot | |
| We make apparent in the API that the implicit tactic is set or not. This was costing a lot in Pretyping for no useful reason, as it is almost always unset and the default implementation was just failing immediately. | |||
| 2017-03-23 | Ensuring static invariants about handling of pending evars in Pretyping. | Pierre-Marie Pédrot | |
| All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component. | |||
| 2017-03-21 | [pp] Move terminal-specific tagging to the toplevel. | Emilio Jesus Gallego Arias | |
| Previously, tags were associated to terminal styles, which doesn't make sense on terminal-free pretty printing scenarios. This commit moves tag interpretation to the toplevel terminal handling module `Topfmt`. | |||
| 2017-03-21 | [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list` | Emilio Jesus Gallego Arias | |
| This is what has always been used, so it doesn't represent a functional change. This is just a preliminary patch, but many more possibilities could be done wrt tags. | |||
| 2017-03-21 | [pp] Remove unused printing tagging infrastructure. | Emilio Jesus Gallego Arias | |
| Applications of it were not clear/unproven, it made printers more complex (as they needed to be functors) and as it lacked examples it confused some people. The printers now tag unconditionally, it is up to the backends to interpreted the tags. Tagging (and indeed the notion of rich document) should be reworked in a follow-up patch, so they are in sync, but this is a first step. Tested, test-suite passes. Notes: - We remove the `Richprinter` module. It was only used in the `annotate` IDE protocol call, its output was identical to the normal printer (or even inconsistent if taggers were not kept manually in sync). - Note that Richpp didn't need a single change. In particular, its main API entry point `Richpp.rich_pp` is not used by anyone. | |||
| 2017-03-21 | Merge PR#134: Enable `-safe-string` | Maxime Dénès | |
| 2017-03-17 | Merge PR#428: Report missing tactic arguments in error message | Maxime Dénès | |
| 2017-03-17 | Merge PR#445: TACTIC EXTEND now takes an optional level as argument. | Maxime Dénès | |
| 2017-03-15 | Attempt to improve error message when "apply in" fail. | Hugo Herbelin | |
| - Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390. | |||
| 2017-03-14 | [safe-string] ltac/profile_ltac | Emilio Jesus Gallego Arias | |
| No functional change, one extra copy introduced but it seems hard to avoid. | |||
| 2017-03-14 | Report missing tactic arguments in error message | Tej Chajed | |
| Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344). | |||
| 2017-03-14 | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun | Maxime Dénès | |
| 2017-03-03 | [ltac] Move dummy plugin to plugins folder. | Emilio Jesus Gallego Arias | |
| This is needed to fix `Declare ML Module "ltac_plugin". | |||
| 2017-02-27 | Merge PR#395: Allow hintdb to be parameters in a Ltac definition or | Maxime Dénès | |
| Tactic Notation | |||
| 2017-02-24 | TACTIC EXTEND now takes an optional level as argument. | Maxime Dénès | |
| The syntax is: TACTIC EXTEND foo AT LEVEL i This commit makes it possible to define tacticals like the ssreflect arrow without having to resort to GEXTEND statements and intepretation hacks. Note that it simply makes accessible through the ML interface what Tactic Notation already supports: Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ... | |||
| 2017-02-24 | Revert "Add empty ltac_plugin file for forward compatibility." | Maxime Dénès | |
| This reverts commit e8137ae63b3b19436755f372b595e7343e942894, was meant for 8.6 branch only. | |||
| 2017-02-22 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |