aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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
2010-10-06Extraction: allow to use Extraction Inline / NoInline even from under a section.letouzey
2010-10-06Remove unused unshare_proof_tree from xml pluginglondu
2010-10-06Remove open_subgoals field of proof_treeglondu
2010-10-05Auto-inlining of f_terminate in Functionjforest
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-28Fix bug #2321, allowing "_" named projections in classes. Not realizingmsozeau
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
2010-09-24Dead code in extractionletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-21Report fix bug 2345 from v8.3 (Bad error message when functionalcourtieu
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-09-20Extraction: re-introduce some eta-expansions in rare situations leading to '_...letouzey
2010-09-19Reverting partial fix for #2335 committed by mistake in r13435. Sorry.herbelin
2010-09-19Patch solving the bug but leaving open design choicesherbelin
2010-09-17Extraction: multiple fixes related with the Not_found encountered by X. Leroyletouzey
2010-09-15Fix likely semantic typosglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 09:43:16 +0000