| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-02 | Merge PR#708: [ide] Correct merging error. | Maxime Dénès | |
| 2017-06-02 | Merge PR#691: [travis] Add OSX test-suite checking. | Maxime Dénès | |
| 2017-06-02 | Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel. | Maxime Dénès | |
| 2017-06-02 | Merge PR#499: Drop all "theories/*/vo.itarget" files and compute the ↵ | Maxime Dénès | |
| corresponding information automatically. | |||
| 2017-06-02 | Merge PR#515: extract "plugins/micromega/micromega.ml{,i}" files from ↵ | Maxime Dénès | |
| "plugins/micromega/MExtraction.v" | |||
| 2017-06-02 | Merge PR#711: [gitlab] Artifact test suite logs on failure. | Maxime Dénès | |
| 2017-06-01 | [travis] Add OSX test-suite checking. | Maxime Dénès | |
| This is a first step towards getting Travis build our OSX package, but is also useful immediately (c.f. the recent breakage of the coq_makefile test-suite under OSX). | |||
| 2017-06-01 | Test-suite: do not test native compiler if disabled by configure. | Maxime Dénès | |
| 2017-06-01 | drop vo.itarget files and compute the corresponding the corresponding values ↵ | Matej Kosik | |
| automatically instead | |||
| 2017-06-01 | Merge PR#449: make specialize smarter (bug 5370). | Maxime Dénès | |
| 2017-06-01 | Merge PR#670: Postponing of universe constraints unification in term equality. | Maxime Dénès | |
| 2017-06-01 | [emacs] [toplevel] Make emacs flag local to the toplevel. | Emilio Jesus Gallego Arias | |
| We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel. | |||
| 2017-06-01 | Merge PR#696: Trunk+cleanup constr of global | Maxime Dénès | |
| 2017-06-01 | Remove a post merge warning. | Maxime Dénès | |
| 2017-06-01 | Merge PR#561: Improving the Name API | Maxime Dénès | |
| 2017-06-01 | Fix coq_makefile uninstall target under OSX. | Maxime Dénès | |
| 2017-06-01 | Merge PR#694: Fixing #5523 (missing support for complex constructions in ↵ | Maxime Dénès | |
| recursive notations) (bis) | |||
| 2017-06-01 | Break circular dependency in MExtraction | Jason Gross | |
| Described in https://github.com/coq/coq/pull/515#discussion_r119230833 | |||
| 2017-06-01 | a solution that works also with make 3.81 | Matej Kosik | |
| 2017-06-01 | extract "plugins/micromega/micromega.ml{,i}" files from ↵ | Matej Kosik | |
| "plugins/micromega/MExtraction.v" | |||
| 2017-06-01 | Merge PR#704: Fix empty parentheses display in test-suite | Maxime Dénès | |
| 2017-05-31 | Merge PR#701: [readlink -f] doesn't work on OSX | Maxime Dénès | |
| 2017-05-31 | Merge PR#248: Adding eassert, eset, epose, etc. | Maxime Dénès | |
| 2017-05-31 | Makefile.build: test-suite all = run + report, so don't report again | Gaëtan Gilbert | |
| 2017-05-31 | [travis] print failing test suite logs on failure | Gaëtan Gilbert | |
| 2017-05-31 | Tests for new specialize feature + CHANGES. | Pierre Courtieu | |
| 2017-05-31 | Documenting the new behaviour of specialize. | Pierre Courtieu | |
| 2017-05-31 | Make specialize smarter. | Pierre Courtieu | |
| Now when a partial with-binding is given the unsolved parameters are left quantified. A letin is added when mixing (fun x => ...) and with-bindings. | |||
| 2017-05-31 | Merge PR#700: make sure that "ocamllibdep" properly recognizes Ocaml that ↵ | Maxime Dénès | |
| are composed from uppercase letters | |||
| 2017-05-31 | Creating a module Nameops.Name extending module Names.Name. | Hugo Herbelin | |
| This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name. | |||
| 2017-05-31 | Renaming interp_rawcontext_evars using a more "standard" name. | Hugo Herbelin | |
| 2017-05-31 | Fixing #5523 (missing support for complex constructions in recursive notations). | Hugo Herbelin | |
| We get rid of a complex function doing both an incremental comparison and an effect on names (Notation_ops.compare_glob_constr). For the effect on names, it was actually already done at the time of turning glob_constr to notation_constr, so it could be skipped here. For the comparison, we rely on a new incremental variant of Glob_ops.glob_eq_constr (thanks to Gaëtan for getting rid of the artificial recursivity in mk_glob_constr_eq). Seizing the opportunity to get rid of catch-all clauses in pattern-matching (as advocated by Maxime). Also make indentation closer to the one of other functions. | |||
| 2017-05-31 | Fixing a too lax constraint for finding recursive binder part of a notation. | Hugo Herbelin | |
| This was preventing to work examples such as: Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))). | |||
| 2017-05-30 | [ide] Correct merging error. | Emilio Jesus Gallego Arias | |
| There was a mistake in the conflict resolution of merge 6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 which wrongly undid the the deletion of the file `ide/texmacspp.ml` in 6a412da , fixing here and sorry for the problem. | |||
| 2017-05-30 | Merge PR#706: Add some test-suite generated files to .gitignore | Maxime Dénès | |
| 2017-05-30 | [gitlab] Artifact test suite logs on failure. | Gaëtan Gilbert | |
| 2017-05-30 | Add some test-suite generated files to .gitignore | Jason Gross | |
| 2017-05-30 | Fix empty parentheses display in test-suite | Jason Gross | |
| There was an extra trailing space in #680. Now things display as, e.g., ``` TEST bugs/opened/3754.v TEST bugs/opened/4803.v (-compat 8.4) ``` instead of ``` TEST bugs/opened/3754.v ( ) TEST bugs/opened/4803.v (-compat 8.4 ) ``` | |||
| 2017-05-30 | [readlink -f] doesn't work on OSX | Gaëtan Gilbert | |
| We only want an absolute path, no need to follow symlinks. | |||
| 2017-05-30 | Support for using type information to infer more precise evar sources. | Hugo Herbelin | |
| This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted). | |||
| 2017-05-30 | Documentation for eassert, eenough, epose proof, eset, eremember, epose. | Hugo Herbelin | |
| Includes fixes and suggestions from Théo. | |||
| 2017-05-30 | Few tests for e-variants of assert, set, remember. | Hugo Herbelin | |
| 2017-05-30 | Adding "epose", "eset", "eremember" which allow to set terms with | Hugo Herbelin | |
| evars. This is for consistency with the rest of the language. For instance, "eremember" and "epose" are supposed to refer to terms occurring in the goal, hence not leaving evars, hence in general pointless. Eventually, I guess that "e" should be a modifier (see e.g. the discussion at #3872), or the difference is removed. | |||
| 2017-05-30 | Adding "eassert", "eenough", "epose proof", which allow to state | Hugo Herbelin | |
| a goal with unresolved evars. | |||
| 2017-05-30 | make sure that "ocamllibdep" properly recognizes Ocaml modules that are all ↵ | Matej Košík | |
| upper-case At the moment, when one tries to add an Ocaml module to Coq code-base which is composed just from upper-cases letters, the compilation fails with an error: File "......ml", line 1: Error: Error while linking ... Reference to undefined global `FOO' This commit removes the restriction. | |||
| 2017-05-30 | Merge PR#356: Making management of installation directories more structured, ↵ | Maxime Dénès | |
| more uniform | |||
| 2017-05-30 | Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3 | Maxime Dénès | |
| 2017-05-29 | Merge PR#687: Gitlab CI | Maxime Dénès | |
| 2017-05-29 | Pretyping cleanup: remove constr_of_global calls | Matthieu Sozeau | |
| 2017-05-29 | tactics cleanup: remove constr_of_global calls | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |