| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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#481: [option] Remove support for non-synchronous options. | Maxime Dénès | |
| 2017-05-25 | Merge PR#406: coq makefile2 | Maxime Dénès | |
| 2017-05-25 | [location] [travis] Add overlays for located_switch | Emilio Jesus Gallego Arias | |
| 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-23 | Add parsers-examples target to fiat-parsers ci | Jason Gross | |
| This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build. | |||
| 2017-05-23 | overlay for UniMath | Enrico Tassi | |
| 2017-05-23 | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias | |
| We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc... | |||
| 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-18 | Fix a typo | Jason Gross | |
| 2017-05-17 | Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵ | Maxime Dénès | |
| tricks available to users | |||
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-05-16 | Adding support for using grammar entries returning no value in EXTEND. | Hugo Herbelin | |
| 2017-05-10 | Switch bedrock to mit-plv base | Jason Gross | |
| 2017-05-08 | Fix warnings in top_printers | Gaetan Gilbert | |
| Note that [@@@ocaml.warning "-32"] caused an error with Drop. It was put there because I didn't realise the warning was about a real issue. | |||
| 2017-05-02 | Merge PR#582: Fix warnings | Maxime Dénès | |
| 2017-05-01 | Add bmsherman/topology to the ci | Jason Gross | |
| This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk. | |||
| 2017-05-01 | More consistent writing of de Bruijn. | Théo Zimmermann | |
| 2017-05-01 | Fix for bug 5507. Mispelt de Bruijn. | Théo Zimmermann | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Locally disable some warnings. | Gaetan Gilbert | |
| 2017-04-27 | Merge PR#568: Remove tactic compatibility layer | Maxime Dénès | |
| 2017-04-27 | Document the API changes. | Pierre-Marie Pédrot | |
| 2017-04-27 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-04-25 | [located] [doc] Improve docs for `CAst.ast`. | Emilio Jesus Gallego Arias | |
| 2017-04-25 | [travis] mathcomp and fiat overlay for #402 | Emilio Jesus Gallego Arias | |
| 2017-04-25 | [location] Document changes. | Emilio Jesus Gallego Arias | |
| 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] Remove Loc.ghost. | Emilio Jesus Gallego Arias | |
| Now it is a private field, locations are optional. | |||
| 2017-04-24 | [location] Switch glob_constr to Loc.located | Emilio Jesus Gallego Arias | |
| 2017-04-24 | Adding a dedicated travis overlay for fiat-parsers. | Pierre-Marie Pédrot | |
| 2017-04-20 | Add bedrock targets src and facade | Jason Gross | |
| 2017-04-19 | Documenting EConstr for developpers. | Pierre-Marie Pédrot | |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-14 | Fix EOL characters in xml protocol documentation. | Maxime Dénès | |
| 2017-04-14 | Merge PR#563: add XML protocol doc for 8.6 | Maxime Dénès | |
| 2017-04-14 | [travis] Use the lite target for fiat-crypto. | Maxime Dénès | |
| 2017-04-13 | update XML protocol doc to 8.6 | Paul Steckler | |
| 2017-04-13 | add XML protocol doc for 8.5 | Paul Steckler | |
| 2017-04-12 | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | |
| 2017-04-12 | [stm] Improve error messages on add/parse. | Emilio Jesus Gallego Arias | |
| As suggested by @psteckler in #524 , we give more explicit information about what is wrong. We also provide some debug information for the possible dangerous case of having the tip go out of sync with the real installed state (which will make parsing fail if there was some changes to the parser). We also fix a couple of typos noticed by Paul, thanks Paul. | |||
| 2017-04-12 | [stm] Port the toplevel to the STM. | Emilio Jesus Gallego Arias | |
| - We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled. | |||
| 2017-04-12 | [stm] Move main parsing entry point to the STM. | Emilio Jesus Gallego Arias | |
| Mainly due to notations, proof modes and plugins, parsing in Coq is stateful, so we expose a state-aware parsing API in the STM. This is a first move to unify all the parsing entry points in the Stm and the toplevel, and allows STM clients to control their input stream properly. This greatly helps for instance, with whole-document parsing. This commit supersedes PR#204. | |||
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵ | Maxime Dénès | |
| record fields. | |||
| 2017-04-11 | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | |
| 2017-04-07 | Merge PR#461: [camlpX] Remove camlp4 compat layer. | Maxime Dénès | |
| 2017-04-07 | Fixes for Drop. to work (decl_mode removal and toplevel -> vernac) | Matthieu Sozeau | |
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot | |
| 2017-04-07 | [travis] Overlay for PR#461: Camlp4 removal. | Emilio Jesus Gallego Arias | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |