aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* Fixing previous commit (something strange happened...)Gravatar ppedrot2012-06-04
* Replacing some str with strbrkGravatar ppedrot2012-06-04
* Added a color output to Coqtop.Gravatar ppedrot2012-06-04
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Restore compatibility with camlp4 (some missing open Tok)Gravatar letouzey2012-05-30
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
* Extend become a mli-only file in intf/Gravatar letouzey2012-05-29
* Avoid Dumpglob dependency on LexerGravatar letouzey2012-05-29
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* Split Egrammar into Egramml and EgramcoqGravatar letouzey2012-05-29
* No more Univ in grammar.cmaGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Strongly reduce the dependencies of grammar.cma, modulo two hacksGravatar letouzey2012-05-29
* Basic stuff about constr_expr migrated from topconstr to constrexpr_opsGravatar letouzey2012-05-29
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29
* slim down a bit genarg.ml (pr_intro_pattern forgotten there)Gravatar letouzey2012-05-29
* Migrate the grammar entry about "Ltac" into g_vernac.ml4.Gravatar letouzey2012-05-29
* simplification in deps of some g_*.ml4Gravatar letouzey2012-05-29
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
* Tactic unfold always asks for comma between names.Gravatar pboutill2012-05-09
* Partial revert of r15148 in order to compile with Camlp4Gravatar pboutill2012-04-27
* migrate g_obligations.ml4 in parsingGravatar letouzey2012-04-26
* Program: avoid staying in program mode after a failed Program commandGravatar letouzey2012-04-26
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
* Corrects a (very) longstanding bug of tactics. As is were, tactic expectingGravatar aspiwack2012-04-18
* Removed syntax BeginSubproof/EndSubproof. It has been replaced byGravatar aspiwack2012-04-13
* Remove print call that do not use the pp mechanismGravatar pboutill2012-04-12
* "A -> B" is a notation for "forall _ : A, B".Gravatar pboutill2012-04-12
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
* Typo in a message.Gravatar aspiwack2012-03-30
* Added a command "Unfocused" which returns an error when the proof isGravatar aspiwack2012-03-30
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
* Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclGravatar letouzey2012-03-30
* Slight change in the semantics of arguments scopes: scopes can noGravatar herbelin2012-03-26
* Remove undocumented command "Delete foo"Gravatar letouzey2012-03-23
* Remove old proof-managment commands Suspend/ResumeGravatar letouzey2012-03-23
* Ppvernac: nicer printing of proof delimiters { ... }Gravatar letouzey2012-03-21
* Fixing bug #2724 (using notations with binders in cases patternsGravatar herbelin2012-03-20
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicGravatar herbelin2012-03-20
* Hopefully complying with camlp5 < 6.00 syntaxGravatar herbelin2012-03-19