aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-03-08syntax for exponentspottier
2011-03-08adding eta in the vmbgregoir
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Revert commit r13883: instantiating ?n by a lambda when "?n a" has toherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-03-07CHANGES: mentionning quickly Separate Extractionletouzey
2011-03-07Extraction: a warning when an opaque constant is enterredletouzey
2011-03-07Extraction: fix printing of haskell modular namesletouzey
2011-03-07Extraction: avoid printing unused mutual fix components (fix #2477)letouzey
2011-03-07A new command "Separate Extraction"letouzey
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2011-03-05Moving printing of module typing errors upwards to himsg.ml so as toherbelin
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
2011-03-05A few more betaiota on environments and types of error messages. Seems toherbelin
2011-03-05Added support for instantiation of ?n by a lambda when "?n a" has toherbelin
2011-03-05Reorganized a bit evarconv.ml:herbelin
2011-03-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
2011-03-05Instantiate evar by a lambda when "?n args" has to unify with Prodherbelin
2011-03-05Fixed a "feature" about subtyping records: one was expected not onlyherbelin
2011-03-05Restore documentation of library String which was removed in 2007 (r10049)herbelin
2011-03-05Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notationherbelin
2011-03-05Fixing injection bug #2493 (regression introduced by fixing injectionherbelin
2011-03-04CHANGES: update of syntax for annotations of functor applicationletouzey
2011-03-04Extraction: improved indentation of extracted code (fix #2497)letouzey
2011-03-04Simplify proofs in Permutation using generalized rewriting.msozeau
2011-03-04- Allow to set a particular transparent_state for the local hintmsozeau
2011-03-04checker: cleanupglondu
2011-03-04checker: add eta-expansionglondu
2011-03-03Propagate recent kernel changes to the checkerletouzey
2011-02-28- Allow rewriting under abitrary products, not just those in Prop.msozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:13:43 +0000