| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-03-05 | Preprend Fail to all the expected failures in the documentation. | Guillaume Melquiond | |
| This commit also removes comments from Coq examples, as they cause extraneous delayed prompts that clutter the output because coq_tex cannot remove them. Some documentation errors were also fixed in the process, since they are easier to spot now that only unexpected failures stand out. | |||
| 2015-03-05 | Do not prepend a "Error:" header when the error is expected by the user. | Guillaume Melquiond | |
| This commit also removes the extraneous "=>" token from Fail messages and prevents them from losing all the formatting information. | |||
| 2015-03-05 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
| 2015-03-05 | MMaps again : adding MMapList, an implementation by ordered list | Pierre Letouzey | |
| 2015-03-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-04 | Introducing MMaps, a modernized FMaps. | Pierre Letouzey | |
| NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty". | |||
| 2015-03-04 | Introducing MMaps, a modernized FMaps. | Pierre Letouzey | |
| NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty". | |||
| 2015-03-04 | Fix bug #3532, providing universe inconsistency information when a | Matthieu Sozeau | |
| unification fails due to that, during a conversion step. | |||
| 2015-03-03 | Fix test-suite file, this is open. | Matthieu Sozeau | |
| 2015-03-03 | Fix bug #3732: firstorder was using detyping to build existential | Matthieu Sozeau | |
| instances and forgeting about the evars and universes that could appear there... dirty hack gone, using the evar map properly and avoiding needless constructions/deconstructions of terms. | |||
| 2015-03-03 | Add missing test-suite files and update gitignore. | Matthieu Sozeau | |
| 2015-03-03 | Add a test-suite file ensuring coinductives with primitive projections | Matthieu Sozeau | |
| do not enjoy eta-conversion and do not allow the usual failure of subject reduction in presence of dependent pattern-matching. | |||
| 2015-03-03 | Fix test-suite file, this is currently a wontfix, but keep the | Matthieu Sozeau | |
| test-suite file for when we move to a better implementation. | |||
| 2015-03-03 | Fix bug #3590, keeping evars that are not turned into named metas by | Matthieu Sozeau | |
| pattern_of_constr in an evar_map, as they can appear in the context of said named metas, which is used by change. Not sure what to do in the PEvar case, which never matches anyway according to Constr_matching.matches. | |||
| 2015-03-03 | Improving display of camlp4/camlp5 versions, library and binary locations. | Hugo Herbelin | |
| 2015-03-03 | Reinstalling search of camlpX in camldir, when given, for | Hugo Herbelin | |
| compatibility with pre-1b7d4a033af heuristic in searching camlpX (continuation of a joint patch with Maxime). Typo basename -> dirname. | |||
| 2015-03-03 | Typos in doc modules. | Hugo Herbelin | |
| 2015-03-03 | Fix bug #4103: forgot to allow unfolding projections of cofixpoints like | Matthieu Sozeau | |
| cases, in some cases. | |||
| 2015-03-03 | Fix bug #4101, noccur_evar's expand_projection can legitimately fail | Matthieu Sozeau | |
| when called from w_unify, so we protect it. | |||
| 2015-03-03 | Fix bug introduced by my last commit, forgetting to adjust de Bruijn | Matthieu Sozeau | |
| index lookup. | |||
| 2015-03-02 | Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into ↵ | Pierre Corbineau | |
| trunk | |||
| 2015-03-02 | rewiring Czar printers that were disabled | Pierre Corbineau | |
| 2015-03-02 | Fix bug #4097. | Matthieu Sozeau | |
| 2015-03-02 | Now accepting unit props in mutual definitions | Bruno Barras | |
| 2015-03-02 | Now accepting unit props in mutual definitions | Bruno Barras | |
| 2015-02-28 | Coq_makefile clean target erases .coq-native dirs in . if they are empty | Pierre Boutillier | |
| 2015-02-28 | Fixing the rule for ml4 depencies in coq_makefile | mlasson | |
| 2015-02-28 | Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ↵ | Pierre Boutillier | |
| r15439 as we were talking at that time) | |||
| 2015-02-28 | Moving Proofview_monad to the engine/ folder. | Pierre-Marie Pédrot | |
| 2015-02-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-27 | Adding a test for bug #3612. | Pierre-Marie Pédrot | |
| 2015-02-27 | Removing the unused field ltacrecvars of tactic internalization. | Pierre-Marie Pédrot | |
| 2015-02-27 | Fixing OCaml 3.12 compilation. | Pierre-Marie Pédrot | |
| 2015-02-27 | Test for bug #3249. | Pierre-Marie Pédrot | |
| 2015-02-27 | Fixing bug #3249. | Pierre-Marie Pédrot | |
| Instead of substituting carelessly the recursive names in Ltac interpretation, we declare them in the environment beforehand, so that they get globalized as themselves. We restore the environment afterwards by transactifying the globalization procedure. | |||
| 2015-02-27 | Taking current env and not global env in b286c9f4f42f (4 commits ago, | Hugo Herbelin | |
| as revealed by #2141). | |||
| 2015-02-27 | simpl: honor Global for "simpl: never" (Close: 3206) | Enrico Tassi | |
| It was an integer overflow! All sorts of memories. | |||
| 2015-02-27 | STM: Considering Stack_overflow as a normal tactic error (Close #3576) | Enrico Tassi | |
| 2015-02-27 | Fix test for #3467, I had moved it in a dumb way. | Maxime Dénès | |
| 2015-02-27 | Add support so that the type of a match in an inductive type with let-in | Hugo Herbelin | |
| is reduced as if without let-in, when applied to arguments. This allows e.g. to have a head-betazeta-reduced goal in the following example. Inductive Foo : let X := Set in X := I : Foo. Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *) | |||
| 2015-02-27 | Hack so that refine_no_check accepts an argument which is a match on an | Hugo Herbelin | |
| inductive type with let-in in the arity (until logic.ml disappears). | |||
| 2015-02-27 | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin | |
| clause in the presence of let-ins in the arity of inductive type). | |||
| 2015-02-27 | Fixing typo resulting in wrong printing of return clauses for | Hugo Herbelin | |
| inductive types with let-in in arity. | |||
| 2015-02-27 | Fix test for #3848, still open. | Maxime Dénès | |
| 2015-02-27 | Moving test for #3467 to closed after PMP's fix. | Maxime Dénès | |
| 2015-02-27 | Fix test-suite files for bugs #2456 and #3593, still open. | Maxime Dénès | |
| 2015-02-27 | Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵ | Guillaume Melquiond | |
| bug #4080) | |||
| 2015-02-27 | Somehow fixing bug #3467. | Pierre-Marie Pédrot | |
| The notations using tactics in term seem now not to respect globalized names. It is not obvious that this is the expected behaviour, but at least it does not die with an anomaly. | |||
| 2015-02-27 | Add test-suite file for #3649. | Maxime Dénès | |
| 2015-02-27 | Moving tests for #2456 and #3593 to "opened" until they're fixed. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |