| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Merge branch 'v8.6' |  Pierre-Marie Pédrot | 2016-10-29 |
| |\ | |||
| | * | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-29 |
| | |\ | |||
| | * | | Removing dead code. |  Hugo Herbelin | 2016-10-29 |
| | * | | Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c). | Hugo Herbelin | 2016-10-29 |
| | * | | Fixing #5164 (regression in locating error in argument of "refine"). | Hugo Herbelin | 2016-10-29 |
| | * | | Merge remote-tracking branch 'github/pr/321' into v8.6 |  Maxime Dénès | 2016-10-28 |
| | |\ \ | |||
| | * \ \ | Merge remote-tracking branch 'github/pr/319' into v8.6 | Maxime Dénès | 2016-10-28 |
| | |\ \ \ | |||
| | * \ \ \ | Merge commit 'fccbd64' into v8.6 | Maxime Dénès | 2016-10-28 |
| | |\ \ \ \ | |||
| | | * | | | | [build] Add a target to install the META file. |  Emilio Jesus Gallego Arias | 2016-10-28 |
| | | * | | | | [build] META file to enable plugin linking with ocamlfind. | Emilio Jesus Gallego Arias | 2016-10-28 |
| | * | | | | | Merge remote-tracking branch 'github/pr/337' into v8.6 | Maxime Dénès | 2016-10-28 |
| | |\ \ \ \ \ | |||
| | | | | | | * | Fixing #5161 (case of a notation with unability to detect a recursive binder). | Hugo Herbelin | 2016-10-27 |
| * | | | | | | | COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it ... |  Matej Kosik | 2016-10-27 |
| | | * | | | | | Add missing dot to impargs error message. | Maxime Dénès | 2016-10-27 |
| | | * | | | | | Proper fix for #3753 (anomaly with implicit arguments and renamings) | Maxime Dénès | 2016-10-27 |
| | | * | | | | | Complete overhaul of the Arguments vernacular. | Maxime Dénès | 2016-10-27 |
| | * | | | | | | Using msg_info for info_auto and info_eauto (PR #324). | Hugo Herbelin | 2016-10-26 |
| | * | | | | | | STM: make ~valid state id non optional from APIs |  Enrico Tassi | 2016-10-26 |
| | * | | | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-26 |
| | |\ \ \ \ \ \ | | | |_|_|_|/ | | |/| | | | | |||
| * | | | | | | | COMMENT: Namegen.next_ident_away | Matej Kosik | 2016-10-26 |
| * | | | | | | | COMMENT: Declarations.constant_def | Matej Kosik | 2016-10-26 |
| * | | | | | | | COMMENT: Names.Cmap and Names.Cmap_env | Matej Kosik | 2016-10-26 |
| * | | | | | | | COMMENT: Proofview.entry | Matej Kosik | 2016-10-26 |
| * | | | | | | | COMMENT: Constr.kind_of_term | Matej Kosik | 2016-10-26 |
| | | * | | | | | Merge remote-tracking branch 'github/pr/338' into v8.5 | Maxime Dénès | 2016-10-25 |
| | | |\ \ \ \ \ | |||
| | | | * | | | | | Remove warning now that info_auto is fixed. |  Théo Zimmermann | 2016-10-25 |
| | | * | | | | | | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | Maxime Dénès | 2016-10-25 |
| | | |/ / / / / | |||
| | * | | | | | | Merge commit 'a799600' into v8.6 | Maxime Dénès | 2016-10-25 |
| | |\ \ \ \ \ \ | |||
| | | * | | | | | | That Function is unable to create a Fixpoint equation is a user problem, |  Yves Bertot | 2016-10-25 |
| | | | * | | | | | Update CHANGES. | Maxime Dénès | 2016-10-25 |
| | | | * | | | | | Bump version number to 8.5pl3. | Maxime Dénès | 2016-10-25 |
| | | | * | | | | | Merge remote-tracking branch 'github/pr/333' into v8.5 | Maxime Dénès | 2016-10-25 |
| | | | |\ \ \ \ \ | |||
| | | | * \ \ \ \ \ | Merge remote-tracking branch 'github/pr/329' into v8.5 | Maxime Dénès | 2016-10-25 |
| | | | |\ \ \ \ \ \ | |||
| * | | | | | | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-24 |
| |\| | | | | | | | | | |||
| | * | | | | | | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-24 |
| | |\ \ \ \ \ \ \ \ \ | | | |/ / / / / / / | | |/| | | | | | | | |||
| | * | | | | | | | | | Adding a test for #4398 (interpretation scopes for "match goal"). | Hugo Herbelin | 2016-10-24 |
| | * | | | | | | | | | Rename lia.cache into .lia.cache in the test-suite Makefile. | Maxime Dénès | 2016-10-24 |
| | * | | | | | | | | | Merge commit '81bdc22' into v8.6 | Maxime Dénès | 2016-10-24 |
| | |\ \ \ \ \ \ \ \ \ | |||
| | | | * \ \ \ \ \ \ \ | Merge remote-tracking branch 'github/pr/326' into v8.5 | Maxime Dénès | 2016-10-24 |
| | | | |\ \ \ \ \ \ \ \ | |||
| | | | | | | * | | | | | | Test file for #5127: Memory corruption with the VM | Maxime Dénès | 2016-10-24 |
| | | | | | | * | | | | | | Fix #5127 Memory corruption with the VM | Maxime Dénès | 2016-10-24 |
| | * | | | | | | | | | | | Merge branch 'v8.5' into v8.6 | Hugo Herbelin | 2016-10-24 |
| | * | | | | | | | | | | | ssrmatching: fix interpretation of rpattern | Enrico Tassi | 2016-10-24 |
| | | |_|_|/ / / / / / / | |/| | | | | | | | | | |||
| | | | * | | | | | | | | Fixing a location bug with "?" and "$". | Hugo Herbelin | 2016-10-24 |
| | | | * | | | | | | | | Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}"). | Hugo Herbelin | 2016-10-24 |
| | | | | |/ / / / / / | | | |/| | | | | | | |||
| | | * | | | | | | | | Update .gitignore with new names for psatz caches |  Jason Gross | 2016-10-24 |
| | | | * | | | | | | | Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit too strong. | Hugo Herbelin | 2016-10-24 |
| | * | | | | | | | | | Merge branch 'v8.5' into v8.6 | Hugo Herbelin | 2016-10-22 |
| | |\ \ \ \ \ \ \ \ \ | | | |/ / / / / / / | | |/| | | | | | | | |||
| | | * | | | | | | | | Remove incorrect assertion in cbn (bug #4822). |  Guillaume Melquiond | 2016-10-22 |
| | | * | | | | | | | | Do not stop propagation of signals when Coq is busy (bug #3941). | Guillaume Melquiond | 2016-10-22 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |