aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2009-09-02Postpone checking of Local/Global to allow grammar extensions to use itmsozeau
2009-08-14Ajout de la gestion de Local et Global pour les options (au sens deaspiwack
2009-08-14Added profile.cmo in grammar.cma so that any functions in one of theherbelin
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-11Add support for "Infix ... := constr" instead of just "Infix ... := ref".herbelin
2009-08-07Fixed incorrect optimization in Prettyp.pr_located_qualid introducedherbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-03Added "etransitivity".herbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-07-15- Granted wish #2138 (support for local binders in syntax of Record fields).herbelin
2009-06-29Miscellaneous practical commits: herbelin
2009-06-15Allow anonymous instances again, with syntax [Instance: T] where Tmsozeau
2009-06-11Simplifying the call to print_no_goals and not calling it when no goalherbelin
2009-06-07- Added two new introduction patterns with the following temptative syntaxes:herbelin
2009-06-06Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0herbelin
2009-06-03Ensure the precondition of the partial function [list_chop] holdsmsozeau
2009-05-28Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonctionaspiwack
2009-05-27Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dansaspiwack
2009-05-27=?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...aspiwack
2009-05-20- Fixing declarative mode in presence of high use of Change_evars nodesherbelin
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-04-27- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-04-08Some dead code removal + cleanupsletouzey
2009-04-08- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingherbelin
2009-03-29Avoid inadvertent declaration of "on" as a keyword. New syntax ismsozeau
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
2009-03-27Remove unused mli filesletouzey
2009-03-23- Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"herbelin
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-03-16Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"herbelin
2009-03-09Optionally list opaque constants in addition to axions/variables inmsozeau
2009-03-04commande Timeout + compaction des traces de debug_tacticbarras
2009-02-03Do not reserve the keyword "Infer".puech
2009-01-19Les records déclarés avec Record ne peuvent plus être récursifs (le aspiwack
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2009-01-18Getting rid of the previous implementation of setoid_rewrite which wasmsozeau
2009-01-18Last changes in type class syntax: msozeau
2009-01-17DISCLAIMERpuech
2009-01-14Fixing #1960 (xml bug with external on goal variable) and #1961herbelin
2009-01-14Fixing/improving management of uniform prefix Local and Globalherbelin
2009-01-13- Standardized prefix use of "Local"/"Global" modifiers as decided inherbelin
2009-01-07Fixing a cosmetic tactic printer bug in passingherbelin
2009-01-02- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",herbelin
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 16:55:14 +0000