| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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). | |||
| 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-18 | Adding a notion of monotonous evarmap. | Pierre-Marie Pédrot | |
| 2015-10-17 | Clarifying and documenting the UState API. | Pierre-Marie Pédrot | |
| 2015-10-17 | Dedicated file for universe unification context manipulation. | Pierre-Marie Pédrot | |
| This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar. | |||
| 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 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-10-16 | Hashcons bytecode generated by the VM. | Pierre-Marie Pédrot | |
| 2015-10-16 | Exporting a purely functional interface to bytecode patching. | Pierre-Marie Pédrot | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |