aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* Add "case as/in/using" and temporary "destruct" with n args.Gravatar herbelin2009-09-20
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Addition of "Reserved Infix" continued.Gravatar herbelin2009-09-14
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* Postpone checking of Local/Global to allow grammar extensions to use itGravatar msozeau2009-09-02
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-28 07:22:55 +0000