Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7860: Fix #7704: Launching coqide through PATH fails. | Emilio Jesus Gallego Arias | 2018-06-28 |
|\ | |||
* \ | Merge PR #7866: Implementation of mutual records in the higher strata | Maxime Dénès | 2018-06-28 |
|\ \ | |||
* \ \ | Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false) | Pierre-Marie Pédrot | 2018-06-27 |
|\ \ \ | |||
| * | | | Test file for #7723 | Maxime Dénès | 2018-06-27 |
| | | | | |||
* | | | | Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations). | Hugo Herbelin | 2018-06-26 |
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We fix the issue by removing terms of the substitutions which have free variables and are thus not interpretable in the context of the "ltac:" subterm. This remains rather ad hoc, since, in an expression "Notation f x := ltac:(foo)", we interpret "x" at calling time of "foo" rather than at use time of "x" in foo, even if "x" is not necessary. We could also imagine that binders in the ltac expressions are then interpreted but that would start to be (very) complicated. Note that this will presumably "fix" ltac2 quotations at the same time. | ||
* | | | Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵ | Matthieu Sozeau | 2018-06-25 |
|\ \ \ | | | | | | | | | | | | | subtyping. | ||
* \ \ \ | Merge PR #7559: Existing Class noop when already a class + warning. | Matthieu Sozeau | 2018-06-25 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7620: [ssr] rewrite: turn anomaly into regular error | Maxime Dénès | 2018-06-25 |
|\ \ \ \ \ | |||
| | | | * | | Adding various tests for mutual records. | Pierre-Marie Pédrot | 2018-06-24 |
| |_|_|/ / |/| | | | | |||
* | | | | | Merge PR #7236: [ssr] simpler semantics for delayed clears | Maxime Dénès | 2018-06-23 |
|\ \ \ \ \ | |||
| | | | | * | Fix #7704: get_toplevel_path needs normalised argv.(0) | Gaëtan Gilbert | 2018-06-22 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When launched through PATH argv.(0) is just the command name. eg "coqtop -compile foo.v" -> argv.(0) = "coqtop" Using executable_name also follows symlinks but this isn't tested to avoid messing with windows. Running Coq through a symlink is not as important as PATH anyways. | ||
| | | | * | | Remove hack skipping comparison of algebraic universes in subtyping. | Gaëtan Gilbert | 2018-06-22 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!). | ||
| * | | | | | [ssr] implement {}/v as a short hand for {v}/v when v is an id | Enrico Tassi | 2018-06-22 |
| | |_|/ / | |/| | | | |||
* / | | | | [ssr] test case for rewrite and set on univ poly keys | Enrico Tassi | 2018-06-22 |
|/ / / / | |||
| * / / | [ssr] test case for rewrite (setoid) making the goal illtyped | Enrico Tassi | 2018-06-20 |
|/ / / | |||
* | | | Merge PR #6754: Better elaboration of pattern-matchings on primitive projections | Pierre-Marie Pédrot | 2018-06-19 |
|\ \ \ | |||
* | | | | Fix #7421: constr_eq ignores universe constraints. | Gaëtan Gilbert | 2018-06-18 |
| |_|/ |/| | | | | | | | | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong. | ||
* | | | Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related ↵ | Pierre-Marie Pédrot | 2018-06-17 |
|\ \ \ | | | | | | | | | | | | | to "match"). | ||
* \ \ \ | Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretyping | Pierre-Marie Pédrot | 2018-06-17 |
|\ \ \ \ | |||
| | * | | | Fixes #7811 (uncaught Not_found in notation printer related to "match"). | Hugo Herbelin | 2018-06-17 |
| |/ / / |/| | | | |||
* | | | | Merge PR #7616: Fix #7615: Functor inlining drops universe substitution. | Maxime Dénès | 2018-06-17 |
|\ \ \ \ | |||
| | | * | | Add test-suite case for performance, had to use Timeout | Matthieu Sozeau | 2018-06-15 |
| | | | | | |||
| | | * | | Better elaboration of pattern-matchings on primitive projections | Matthieu Sozeau | 2018-06-15 |
| |_|/ / |/| | | | | | | | | | | | | | | | This ensures that computations are shared as much as possible, mimicking the "positive" records computational behavior if possible. | ||
| | * | | Do not allow spliting in res_pf, this is reserved for pretyping | Matthieu Sozeau | 2018-06-15 |
| | | | | |||
* | | | | Workaround to handle non-value arguments in tactics. | Cyprien Mangin | 2018-06-14 |
| |/ / |/| | | | | | | | | | | | Although the fix is not a proper one, it seems to solve every instance of #2800 that could be tested. | ||
* | | | Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ↵ | Pierre-Marie Pédrot | 2018-06-14 |
|\ \ \ | | | | | | | | | | | | | of submodules. | ||
* \ \ \ | Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵ | Matthieu Sozeau | 2018-06-14 |
|\ \ \ \ | | | | | | | | | | | | | | | | to anomaly) | ||
* \ \ \ \ | Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder ↵ | Matthieu Sozeau | 2018-06-14 |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | in unification | ||
* \ \ \ \ \ | Merge PR #7771: Tweak printing boxes for unicode binders | Hugo Herbelin | 2018-06-14 |
|\ \ \ \ \ \ | |||
* | | | | | | | Markdown docs: switch from absolute to relative links. | Théo Zimmermann | 2018-06-13 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip] | ||
* | | | | | | | Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn"). | Hugo Herbelin | 2018-06-12 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a quick fix. Code should be made nicer along these lines: - try to pass the name of the variable created by "mkletin_goal" in the monad using "refine_one"; - use a disjunctive type of "inhyps" to indicate when it is meaningful, rather than using []. | ||
| | * | | | | | Fixes #7780 (missing lift in expanding alias under a binder in unification). | Hugo Herbelin | 2018-06-12 |
| |/ / / / / |/| | | | | | |||
| * | | | | | Tweak printing boxes for unicode binders | Ralf Jung | 2018-06-10 |
| | | | | | | |||
* | | | | | | Fixing #7700 (section variables bound to abbreviations were not found). | Hugo Herbelin | 2018-06-10 |
|/ / / / / | | | | | | | | | | | | | | | | | | | | | Redundancy between finding section variables in both interp_var and interp_qualid could probably be cleaned. | ||
| | | | * | Existing Class noop when already a class + warning. | Gaëtan Gilbert | 2018-06-08 |
| |_|_|/ |/| | | | | | | | | | | | Fix #5012. | ||
* | | | | add test for #7595 | Ralf Jung | 2018-06-07 |
| | | | | |||
| | | * | Fix #7615: Functor inlining drops universe substitution. | Pierre-Marie Pédrot | 2018-06-07 |
| |_|/ |/| | | | | | | | | | | | | | | | | | We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case. | ||
* | | | Merge PR #7077: Preserving canonical structure of return predicate in ↵ | Maxime Dénès | 2018-06-05 |
|\ \ \ | | | | | | | | | | | | | vm_compute and native_compute (partial fix to #7068; also fixes #7076)) | ||
* \ \ \ | Merge PR #7663: test suite: make target to regenerate failing output tests | Enrico Tassi | 2018-06-05 |
|\ \ \ \ | |||
* | | | | | Fix #7631: native_compute fails to compile an example in Coq 8.8 | Maxime Dénès | 2018-06-04 |
| | | | | | | | | | | | | | | | | | | | | | | | | | Dependency analysis for separate compilation was not iterated properly on rel_context and named_context. | ||
* | | | | | Merge PR #7315: An attempt to clarify error message for Arguments needing ↵ | Maxime Dénès | 2018-06-04 |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | "rename" flag | ||
| | | * | | | Tests for part of #7068 and for #7076 (vm/native_compute and return predicate). | Hugo Herbelin | 2018-06-04 |
| |_|/ / / |/| | | | | |||
* | | | | | Merge PR #7229: Deprecate implicit tactic solving. | Hugo Herbelin | 2018-06-04 |
|\ \ \ \ \ | |||
| | | * | | | test suite: make target to regenerate failing output tests | Gaëtan Gilbert | 2018-06-04 |
| | | | | | | |||
* | | | | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵ | Matthieu Sozeau | 2018-06-04 |
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | pattern-matching names | ||
* \ \ \ \ \ \ | Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode. | Matthieu Sozeau | 2018-06-04 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly | Matthieu Sozeau | 2018-06-04 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #7189: Fix #5539: algebraic universe produced by cases. | Matthieu Sozeau | 2018-06-04 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵ | Matthieu Sozeau | 2018-06-04 |
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | tactic unification. | ||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵ | Matthieu Sozeau | 2018-06-04 |
|\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | coinductive types. |