| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-27 | Type-safe grammar extensions. | Pierre-Marie Pédrot | |
| 2015-10-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-26 | Pcoq entries are given a proper module. | Pierre-Marie Pédrot | |
| Entries defined in the Pcoq AST of symbols must be marshallable, because they are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as they contain functional values. This is why the Pcoq module used a pair [string * string] to describe entries. It is obviously type-unsafe, so we define a new abstract type in its own module. There is a little issue though, which is that our entries and CAMLP4/5 entries must be kept synchronized through an association table. The Pcoq module tries to maintain this invariant. | |||
| 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 | Getting rid of the Atactic entry. | Pierre-Marie Pédrot | |
| 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-25 | Getting rid of the Agram entry. | Pierre-Marie Pédrot | |
| 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-22 | Using GADTs in Xmlprotocol. | Pierre-Marie Pédrot | |
| This removes 109 Obj.magic in one patch! | |||
| 2015-10-21 | Pcoq.prod_entry_key now uses a GADT to statically enforce typedness. | Pierre-Marie Pédrot | |
| 2015-10-21 | Turn Pcoq into a regular ML file. | Pierre-Marie Pédrot | |
| 2015-10-21 | Expanding the grammar extensions of Pcoq. | Pierre-Marie Pédrot | |
| 2015-10-21 | Removing the dependencies of Pcoq in IFDEF macros. | Pierre-Marie Pédrot | |
| 2015-10-21 | Mention bug 3199 fix as a source of incompatibilities. | Matthieu Sozeau | |
| 2015-10-21 | Expliciting some uses of Compat module. | Pierre-Marie Pédrot | |
| 2015-10-21 | Bug #3956 is fixed. | Matthieu Sozeau | |
| 2015-10-21 | Removing test for bug #3956. | Pierre-Marie Pédrot | |
| It breaks test-suite of trunk since Matthieu's fixes for the soundness of polymorphic universes, and I am unsure of the expected semantics. We should reintroduce it later on when we understand better the issue of simply fix it once and for all. | |||
| 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-20 | Proofview.Goal.sigma returns an indexed evarmap. | Pierre-Marie Pédrot | |
| 2015-10-20 | Indexing Proofview.goals with a stage. | Pierre-Marie Pédrot | |
| This is not perfect though, some primitives are unsound, and some higher-order API should use polymorphic functions so as not to depend on a given level. | |||
| 2015-10-20 | Boxing the Goal.enter primitive into a record type. | Pierre-Marie Pédrot | |
| 2015-10-20 | Renaming Goal.enter field into s_enter. | Pierre-Marie Pédrot | |
| 2015-10-19 | Expliciting the uses of the old Tacmach API in Tactics. | Pierre-Marie Pédrot | |
| 2015-10-19 | Removing some unsafe uses of monotonicity. | Pierre-Marie Pédrot | |
| 2015-10-19 | Do occur-check w.r.t existential's types also when instantiating an evar. | Matthieu Sozeau | |
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-19 | Type delayed_open_constr is now monotonic. | Pierre-Marie Pédrot | |
| 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 | More monotonicity in Tactics. | Pierre-Marie Pédrot | |
| 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 | Removing tclEVARS in various places. | Pierre-Marie Pédrot | |
| 2015-10-19 | Reducing the uses of tclEVARS in Tactics by using monotonous functions. | Pierre-Marie Pédrot | |
| 2015-10-19 | Adding a monotonic variant of Goal.enter and Goal.nf_enter. | Pierre-Marie Pédrot | |
| 2015-10-19 | Function debug mode more formatted. | Pierre Courtieu | |
| 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 | Making Evarutil.new_evar monotonous. | Pierre-Marie Pédrot | |
| 2015-10-18 | Constraining refine to monotonic functions. | 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). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |