| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-05-12 | Adding the possibility for ML modules to declare functions to be called at | Pierre-Marie Pédrot | |
| caching time, i.e. when the Declare ML Module command is evaluated. This can be used by both static and dynamic plugins. | |||
| 2014-05-12 | Fixing the undocumented -dumpgraphbox option of coqdep. | Pierre-Marie Pédrot | |
| 2014-05-11 | Using Maps to handle imports in Safe_typing. The order is irrelevant indeed, | Pierre-Marie Pédrot | |
| and the lookup operation proved to be costly when dealing with big libraries. | |||
| 2014-05-11 | Eliminating a potentially quadratic behaviour in Require, by using maps | Pierre-Marie Pédrot | |
| instead of lists to test if a library has already been encountered. | |||
| 2014-05-10 | Add appropriate Fail(s) to opened bugs | Jason Gross | |
| The contract is that a file in bugs/opened should not raise errors if the bug is still open. Some of them fail for different reasons than they used to; I'm not sure what to do about these. | |||
| 2014-05-10 | Move opened bugs to bugs/opened | Jason Gross | |
| 2014-05-10 | Add more regression tests for univ poly/prim proj | Jason Gross | |
| hese regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently fails. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one. | |||
| 2014-05-09 | Code cleaning & factorizing functions in Equality. | Pierre-Marie Pédrot | |
| 2014-05-09 | Update and start testing rewrite-in-type code. | Matthieu Sozeau | |
| 2014-05-09 | More documentation of new features in CHANGE. | Pierre-Marie Pédrot | |
| 2014-05-09 | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau | |
| fixing two opened bugs from HoTT/coq. | |||
| 2014-05-09 | Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq ↵ | Matthieu Sozeau | |
| into JasonGross-working-polyproj-tests | |||
| 2014-05-09 | Fix second-order matching to properly check that the predicate found by | Matthieu Sozeau | |
| abstraction has the right type. Fixes bug# 3306. Add test-suite files for bugs 3305 and 3306. | |||
| 2014-05-09 | Restore implicit arguments of irreflexivity (fixes bug #3305). | Matthieu Sozeau | |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau | |
| problem with hashconsing at the same time. This fixes bug# 3302. | |||
| 2014-05-08 | Encapsulating some clausenv uses. This simplifies the control flow of some | Pierre-Marie Pédrot | |
| tactics. | |||
| 2014-05-08 | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic." | Hugo Herbelin | |
| (made push command with wrong local ref; leaving control to Matthieu on new revert) This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a. | |||
| 2014-05-08 | Avoid "revert" to retype-check the goal, and move it to a "new" tactic. | Hugo Herbelin | |
| 2014-05-08 | Typo reference manual | Hugo Herbelin | |
| 2014-05-08 | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin | |
| which compute an abstraction of the goal over a term or a pattern. | |||
| 2014-05-08 | Simplification and improvement of "subst x" in such a way that it | Hugo Herbelin | |
| works in the presence of local definitions referring to x and dependent in other hyps or concl. | |||
| 2014-05-08 | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin | |
| 2014-05-08 | Little reorganization of generalize tactics code w/o semantic changes. | Hugo Herbelin | |
| Also removing trailing spaces. | |||
| 2014-05-08 | Cleanup code in pretyping/evarutil | Matthieu Sozeau | |
| 2014-05-08 | Fix performance problem with unification in presence of universes (bug ↵ | Matthieu Sozeau | |
| #3302) by considering Type i a ground term even when "i" is a flexible universe variable, using the infer_conv function to do the unification of universes. | |||
| 2014-05-08 | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ↵ | Matthieu Sozeau | |
| evar_map in tactics, avoiding useless and potentially costly merge's of constraints. - Implement revert and generalize using the new tactics (not bound to syntax though, as they are not backwards-compatible yet). | |||
| 2014-05-08 | Avoid allocations in type_of_inductive | Matthieu Sozeau | |
| 2014-05-08 | Fast-path equality of sorts in compare_constr* | Matthieu Sozeau | |
| 2014-05-08 | Adapt the checker to polymorphic universes and projections (untested). | Matthieu Sozeau | |
| 2014-05-08 | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot | |
| 2014-05-08 | Fixing test-suite for bug #3043. | Pierre-Marie Pédrot | |
| 2014-05-08 | Fixing output test-suite: since universe polymorphism, the Print command | Pierre-Marie Pédrot | |
| shows the polymorphism status of the term. | |||
| 2014-05-08 | Code cleaning in Tacinterp: factorizing some uses of tclEVARS. | Pierre-Marie Pédrot | |
| 2014-05-07 | Removing comment outdated since eta holds in conversion rule (this | Hugo Herbelin | |
| answers #3299). | |||
| 2014-05-06 | Adding test-suite for bug #3242. | Pierre-Marie Pédrot | |
| 2014-05-06 | Add regression tests for univ. poly. and prim proj | Jason Gross | |
| These regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently passes. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one. | |||
| 2014-05-06 | Remove Lemmas from base_include, it's not linked in dev/printers anymore | Matthieu Sozeau | |
| 2014-05-06 | Cleanup before merge with the trunk | Matthieu Sozeau | |
| 2014-05-06 | Use new tactic combinators in tclABSTRACT, to avoid blowup when using ↵ | Matthieu Sozeau | |
| V82.tactic (tclEVARS _). Again, performance is back to normal. Remove reintroduced try .. with _ -> in raw_enter's. | |||
| 2014-05-06 | Add missing case for primitive projection in fold_map. | Matthieu Sozeau | |
| 2014-05-06 | Fix after merge. | Matthieu Sozeau | |
| 2014-05-06 | Add incompatibilities paragraph in doc about universe polymorphism. | Matthieu Sozeau | |
| 2014-05-06 | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau | |
| in the Evd of proofs (Evd.from_env). - Allow to set the Store.t value of new evars, e.g. to set constraint evars as unresolvable in rewrite.ml. - Fix a HUGE performance problem in the processing of constraints, which was remerging all the previous constraints with the ambient global universes at each new constraint addition. Performance is now back to (or better than) normal. | |||
| 2014-05-06 | Fix extraction taking a type in the wrong environment. | Matthieu Sozeau | |
| Fix restriction of universe contexts to not forget about potentially useful constraints. | |||
| 2014-05-06 | Fix Field_tac to get fast reification again, with the fix on template ↵ | Matthieu Sozeau | |
| universe polymorphic constructors. | |||
| 2014-05-06 | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau | |
| eagerly solve l <= k constraints as k := l when k is a fresh variable coming from a template type. This has the effect of fixing the variable at the first instantiation of the parameters of template polymorphic inductive and avoiding to generate useless <= constraints that need to be minimized afterwards. | |||
| 2014-05-06 | Try a new way of handling template universe levels | Matthieu Sozeau | |
| 2014-05-06 | Print universes in module printing | Matthieu Sozeau | |
| 2014-05-06 | Fix funind w.r.t. universes | Matthieu Sozeau | |
| 2014-05-06 | Fix a pervasive equality use. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |