| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-11-13 | MacOS package script: do not fail if directory _dmg already exists. | Maxime Dénès | |
| 2015-11-12 | Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms. | Pierre-Marie Pédrot | |
| We retypecheck the hypotheses introduced by the refine primitive instead of blindly trusting them when the unsafe flag is set to false. | |||
| 2015-11-12 | Fixed test-suite file for bug #3998. | Matthieu Sozeau | |
| 2015-11-12 | Update CHANGES | Jason Gross | |
| Mention compatibility file. | |||
| 2015-11-12 | Script building MacOS package. | Maxime Dénès | |
| 2015-11-11 | Now closed. | Matthieu Sozeau | |
| 2015-11-11 | Ensure that conversion is called on terms of the same type in | Matthieu Sozeau | |
| unification (not necessarily preserved due to the fo approximation rule). | |||
| 2015-11-11 | Fix bug #3998: when using typeclass resolution for conversion, allow | Matthieu Sozeau | |
| only one disjoint component of the typeclasses instances to resolve. | |||
| 2015-11-11 | Fix bug #3735: interpretation of "->" in Program follows the standard one. | Matthieu Sozeau | |
| 2015-11-11 | Fix bug #3257, setoid_reflexivity should fail if not completing the goal. | Matthieu Sozeau | |
| 2015-11-11 | Fix bug #4293: ensure let-ins do not contain algebraic universes in | Matthieu Sozeau | |
| their type annotation. | |||
| 2015-11-11 | Fixing bug #3554: Anomaly: Anonymous implicit argument. | Pierre-Marie Pédrot | |
| We just handle unnamed implicits using a dummy name. Note that the implicit argument logic should still output warnings whenever the user writes implicit arguments that won't be taken into account, but I'll leave that for another time. | |||
| 2015-11-10 | Dead code from the commit having introduced primitive projections (a4043608). | Hugo Herbelin | |
| 2015-11-10 | Typo. | Hugo Herbelin | |
| 2015-11-10 | Fixing a bug in reporting ill-formed constructor. | Hugo Herbelin | |
| For instance, Inductive a (x:=1) := C : a -> True. was wrongly reporting Error: The type of constructor C is not valid; its conclusion must be "a" applied to its parameter. Also "simplifying" explain_ind_err. | |||
| 2015-11-10 | Test for bug #4404. | Pierre-Marie Pédrot | |
| 2015-11-10 | Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly. | Pierre-Marie Pédrot | |
| 2015-11-09 | Pushing the backtrace in conversion anomalies. | Pierre-Marie Pédrot | |
| 2015-11-07 | Fixing output test Existentials.v after eec77191b. | 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-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-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 | 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |