aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-07-16removed a potentially dangerous try ... with _ -> ...barras
2010-07-16MSetPositive: mention MSetInterface instead of FSetInterfaceletouzey
2010-07-16FSetPositive: sets of positive inspired by FMapPositive.letouzey
2010-07-16Bool: shorter and more systematic proofs + an iff lemma about eqbletouzey
2010-07-16fixed bug #2316 (ring_simplify)barras
2010-07-15Be more clever when trying to find out the relation inmsozeau
2010-07-15Extraction: fix a bit the extraction under modulesletouzey
2010-07-15Ocamlbuild: adapt to last changes for camlp4 (use of tools/compat5*.cmo)letouzey
2010-07-12Fix compilation and test-suite of nsatzglondu
2010-07-12coqide: s/Sys.argv.(0)/Sys.executable_name/ for coqtop (cf #2341)glondu
2010-07-10Bool: iff lemmas about or, a reflect inductive, an is_true functionletouzey
2010-07-09Finish adding out-of-the-box support for camlp4letouzey
2010-07-08Extraction: restrict autoinling to csts whose body is globally visible (fix #...letouzey
2010-07-08Updating reference manual credits: gb is now nsatz.herbelin
2010-07-08Extraction: more factorization of common match branchesletouzey
2010-07-08Extraction: Unset Extraction AutoInline is now the defaultletouzey
2010-07-08nsatz in an integral domain with specialization to Z and Rpottier
2010-07-07Fixed compilation with statically-linked plugins (the decl_modeherbelin
2010-07-07Extraction Library Foo creates Foo.ml, not foo.ml (correct version)letouzey
2010-07-07Extraction Library Foo creates Foo.ml, not foo.mlletouzey
2010-07-07CHANGES: mention last-minute improvements of extractionletouzey
2010-07-07Extraction: get advantage of nicer, algebraic, module typesletouzey
2010-07-07Extraction: some more work on the (re)naming frameworkletouzey
2010-07-07Mod_typing: fix the content of the typ_expr_alg fieldletouzey
2010-07-05Fix goal display when backtrackingvgross
2010-07-05Robustness fix : clean restart of coqtop on pipe error + force matchingvgross
2010-07-05Turned off Mac dynlink hack for 10.6.3+ on x86_64thutchin
2010-07-05Stronger checks on coqtop termination, warning when zombies.vgross
2010-07-05Extraction: (yet another) rework of the renaming codeletouzey
2010-07-05FSets/Msets: some renaming of module params to simplify the task of the extra...letouzey
2010-07-02Fixing tabs closing problems by removing activation infrastructure.vgross
2010-07-02Extraction: better support of modulesletouzey
2010-07-02Extraction: no more MPself hence no need for subst during ppletouzey
2010-07-02Remove dependency to Unix from module Profileglondu
2010-07-02Sorting library: export as hints only lemmas that obviously simplifyherbelin
2010-07-01Miscellaneous small updates:herbelin
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
2010-06-30Fix generalize_eqs tactic to not consider defined variables as being generali...msozeau
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
2010-06-29Correct wrong handling of evars in instance definitions that preventedmsozeau
2010-06-29QArith: typo in name of hint db (fix #2346)letouzey
2010-06-29change the flag "internal" in declare/ind_tables from bool tovsiles
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-28Fix compilation by replacing some "auto with zarith" with "ring"glondu
2010-06-28Extraction: handling modules (not functors) in Haskell by name manglingletouzey
2010-06-28Update of documentation for the standard library (cf. #2332)letouzey
2010-06-28Extraction: remove a useless matchletouzey
2010-06-28Made "replace" accepts open terms on its left-hand-side.herbelin
2010-06-28Fixed a bug introduced in a combination in r12807 and revealed inherbelin
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 20:47:13 +0000