aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-09-13commit 13400 and 13409.soubiran
2010-09-02fixed bug #2375 (congruence)corbinea
2010-08-02Fix [clenv_missing] to compute a better approximation of missingmsozeau
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
2010-07-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...pottier
2010-07-27nstaz pour les anneaux integres et les setoides, R Z et Qpottier
2010-07-27Minor fixes:msozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-23correcting a bug in funind introduced in r 13292jforest
2010-07-22Extension of the recursive notations mechanismherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 09:35:27 +0000