| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-28 | Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins" | Hugo Herbelin | |
| After all, let's target 8.6. | |||
| 2015-10-26 | Documenting a bit more interpretation functions in passing. | Hugo Herbelin | |
| 2015-10-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-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 | More monotonicity in Tactics. | Pierre-Marie Pédrot | |
| 2015-10-18 | Making Evarutil.new_evar monotonous. | Pierre-Marie Pédrot | |
| 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 | 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-16 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 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 | 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-14 | Occur-check in evar_define was not strong enough. | Matthieu Sozeau | |
| 2015-10-14 | Fix constr_matching when a match is found in the head of a case construct | Matthieu Sozeau | |
| 2015-10-14 | Fixing evarmap implementation. | Pierre-Marie Pédrot | |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-12 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-12 | Fix rechecking of applications: it can be given ill-typed terms. Fixes ↵ | Matthieu Sozeau | |
| math-classes. | |||
| 2015-10-11 | Fixing untimely unexpected warning "Collision between bound variables" (#4317). | Hugo Herbelin | |
| Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables. | |||
| 2015-10-11 | Refining 0c320e79ba30 in fixing interpretation of constr under binders | Hugo Herbelin | |
| which was broken after it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). Interpretation was corrected, but error message was damaged. | |||
| 2015-10-11 | Fixing obviously untested fold_glob_constr and iter_glob_constr. | Hugo Herbelin | |
| 2015-10-11 | Constr_matching: renaming misleading name stk into ctx. | Hugo Herbelin | |
| 2015-10-10 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-09 | Code cleaning in VM (with Benjamin). | Maxime Dénès | |
| Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values. | |||
| 2015-10-09 | Fix inference of return clause raising a type error. | Matthieu Sozeau | |
| 2015-10-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-08 | Univs: fix bug #3807 | Matthieu Sozeau | |
| Add a flag to disallow minimization to set | |||
| 2015-10-08 | Univs: fix bug #4161. | Matthieu Sozeau | |
| Retypecheck abstracted infered predicate to register the right universe constraints. | |||
| 2015-10-07 | Univs: fix FingerTree contrib. | Matthieu Sozeau | |
| Let merge_context_set be lenient when merging the context of side effects of an entry from solve_by_tac. | |||
| 2015-10-07 | Univs: add Strict Universe Declaration option (on by default) | Matthieu Sozeau | |
| This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option. | |||
| 2015-10-06 | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot | |
| 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. | |||
| 2015-10-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-06 | Univs (pretyping): call vm_compute/native_compute with the current | Matthieu Sozeau | |
| universe graph | |||
| 2015-10-06 | Fix bug #4354: interpret hints in the right env and sigma. | Matthieu Sozeau | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Univs: fix bug #4251, handling of template polymorphic constants. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix after rebase (from_ctx/from_env) | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau | |
| 2015-10-02 | Univs (pretyping): allow parsing and decl of Top.n | Matthieu Sozeau | |
| This allows pretyping and detyping to be inverses regarding universes, and makes Function's detyping/pretyping manipulations bearable in presence of global universes that must be declared (otherwise an evd would need to be threaded there in many places as well). | |||
| 2015-10-02 | Univs (evd): deal with global universes and sideff | Matthieu Sozeau | |
| - Fix union of universe contexts to keep declarations - Fix side-effect handling to register new global universes in the graph. | |||
| 2015-10-02 | Forcing i > Set for global universes (incomplete) | Matthieu Sozeau | |
| 2015-10-02 | Univs: force all universes to be >= Set. | Matthieu Sozeau | |
| 2015-10-02 | Univs: Fix part of bug #4161 | Matthieu Sozeau | |
| Rechecking applications built by evarconv's imitation. | |||
| 2015-10-02 | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau | |
| 2015-09-27 | Removing subst_defined_metas_evars from Evd. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |