aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-07-21Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).herbelin
2010-07-21Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofherbelin
2010-07-20Fixed a bug in list_forall2eq (wrong exception was caught).herbelin
2010-07-18Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).herbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-07-16Amelioration dans Functionjforest
2010-07-16fixed (serious) bug #2353: non-recursive parameters of nested inductive types...barras
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 17:29:58 +0000