| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-11-18 | Slightly documenting code for building primitive projections. | Hugo Herbelin | |
| 2015-11-18 | Fixing logical bugs in the presence of let-ins in computiong primitive | Hugo Herbelin | |
| projections. - lift accounting for the record missing in computing the subst from fields to projections of the record - substitution for parameters should not lift the local definitions - typo in building the latter (subst -> letsubst) | |||
| 2015-11-17 | More optimizations of [Clenv.clenv_fchain]. | Pierre-Marie Pédrot | |
| Everywhere we know that the universes of the left argument are an extension of the right argument, we do not have to merge universes. | |||
| 2015-11-17 | Performance fix for destruct. | Pierre-Marie Pédrot | |
| The clenv_fchain function was needlessly merging universes coming from two evarmaps even though one was an extension of the other. A flag was added so that the tactic just retrieves the newer universes. | |||
| 2015-11-16 | Being more precise and faithful about the origin of the file reporting | Hugo Herbelin | |
| about the prehistory of Coq. | |||
| 2015-11-13 | Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly. | Matthieu Sozeau | |
| 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! | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |