| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-11-07 | Adding an amazing property of Prop. | Hugo Herbelin | |
| 2015-11-07 | Merge remote-tracking branch 'origin/v8.5' into upstream-trunk | Hugo Herbelin | |
| - Had to add a Sigma.to_evar_map - Had to rework coqdep_common.ml{,i} and coqdep.ml | |||
| 2015-11-06 | Fixed #4407. | Pierre Courtieu | |
| Like coqc: detect if the current directory was set by options, if not: add it with empty logical path. TODO: check if coq_makefile is still correct wrt to this modification, I think yes, actually it should end being more correct. | |||
| 2015-11-06 | Fixing #4406 coqdep: No recursive search of ml (-I). | Pierre Courtieu | |
| 2015-11-06 | Fixing complexity file f_equal.v. | Hugo Herbelin | |
| 2015-11-06 | More on how to compile doc. | Hugo Herbelin | |
| 2015-11-06 | Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan | Hugo Herbelin | |
| for reporting it. A "cut" was not appropriately chained on the second goal but on both goals, with the chaining on the first goal introducing noise. | |||
| 2015-11-05 | Add test-suite file for #4273. | Matthieu Sozeau | |
| 2015-11-05 | Fix bug #4273 | Matthieu Sozeau | |
| Syntactic analysis of dependencies when atomizing arguments in destruct was not dealing properly with primitive projections hiding their parameters. | |||
| 2015-11-05 | Update version numbers and magic numbers for 8.5beta3 release. | Maxime Dénès | |
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-04 | Checker was forgetting to register global universes introduced by opaque | Matthieu Sozeau | |
| proofs. | |||
| 2015-11-04 | Univs: missing checks in evarsolve with candidates and missing a | Matthieu Sozeau | |
| whd_evar in refresh_universes. | |||
| 2015-11-04 | Univs: update refman, better printers for universe contexts. | Matthieu Sozeau | |
| 2015-11-04 | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau | |
| inconsistent). | |||
| 2015-11-04 | Univs: compatibility with 8.4. | Matthieu Sozeau | |
| When refreshing a type variable, always use a rigid universe to force the most general universe constraint, as in 8.4. | |||
| 2015-11-04 | Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion | Matthieu Sozeau | |
| is buggy in general. | |||
| 2015-11-04 | Test file for #4397. | Maxime Dénès | |
| 2015-11-03 | Update compatibility file for some of bug #4392 | Jason Gross | |
| Now doing ```coq Tactic Notation "left" "~" := left. Tactic Notation "left" "*" := left. ``` will no longer break the `left` tactic in Coq 8.4. List obtained via ``` grep -o '^ \[[^]]*\]' tactics/coretactics.ml4 | sed s'/^ \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g' ``` | |||
| 2015-11-02 | Fix bug #4397: refreshing types in abstract_generalize. | Matthieu Sozeau | |
| 2015-11-02 | Fix bug #4151: discrepancy between exact and eexact/eassumption. | Matthieu Sozeau | |
| 2015-11-02 | Refresh rigid universes as well, and in 8.4 compatibility mode, | Matthieu Sozeau | |
| make them rigid to disallow minimization. | |||
| 2015-11-02 | Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico. | Maxime Dénès | |
| 2015-11-02 | Adding syntax "Show id" to show goal named id (shelved or not). | Hugo Herbelin | |
| 2015-11-02 | Made that the syntax [id]:tac also applies to the shelve, which is after all ↵ | Hugo Herbelin | |
| its main interest! | |||
| 2015-11-02 | STM: fix undo into a branch containing side effects | Enrico Tassi | |
| The "master" label used to be reset to the wrong id | |||
| 2015-11-02 | STM: never reopen a branch containing side effects | Enrico Tassi | |
| 2015-10-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-30 | Command.declare_definition: grab the fix_exn early (follows 77cf18e) | Enrico Tassi | |
| When a future is fully forced (joined), the fix_exn is dropped, since joined futures are values (hence they cannot raise exceptions). When a future for a transparent definition enters the environment it is joined. If one needs to pick its fix_exn, he should do it before that. | |||
| 2015-10-30 | Manually expand red_tactic so that notations do not break reduction tactics. ↵ | Guillaume Melquiond | |
| (Fix bug #3654) | |||
| 2015-10-30 | Add a way to get the right fix_exn in external vernacular commands | Matthieu Sozeau | |
| involving Futures. | |||
| 2015-10-30 | Fix typo. | Guillaume Melquiond | |
| 2015-10-29 | Monotonizing Tactics.change_arg. | Pierre-Marie Pédrot | |
| 2015-10-29 | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau | |
| universes are declared correctly in the enclosing proofs evar_map's. | |||
| 2015-10-29 | Collect subproof universes in handle_side_effects. | Matthieu Sozeau | |
| 2015-10-29 | Removing some goal unsafeness in Equality. | Pierre-Marie Pédrot | |
| 2015-10-29 | Removing unused and useless exported function in Hints. | Pierre-Marie Pédrot | |
| 2015-10-29 | Removing the evar_map argument from s_enter. | Pierre-Marie Pédrot | |
| 2015-10-29 | Removing some goal unsafeness in inductive schemes. | Pierre-Marie Pédrot | |
| 2015-10-29 | Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392) | Guillaume Melquiond | |
| Without this expansion, camlp4 fails to properly factor a user notation starting with either "trivial" or "auto". | |||
| 2015-10-29 | Avoid an anomaly when destructing an unknown ident. (Fix bug #4395) | Guillaume Melquiond | |
| It is too bad that OCaml does not warn when catching an exception over a closure rather than inside it. | |||
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin | |
| presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger. | |||
| 2015-10-29 | Cleanup API and comments of 908dcd613 | Enrico Tassi | |
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-29 | Accept option -compat 8.5. (Fix bug #4393) | Guillaume Melquiond | |
| 2015-10-28 | Univs: local names handling. | Matthieu Sozeau | |
| Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. | |||
| 2015-10-28 | Printing of @{} instances for polymorphic references in Print and About. | Matthieu Sozeau | |
| 2015-10-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi | |
| Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. | |||
| 2015-10-28 | lib_stack: API to reorder the libstack | Enrico Tassi | |
| For discharging it is important that constants occur in the libstack in an order that respects the dependencies among them. This is impossible to achieve for private constants when they are exported globally without this (ugly IMO) api. | |||
| 2015-10-28 | Fix test suite after Matthieu's ed7af646f2e486b. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |