| Age | Commit message (Expand) | Author |
|---|
| 2011-02-17 | In Program obligation, do not use auto on non-proposition goals by | msozeau |
| 2011-02-17 | - Use transparency information all the way through unification and | msozeau |
| 2011-02-16 | Fix compilation issues. | msozeau |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2011-02-12 | fix last commit about modules (subst_cl_typ may raise Not_found) | letouzey |
| 2011-02-11 | An automatic substitution of scope at functor application | letouzey |
| 2011-02-11 | Annotations at functor applications: | letouzey |
| 2011-02-11 | Mod_typing: some refactoring (common parts about MSEapply and co) | letouzey |
| 2011-02-11 | Safe_typing: some refactoring (avoiding copy-paste of record definitions) | letouzey |
| 2011-02-11 | Mod_subt: some more refactoring, substitution is also separated in two tables | letouzey |
| 2011-02-11 | Mod_subst: split delta_resolver in two tables (mp / kn) | letouzey |
| 2011-02-11 | Update changelogs | glondu |
| 2011-02-11 | In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809) | letouzey |
| 2011-02-11 | Try to clarify a bit Class_tactics (comments, refactoring,...) | letouzey |
| 2011-02-11 | An generic imperative union-find, used for deps of evars in Class_tactics | letouzey |
| 2011-02-11 | Change Evd.fold to a faster version that simply removes unneeded evars. | msozeau |
| 2011-02-11 | compatibility <3.12 (Map.exists Map.singleton) | pboutill |
| 2011-02-10 | Remove obsolete TheoryList | glondu |
| 2011-02-10 | Vectors fully use implicit arguments | pboutill |
| 2011-02-10 | Fixpoints are traverse during implicits arguments search to toplevel | pboutill |
| 2011-02-10 | Interp a definition with the implicit arguments of its local context | pboutill |
| 2011-02-10 | local variables can have implicits locally | pboutill |
| 2011-02-10 | Data structure telling implicits of local variables is a map in the | pboutill |
| 2011-02-10 | internalize now use a record for its env | pboutill |
| 2011-02-10 | MacOS compatibility | pboutill |
| 2011-02-10 | More comments and less doublons in some mli | pboutill |
| 2011-02-10 | - proper printing of setoid_rewrite tactic applications | msozeau |
| 2011-02-10 | Rename subst_raw_with_bindings to subst_glob_with_bindings and export | msozeau |
| 2011-02-10 | Started to fix the declarative proof mode (C-zar). | aspiwack |
| 2011-02-09 | One more fix for setoid_rewrite: completely reinterpret the given lemmas | msozeau |
| 2011-02-08 | Correct handling of existential variables when multiple different | msozeau |
| 2011-02-07 | Factorize code of rewrite to make way for a new implementation using the | msozeau |
| 2011-02-03 | Dp: another fix suggested by Virgile Prevosto | letouzey |
| 2011-02-03 | Repair Class_tactics.split_evars, broken by r13717 (should fix #2481) | letouzey |
| 2011-01-31 | Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar" | letouzey |
| 2011-01-31 | A fine-grain control of inlining at functor application via priority levels | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2011-01-27 | test-suite/Makefile: add a rule to build all_stdlib.v (for the bench) | glondu |
| 2011-01-27 | Make simpl use the proper constant when folding (mutual) fixpoints | letouzey |
| 2011-01-25 | Fix compilation with camlp5 (Closes: #2487) | glondu |
| 2011-01-25 | Update .gitignore | glondu |
| 2011-01-25 | Add a test for sorting all universes of stdlib | glondu |
| 2011-01-25 | Rewrite sort_universes to minimize the number of universes | glondu |
| 2011-01-20 | Numbers: simplier spec for testbit | letouzey |
| 2011-01-12 | Fix formatting issue in refman | glondu |
| 2011-01-11 | Fix ocamlbuild-based build system | glondu |
| 2011-01-11 | Remove references to -ide option of coqmktop | glondu |
| 2011-01-11 | In univ.ml, put universe_level primitives in its their own sub-module | glondu |
| 2011-01-11 | Add [Typeclasses Debug] option that respects backtracking, solve | msozeau |
| 2011-01-11 | Add "Print Sorted Universes" | glondu |
