| Age | Commit message (Expand) | Author |
|---|
| 2011-03-05 | Added support for instantiation of ?n by a lambda when "?n a" has to | herbelin |
| 2011-03-05 | Reorganized a bit evarconv.ml: | herbelin |
| 2011-03-05 | Improved define_evar_as_lambda which was creating an unrelated new evar | herbelin |
| 2011-03-05 | Instantiate evar by a lambda when "?n args" has to unify with Prod | herbelin |
| 2011-03-05 | Fixed a "feature" about subtyping records: one was expected not only | herbelin |
| 2011-03-05 | Restore documentation of library String which was removed in 2007 (r10049) | herbelin |
| 2011-03-05 | Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notation | herbelin |
| 2011-03-05 | Fixing injection bug #2493 (regression introduced by fixing injection | herbelin |
| 2011-03-04 | CHANGES: update of syntax for annotations of functor application | letouzey |
| 2011-03-04 | Extraction: improved indentation of extracted code (fix #2497) | letouzey |
| 2011-03-04 | Simplify proofs in Permutation using generalized rewriting. | msozeau |
| 2011-03-04 | - Allow to set a particular transparent_state for the local hint | msozeau |
| 2011-03-04 | checker: cleanup | glondu |
| 2011-03-04 | checker: add eta-expansion | glondu |
| 2011-03-03 | Propagate recent kernel changes to the checker | letouzey |
| 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 |
