aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | Expliciting some uses of Compat module.Gravatar Pierre-Marie Pédrot2015-10-21
| |
| * Bug #3956 is fixed.Gravatar Matthieu Sozeau2015-10-21
| |
* | Removing test for bug #3956.Gravatar Pierre-Marie Pédrot2015-10-21
| | | | | | | | | | | | | | 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.
| * Fixed (and changed) infoH.Gravatar Pierre Courtieu2015-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Fix lemma-overloadingGravatar Matthieu Sozeau2015-10-20
| | | | | | | | | | | | 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.
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
| |
* | Indexing Proofview.goals with a stage.Gravatar Pierre-Marie Pédrot2015-10-20
| | | | | | | | | | | | 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.
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
| |
* | Renaming Goal.enter field into s_enter.Gravatar Pierre-Marie Pédrot2015-10-20
| |
* | Expliciting the uses of the old Tacmach API in Tactics.Gravatar Pierre-Marie Pédrot2015-10-19
| |
* | Removing some unsafe uses of monotonicity.Gravatar Pierre-Marie Pédrot2015-10-19
| |
| * Do occur-check w.r.t existential's types also when instantiating an evar.Gravatar Matthieu Sozeau2015-10-19
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
* | Type delayed_open_constr is now monotonic.Gravatar Pierre-Marie Pédrot2015-10-19
| |
| * Categorizing debug messages as such + NonLogical uses loggers.Gravatar Pierre Courtieu2015-10-19
| |
| * Test for #4372 (anomaly in inversion in the presence of fake dependency).Gravatar Hugo Herbelin2015-10-19
| |
* | More monotonicity in Tactics.Gravatar Pierre-Marie Pédrot2015-10-19
| |
| * Turning anomaly into error for #4372 (weakness of inversion in theGravatar Hugo Herbelin2015-10-19
| | | | | | | | | | | | presence of dependent types with only superficial dependency). See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372.
* | Removing tclEVARS in various places.Gravatar Pierre-Marie Pédrot2015-10-19
| |
* | Reducing the uses of tclEVARS in Tactics by using monotonous functions.Gravatar Pierre-Marie Pédrot2015-10-19
| |
* | Adding a monotonic variant of Goal.enter and Goal.nf_enter.Gravatar Pierre-Marie Pédrot2015-10-19
| |
* | Function debug mode more formatted.Gravatar Pierre Courtieu2015-10-19
| |
| * Partly fixes #3225. Removed some old experimental stuff in funind.Gravatar Pierre Courtieu2015-10-19
| |
| * Fixed #4274, bad formatting of messages in emacs mode.Gravatar Pierre Courtieu2015-10-19
| |
| * Documenting the option "Strict Universe Declaration" in CHANGES.Gravatar Pierre-Marie Pédrot2015-10-19
| |
* | Making Evarutil.new_evar monotonous.Gravatar Pierre-Marie Pédrot2015-10-18
| |
* | Constraining refine to monotonic functions.Gravatar Pierre-Marie Pédrot2015-10-18
| |
| * Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
| |
| * Using "__" rather than this unelegant arbitrary "A" for the name of ↵Gravatar Hugo Herbelin2015-10-18
| | | | | | | | variables of the context of an evar in debugging mode.
| * Reference Manual: Applying standard style recommendation about notGravatar Hugo Herbelin2015-10-18
| | | | | | | | starting a sentence with a symbolic expression.
| * Fixing #4198 (continued): not matching within the inner lambdas/let-insGravatar Hugo Herbelin2015-10-18
| | | | | | | | | | | | | | 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).
| * Using appropriate lambda decomposition function counting let-ins whenGravatar Hugo Herbelin2015-10-18
| | | | | | | | | | | | | | | | 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).
| * Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Gravatar Hugo Herbelin2015-10-18
| | | | | | | | | | | | | | 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?
* | Adding a notion of monotonous evarmap.Gravatar Pierre-Marie Pédrot2015-10-18
| |
* | Clarifying and documenting the UState API.Gravatar Pierre-Marie Pédrot2015-10-17
| |
* | Dedicated file for universe unification context manipulation.Gravatar Pierre-Marie Pédrot2015-10-17
| | | | | | | | | | | | | | 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.
| * Lemmas accept the Local flag.Gravatar Pierre-Marie Pédrot2015-10-17
| | | | | | | | This was a trivial overlook.
| * Test for bug #4325.Gravatar Pierre-Marie Pédrot2015-10-17
| |
| * Generalize fix for auto from PMP to eauto and typeclasses eauto.Gravatar Matthieu Sozeau2015-10-16
| |
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-10-16
|\|
* | Hashcons bytecode generated by the VM.Gravatar Pierre-Marie Pédrot2015-10-16
| |
* | Exporting a purely functional interface to bytecode patching.Gravatar Pierre-Marie Pédrot2015-10-16
| |
| * Remove left2right reference from the kernel.Gravatar Maxime Dénès2015-10-16
| | | | | | | | | | | | | | | | Was introduced by seemingly unrelated commit fd62149f9bf40b3f309ebbfd7497ef7c185436d5. The currently policy is to avoid exposing global references in the kernel interface when easily doable.
| * Merge hint lists instead of appending them. (Fix bug #3199)Gravatar Guillaume Melquiond2015-10-16
| |
| * Avoid dependency of the pretyper on C code.Gravatar Maxime Dénès2015-10-15
| | | | | | | | | | | | | | | | | | 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.
| * Test file for #4346: Set is no longer of type TypeGravatar Maxime Dénès2015-10-15
| |
| * Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
| |
| * Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
| |
| * Warn user when bytecode compilation fails.Gravatar Maxime Dénès2015-10-15
| | | | | | | | Previously, the kernel was silently switching back to the standard conversion.
| * Remove now useless exception handler in default conversion.Gravatar Maxime Dénès2015-10-15
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:31:27 +0000