aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Added profile.cmo in grammar.cma so that any functions in one of theGravatar herbelin2009-08-14
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Added "etransitivity".Gravatar herbelin2009-08-03
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* Miscellaneous practical commits: Gravatar herbelin2009-06-29
* Allow anonymous instances again, with syntax [Instance: T] where TGravatar msozeau2009-06-15
* Simplifying the call to print_no_goals and not calling it when no goalGravatar herbelin2009-06-11
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* Ensure the precondition of the partial function [list_chop] holdsGravatar msozeau2009-06-03
* Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonctionGravatar aspiwack2009-05-28
* Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dansGravatar aspiwack2009-05-27
* =?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...Gravatar aspiwack2009-05-27
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* - Fixed a little bug in previous commit (bad failure in case of unknown entry).Gravatar herbelin2009-04-27
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
* Avoid inadvertent declaration of "on" as a keyword. New syntax isGravatar msozeau2009-03-29
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Parsing files for numerals (+ ascii/string) moved into pluginsGravatar letouzey2009-03-27
* Remove unused mli filesGravatar letouzey2009-03-27
* - Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"Gravatar herbelin2009-03-23
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* Optionally list opaque constants in addition to axions/variables inGravatar msozeau2009-03-09
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Do not reserve the keyword "Infer".Gravatar puech2009-02-03
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
* Last changes in type class syntax: Gravatar msozeau2009-01-18
* DISCLAIMERGravatar puech2009-01-17
* Fixing #1960 (xml bug with external on goal variable) and #1961Gravatar herbelin2009-01-14
* Fixing/improving management of uniform prefix Local and GlobalGravatar herbelin2009-01-14
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
* Fixing a cosmetic tactic printer bug in passingGravatar herbelin2009-01-07
* - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",Gravatar herbelin2009-01-02
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* About "apply in":Gravatar herbelin2008-12-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 01:28:41 +0000