aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2012-03-19Hopefully complying with camlp5 < 6.00 syntaxherbelin
2012-03-18Yet another subtlety with bug 2732: when several grammar rules of aherbelin
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02Noise for nothingpboutill
2012-02-29In the syntax of pattern matching, "in" clauses are patterns.pboutill
2012-02-14Arguments supports extra notation scopesgareuselesinge
2012-02-07A "Grab Existential Variables" to transform the unresolved evars at the end o...aspiwack
2012-01-31Fix camlp4 compilationpboutill
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2012-01-23Removed a seemingly unused argument in Require of modules, introduced 10 year...ppedrot
2012-01-23Fixed pretty-printing of Opaque, Transparent and Strategy locality flags.ppedrot
2012-01-20Reverted previous commit, which broke library compilation.ppedrot
2012-01-20This is a quick hack to permit the parsing of the locality flag in the Progra...ppedrot
2012-01-20Fix printing of classesmsozeau
2012-01-19Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.msozeau
2012-01-19Pretty printing of generalized binderpboutill
2012-01-17Fixed the pretty-printing of the Program plugin.ppedrot
2012-01-17Some fix in beautify pretty-printerpboutill
2012-01-16Inductiveops.nb_*{,_env} cleaningpboutill
2012-01-10Fix printing of instances, generalized arguments.msozeau
2011-12-19Fixed some printing details for dependent evars in emacs mode. Patchcourtieu
2011-12-18Applied patches proposed suggested by Hendrik Tews to fix existentialcourtieu
2011-12-18Removing PrintConstr debugging entry in g_proof.ml4 which was notherbelin
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
2011-12-17Improving pretty-printing of Ltac functions.herbelin
2011-12-16Fixing previous commit which was bugging on tactics preceded by goal number (...courtieu
2011-12-16Moving bullets (-, +, *) into stand-alone commands instead of beingcourtieu
2011-12-12Proof using ...gareuselesinge
2011-12-08Makefile: force the installation of all .cmi (and remove some obsolete .mli)letouzey
2011-12-07Fixing grammar resetting bug in the presence of levels initially emptyherbelin
2011-12-06Minor fixes to Argumentsgareuselesinge
2011-12-04Fixing superflous newline in output of About when no parameter is renamed.herbelin
2011-11-30Continuing r14747 being actually incomplete (flushing warnings andherbelin
2011-11-30Preventing Implicit Arguments warning to be shown in non verbose modeherbelin
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-23In emacs mode, prints a list of the dependent existential variables introducedaspiwack
2011-11-21Renamig support added to "Arguments"gareuselesinge
2011-11-21New Arguments vernaculargareuselesinge
2011-11-18Adding the type infrastructure to handle properly API management of optionsppedrot
2011-11-18Fix parsing of :>> and backtrack correctly on the cache of hints for local co...msozeau
2011-11-18Added a printing function to handle single evarsppedrot
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class declarati...msozeau
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-16Fixing beautification of "thm_token" (missing space) + improvements.herbelin
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-10-25Applying Tom Prince's patch to support parametric "constructor n" inherbelin