aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2011-03-08syntax for exponentspottier
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
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-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
2011-03-04Extraction: improved indentation of extracted code (fix #2497)letouzey
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-25Revert "syntax for exponents"glondu
2011-02-22syntax for exponentspottier
2011-02-22anneaux commutatifs ou non, reification sans mlpottier
2011-02-10Interp a definition with the implicit arguments of its local contextpboutill
2011-02-10Data structure telling implicits of local variables is a map in thepboutill
2011-02-10Started to fix the declarative proof mode (C-zar).aspiwack
2011-02-03Dp: another fix suggested by Virgile Prevostoletouzey
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-07Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)letouzey
2010-12-25ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDglondu
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
2010-12-24s/raw/glob/g in decl_interp.ml for more consistencyglondu
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-24Rename files in funind to respect new conventionsglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-23Prepare change of nomenclature rawconstr -> glob_constrglondu
2010-12-21Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)letouzey
2010-12-13Remove an unused function with a Evd.fold in subtacletouzey
2010-11-25Dp: minor fix suggested by Virgile Prevostoletouzey
2010-11-18Some more revision of {P,N,Z}Arith + bitwise ops in Ndigitsletouzey
2010-11-16Use full path for unknown stuff in omegaglondu
2010-11-10Integer division: quot and rem (trunc convention) in addition to div and modletouzey
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-11-07Add information of localisation when an error involving an "implicitherbelin
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
2010-10-31An experimental support for open constrs in hints and in "using"herbelin
2010-10-31Cleaning the use of parentheses around evd and evdref (cosmetic commit).herbelin
2010-10-21Solve name conflict about pow introduced by commit 13546.letouzey
2010-10-21Still some more Cpow in Type rather than Set (cf. r13542)letouzey
2010-10-14Reparation du parseur/printer de nombres BigNletouzey
2010-10-14Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)letouzey
2010-10-12Fix bug #2393: allow let-ins inside telescopes (only fails when there'smsozeau
2010-10-07Fix bug# 2392msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 03:20:55 +0000