aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-02-28Add a flag to hide obligations in Program-generated terms under anmsozeau
2011-02-25Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)letouzey
2011-02-25Fix indentation of default pattern in haskell case (bug #2476)letouzey
2011-02-25Filter out admitted subgoals from search resultsglondu
2011-02-25Ocamlbuild needs OCAML_LD_LIBRARY_PATH (bug #2502)glondu
2011-02-25Revert "syntax for exponents"glondu
2011-02-24Mod_subst: improving sharing of subst_mpsletouzey
2011-02-23Some more simplification in Mod_substletouzey
2011-02-23BigQ : setting correct arguments scopesletouzey
2011-02-22Try to fix the behavior of clenv_missing used when declaring hintsletouzey
2011-02-22syntax for exponentspottier
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 09:09:04 +0000