| Age | Commit message (Expand) | Author |
|---|
| 2011-02-28 | - Allow rewriting under abitrary products, not just those in Prop. | msozeau |
| 2011-02-28 | Add a flag to hide obligations in Program-generated terms under an | msozeau |
| 2011-02-25 | Extraction: Add missing parenthesis around emulated pattern-match (fix #2478) | letouzey |
| 2011-02-25 | Fix indentation of default pattern in haskell case (bug #2476) | letouzey |
| 2011-02-25 | Filter out admitted subgoals from search results | glondu |
| 2011-02-25 | Ocamlbuild needs OCAML_LD_LIBRARY_PATH (bug #2502) | glondu |
| 2011-02-25 | Revert "syntax for exponents" | glondu |
| 2011-02-24 | Mod_subst: improving sharing of subst_mps | letouzey |
| 2011-02-23 | Some more simplification in Mod_subst | letouzey |
| 2011-02-23 | BigQ : setting correct arguments scopes | letouzey |
| 2011-02-22 | Try to fix the behavior of clenv_missing used when declaring hints | letouzey |
| 2011-02-22 | syntax for exponents | pottier |
| 2011-02-22 | anneaux commutatifs ou non, reification sans ml | pottier |
| 2011-02-21 | Some fixes of the test-suite scripts | letouzey |
| 2011-02-21 | Fix test-suite script. | msozeau |
| 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 |
