| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-27 | Exporting a few primitive tacticals as named Ltac definitions. | Pierre-Marie Pédrot | |
| 2017-05-25 | Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings | Maxime Dénès | |
| 2017-05-25 | Merge PR#608: Allow Ltac2 as a plugin | Maxime Dénès | |
| 2017-05-25 | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès | |
| 2017-05-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias | |
| Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers. | |||
| 2017-05-22 | Using type classes in the interpretation of "specialize" and "contradiction". | Hugo Herbelin | |
| We do that by using constr_with_bindings rather than open_constr_with_bindings (+ extra call to typeclasses in "specialize"). If my understanding is right, the only effect would be to succeed more in cases where it was failing (in inh_conv_coerce_to_gen). In particular, "specialize" and "contradiction" already have a WITHHOLES test for rejecting pending holes. Incidentally, this answers enhancement #5153. | |||
| 2017-05-22 | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin | |
| This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility. | |||
| 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-25 | [location] [ast] Port module AST to CAst | Emilio Jesus Gallego Arias | |
| 2017-04-25 | [location] [ast] Switch Constrexpr AST to an extensible node type. | Emilio Jesus Gallego Arias | |
| Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes. | |||
| 2017-04-25 | [location] Remove `Loc.internal_ghost` | Emilio Jesus Gallego Arias | |
| `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it. | |||
| 2017-04-25 | [location] Make location optional in Loc.located | Emilio Jesus Gallego Arias | |
| This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream. | |||
| 2017-04-25 | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | |
| Now it is a private field, locations are optional. | |||
| 2017-04-24 | [location] Use located in tactics. | Emilio Jesus Gallego Arias | |
| One case missing due the TACTIC EXTEND macro. | |||
| 2017-04-24 | [location] Use located in misctypes. | Emilio Jesus Gallego Arias | |
| 2017-04-24 | [location] Switch glob_constr to Loc.located | Emilio Jesus Gallego Arias | |
| 2017-04-24 | [location] Use Loc.located for constr_expr. | Emilio Jesus Gallego Arias | |
| This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location. | |||
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |