aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-01-11In univ.ml, put universe_level primitives in its their own sub-moduleglondu
2011-01-11Add [Typeclasses Debug] option that respects backtracking, solvemsozeau
2011-01-11Add "Print Sorted Universes"glondu
2011-01-11Use dashed lines for equivalence edges in dot output of universesglondu
2011-01-11More coherent comment orderingglondu
2011-01-11Fix some typosglondu
2011-01-11ratrapage exception, deja fait ...bgregoir
2011-01-07Fixing an uncaught exception bug with use of vmcastherbelin
2011-01-07MacOS integrationpboutill
2011-01-07Separate load_file handler in coqidepboutill
2011-01-07Coqide is not built with coqmktop any morepboutill
2011-01-07Don't install both coqide.byte and coqide.optpboutill
2011-01-07Call coqtop with -nois when probing for filespboutill
2011-01-07Fix print in coqidepboutill
2011-01-07mli comments for docpboutill
2011-01-07Update CHANGESpboutill
2011-01-07Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)letouzey
2011-01-06Remove fake alpha-specific case in configureglondu
2011-01-06s/appartness/membership/g (Closes: #2470)glondu
2011-01-06Reverted r13715 "Add improved indenters that rely on the current proof state ...gmelquio
2011-01-06Remove Safe_marshalglondu
2011-01-04Ndigits: a Pshiftl_nat used in BigN (was double_digits there)letouzey
2011-01-04f_equiv : a clone of f_equal that handles setoid equivalencesletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 14:37:28 +0000