aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-02-22anneaux commutatifs ou non, reification sans mlpottier
2011-02-21Some fixes of the test-suite scriptsletouzey
2011-02-21Fix test-suite script.msozeau
2011-02-17In Program obligation, do not use auto on non-proposition goals bymsozeau
2011-02-17- Use transparency information all the way through unification andmsozeau
2011-02-16Fix compilation issues.msozeau
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
2011-02-12fix last commit about modules (subst_cl_typ may raise Not_found)letouzey
2011-02-11An automatic substitution of scope at functor applicationletouzey
2011-02-11Annotations at functor applications:letouzey
2011-02-11Mod_typing: some refactoring (common parts about MSEapply and co)letouzey
2011-02-11Safe_typing: some refactoring (avoiding copy-paste of record definitions)letouzey
2011-02-11Mod_subt: some more refactoring, substitution is also separated in two tablesletouzey
2011-02-11Mod_subst: split delta_resolver in two tables (mp / kn)letouzey
2011-02-11Update changelogsglondu
2011-02-11In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809)letouzey
2011-02-11Try to clarify a bit Class_tactics (comments, refactoring,...)letouzey
2011-02-11An generic imperative union-find, used for deps of evars in Class_tacticsletouzey
2011-02-11Change Evd.fold to a faster version that simply removes unneeded evars.msozeau
2011-02-11compatibility <3.12 (Map.exists Map.singleton)pboutill
2011-02-10Remove obsolete TheoryListglondu
2011-02-10Vectors fully use implicit argumentspboutill
2011-02-10Fixpoints are traverse during implicits arguments search to toplevelpboutill
2011-02-10Interp a definition with the implicit arguments of its local contextpboutill
2011-02-10local variables can have implicits locallypboutill
2011-02-10Data structure telling implicits of local variables is a map in thepboutill
2011-02-10internalize now use a record for its envpboutill
2011-02-10MacOS compatibilitypboutill
2011-02-10More comments and less doublons in some mlipboutill
2011-02-10- proper printing of setoid_rewrite tactic applicationsmsozeau
2011-02-10Rename subst_raw_with_bindings to subst_glob_with_bindings and exportmsozeau
2011-02-10Started to fix the declarative proof mode (C-zar).aspiwack
2011-02-09One more fix for setoid_rewrite: completely reinterpret the given lemmasmsozeau
2011-02-08Correct handling of existential variables when multiple differentmsozeau
2011-02-07Factorize code of rewrite to make way for a new implementation using themsozeau
2011-02-03Dp: another fix suggested by Virgile Prevostoletouzey
2011-02-03Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)letouzey
2011-01-31Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"letouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2011-01-27test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)glondu
2011-01-27Make simpl use the proper constant when folding (mutual) fixpointsletouzey
2011-01-25Fix compilation with camlp5 (Closes: #2487)glondu
2011-01-25Update .gitignoreglondu
2011-01-25Add a test for sorting all universes of stdlibglondu
2011-01-25Rewrite sort_universes to minimize the number of universesglondu
2011-01-20Numbers: simplier spec for testbitletouzey
2011-01-12Fix formatting issue in refmanglondu
2011-01-11Fix ocamlbuild-based build systemglondu
2011-01-11Remove references to -ide option of coqmktopglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-11 06:50:23 +0000