| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-11-07 | Preventing an unwanted warning 5 "this function application is partial" | Hugo Herbelin | |
| which e.g. OCaml 4.02.1 displays. | |||
| 2015-11-07 | Implementing assert and cut with LetIn rather than using a beta-redex. | Hugo Herbelin | |
| Hopefully, it will provide with nicer proof terms, in combination with the commit printing the type of LetIn when the defined term is a proof. | |||
| 2015-11-07 | Experimenting printing the type of the defined term of a LetIn when | Hugo Herbelin | |
| this type is a proposition. This is based on the assumption that in Prop, what matters first is the statement. | |||
| 2015-11-07 | Adding an amazing property of Prop. | Hugo Herbelin | |
| 2015-11-07 | Preservation of the name of evars/goals when applying pose/set/intro/clearbody. | Hugo Herbelin | |
| For pose/set/clearbody, I think it is clear that we want to preserve the name and this commit do it. For revert, I first did not preserve the name, then considered in 2ba2ca96be88 that it was better to preserve it. For intro, like for revert actually, I did not preserve the name, based on the idea that the type was changing (*). For instance if we have ?f:nat->nat, do we really want to keep the name f in ?f:nat after an intro. For revert, I changed my mind based on the idea that if we had a better control of the name if we keep the name that if the system invents a new one based on the type. I think this is more reasonable than (*), so this commit preserves the name for intro. For generalize, it is still not done because of generalize being in the old proof engine. | |||
| 2015-11-07 | Tests for syntax "Show id" and [id]:tac (shelved or not). | Hugo Herbelin | |
| 2015-11-07 | Fixing documention of Add Printing Coercion. | 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-30 | More uniformity in the style of comparison functions. | Arnaud Spiwack | |
| 2015-10-29 | Make the code of compare functions linear in the number of constructors. | Arnaud Spiwack | |
| This scheme has been advised by @gashe on #79. Interestingly there are several comparison functions in Coq which were already implemented with this scheme. | |||
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |