| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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. | |||
| 2015-10-15 | Remove now useless exception handler in default conversion. | Maxime Dénès | |
| 2015-10-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |