| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-26 | Fixing bugs in options of the configure. | Hugo Herbelin | |
| - usage ill-formed for -native-compiler - compatibility with the configure of 8.4 (-force-caml-version), though e.g. its force-ocaml-version alias is no longer supported (but at the same time not documented either, so...) | |||
| 2015-10-26 | Preventing using OCaml 4.02.0 for compiling Coq as compilation times | Hugo Herbelin | |
| are redhibitory. | |||
| 2015-10-26 | Documenting a bit more interpretation functions in passing. | Hugo Herbelin | |
| 2015-10-26 | Preserving goal name in revert/bring_hyps. | Hugo Herbelin | |
| 2015-10-26 | Two test-suite files for bugs 3974 and 3975 | Pierre Letouzey | |
| 2015-10-25 | Declaremods: replace two anomalies by user errors (fix #3974 and #3975) | Pierre Letouzey | |
| As shown by the code snippets in these bug reports, I've been too hasty in considering these situations as anomalies in commit 466c4cb (at least the one at the last line of consistency_checks). So let's turn these anomalies back to regular user errors, as they were before this commit. | |||
| 2015-10-25 | Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331) | Pierre Letouzey | |
| 2015-10-25 | Minor module cleanup : error HigherOrderInclude was never happening | Pierre Letouzey | |
| When F is a Functor, doing an 'Include F' triggers the 'Include Self' mechanism: the current context is used as an pseudo-argument to F. This may fail with a subtype error if the current context isn't adequate. | |||
| 2015-10-24 | Fixing a loop in checking hints with holes. | Hugo Herbelin | |
| For instance, "Hint Resolve (fst _ _)." was looping (bug in 841bc461). | |||
| 2015-10-24 | Backtracking on interpreting toplevel calls to exact in scope determined | Hugo Herbelin | |
| by the type to prove (was introduced in 35846ec22, r15978, Nov 2012). Not only it does not work when exact is called via a Ltac definition, but, also, it does not scale easily to refine which is a TACTIC EXTEND. Ideally, one may then want to propagate scope interpretations through ltac variables, as well as supporting refine... See #4034 for a discussion. | |||
| 2015-10-23 | Support "Functional Scheme" in coqdoc. (Fix bug #4382) | Guillaume Melquiond | |
| 2015-10-22 | Fixing a bug in reporting ill-formed inductive. | Hugo Herbelin | |
| Was introduced in b06d3badb (15 Jul 2015). | |||
| 2015-10-21 | Mention bug 3199 fix as a source of incompatibilities. | Matthieu Sozeau | |
| 2015-10-21 | Bug #3956 is fixed. | Matthieu Sozeau | |
| 2015-10-21 | Fixed (and changed) infoH. | Pierre Courtieu | |
| The detection of new hypothesis was bugged. Now infoH behaves like "Show Intros": it performs tac, grab information on hypothesis names but let the state unchanged. FTR: infoH is fundamentally unable to be correct in presence of tactics that delete hypothesis and reuse there names. Like destruct or induction. Fortunately destruct and induction now come with a variant asking that the hypothesis is not deleted. To guess for the right as-close for [induction H], do [infoH induction !H]. This will not create the same names as induction would have by itself but at least there will be the right number of hypothesis. | |||
| 2015-10-20 | Fix lemma-overloading | Matthieu Sozeau | |
| Update the evar_source of the solution evar in evar/evar problems to propagate the information that it does not necessarily have to be solved in Program mode. | |||
| 2015-10-19 | Do occur-check w.r.t existential's types also when instantiating an evar. | Matthieu Sozeau | |
| 2015-10-19 | Categorizing debug messages as such + NonLogical uses loggers. | Pierre Courtieu | |
| 2015-10-19 | Test for #4372 (anomaly in inversion in the presence of fake dependency). | Hugo Herbelin | |
| 2015-10-19 | Turning anomaly into error for #4372 (weakness of inversion in the | Hugo Herbelin | |
| presence of dependent types with only superficial dependency). See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372. | |||
| 2015-10-19 | Partly fixes #3225. Removed some old experimental stuff in funind. | Pierre Courtieu | |
| 2015-10-19 | Fixed #4274, bad formatting of messages in emacs mode. | Pierre Courtieu | |
| 2015-10-19 | Documenting the option "Strict Universe Declaration" in CHANGES. | Pierre-Marie Pédrot | |
| 2015-10-18 | Miscellaneous typos, spacing, US spelling in comments or variable names. | Hugo Herbelin | |
| 2015-10-18 | Using "__" rather than this unelegant arbitrary "A" for the name of ↵ | Hugo Herbelin | |
| variables of the context of an evar in debugging mode. | |||
| 2015-10-18 | Reference Manual: Applying standard style recommendation about not | Hugo Herbelin | |
| starting a sentence with a symbolic expression. | |||
| 2015-10-18 | Fixing #4198 (continued): not matching within the inner lambdas/let-ins | Hugo Herbelin | |
| of the return clause and of the branches (what assumed that the implementation preserves the invariant that the return predicate and the branches are in canonical [fun Δ => t] form, with Δ possibly containing let-ins). | |||
| 2015-10-18 | Using appropriate lambda decomposition function counting let-ins when | Hugo Herbelin | |
| dealing with "match". Contrastingly, "fix" is considered not to count let-ins for finding the recursive argument (which is ok because the last argument is necessarily a lambda). | |||
| 2015-10-18 | Adding a function to mirror decompose_prod_n_assum in that it counts let-ins, | Hugo Herbelin | |
| to compensate decompose_lam_n_assum which does not count let-ins. Any idea on a uniform and clear naming scheme for this kind of decomposition functions? | |||
| 2015-10-17 | Lemmas accept the Local flag. | Pierre-Marie Pédrot | |
| This was a trivial overlook. | |||
| 2015-10-17 | Test for bug #4325. | Pierre-Marie Pédrot | |
| 2015-10-16 | Generalize fix for auto from PMP to eauto and typeclasses eauto. | Matthieu Sozeau | |
| 2015-10-16 | Remove left2right reference from the kernel. | Maxime Dénès | |
| Was introduced by seemingly unrelated commit fd62149f9bf40b3f309ebbfd7497ef7c185436d5. The currently policy is to avoid exposing global references in the kernel interface when easily doable. | |||
| 2015-10-16 | Merge hint lists instead of appending them. (Fix bug #3199) | Guillaume Melquiond | |
| 2015-10-15 | Avoid dependency of the pretyper on C code. | Maxime Dénès | |
| Using the same hack as in the kernel: VM conversion is a reference to a function, updated when modules using C code are actually linked. This hack should one day go away, but always linking C code may produce some other trouble (with the OCaml debugger for instance), so better be safe for now. | |||
| 2015-10-15 | Test file for #4346: Set is no longer of type Type | Maxime Dénès | |
| 2015-10-15 | Fix #4346 2/2: VM casts were not inferring universe constraints. | Maxime Dénès | |
| 2015-10-15 | Fix #4346 1/2: native casts were not inferring universe constraints. | Maxime Dénès | |
| 2015-10-15 | Warn user when bytecode compilation fails. | Maxime Dénès | |
| Previously, the kernel was silently switching back to the standard conversion. | |||
| 2015-10-15 | Remove now useless exception handler in default conversion. | Maxime Dénès | |
| 2015-10-15 | Fix detection of ties in oracle_order. | Guillaume Melquiond | |
| This commit has no impact, since l2r is always false in practice due to the definition of default_conv. | |||
| 2015-10-14 | Reverting modifications in dev/top_printers pushed mistakenly. | Pierre-Marie Pédrot | |
| 2015-10-14 | Fixing perfomance issue of auto hints induced by universes. | Pierre-Marie Pédrot | |
| Instead of brutally merging the whole evarmap coming from the clenv, we remember the context associated to the hint and we only merge that tiny part of constraints. We need to be careful for polymorphic hints though, as we have to refresh them beforehand. | |||
| 2015-10-14 | Fix LemmaOverloading | Matthieu Sozeau | |
| Do not normalize the type of a proof according to the final universes when keep_body_ucst_separate is true, otherwise the type might not be retypable in the initial context... | |||
| 2015-10-14 | Occur-check in evar_define was not strong enough. | Matthieu Sozeau | |
| 2015-10-14 | Fix constr_matching when a match is found in the head of a case construct | Matthieu Sozeau | |
| 2015-10-14 | When typechecking a lemma statement, try to resolve typeclasses before | Matthieu Sozeau | |
| failing for unresolved evars (regression). | |||
| 2015-10-14 | Univs: inductives, remove unneeded test | Matthieu Sozeau | |
| 2015-10-14 | Temporary fix: kernel conversion needs to ignore l2r flag. | Maxime Dénès | |
| Stdlib does not compile when l2r flag is actually taken into account. We should investigate... | |||
| 2015-10-14 | Exporting the original unprocessed hint in the hint running function. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |