aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Refine API using EConstr.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Coercion API using EConstr.Pierre-Marie Pédrot
2017-02-14Classops API using EConstr.Pierre-Marie Pédrot
2017-02-14Typeclasses API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacred API using EConstr.Pierre-Marie Pédrot
2017-02-14Constr_matching API using EConstr.Pierre-Marie Pédrot
2017-02-14Typing API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarsolve API using EConstr.Pierre-Marie Pédrot
2017-02-14Evardefine API using EConstr.Pierre-Marie Pédrot
2017-02-14Find_subterm API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-29Removing dead code.Hugo Herbelin
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
2016-10-28Merge remote-tracking branch 'github/pr/337' into v8.6Maxime Dénès
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-22Fix a bug in error printing of unif constraintsMatthieu Sozeau
2016-10-20[search] Don't build intermediate lists in search.Emilio Jesus Gallego Arias
2016-10-18[pp] Add tagging function to all low-level printing calls.Emilio Jesus Gallego Arias
2016-10-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-17[toplevel] Remove undocumented "just_parsing" flag.Emilio Jesus Gallego Arias
2016-10-17[toplevel] Remove duplicate beautify flags.Emilio Jesus Gallego Arias
2016-10-17Vernac.ml: inlining read_vernac_file within load_vernac.Hugo Herbelin
2016-10-17Grouping checks about commands together.Hugo Herbelin
2016-10-17Vernac.ml: parenthesizing a side-effect.Hugo Herbelin
2016-10-17Factorizing two instances of load_vernac.Hugo Herbelin
2016-10-17Passing chan_beautify functionally rather than by side-effect.Hugo Herbelin
2016-10-17Applying Emilio's suggestion to simplify type of eval_expr.Hugo Herbelin
2016-10-17More on making the lexer more functional (continuing b8ae2de5 andHugo Herbelin
2016-10-17Removing export of location_table outside of cLexer.Hugo Herbelin
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-16Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".Pierre-Marie Pédrot
2016-10-12Merge PR #224 into v8.6Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-10Fixing #5133 (error reporting delayed).Hugo Herbelin
2016-10-09A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).Hugo Herbelin
2016-10-09Moving Pp.comments to CLexer so that Pp is purer (no more side-effectHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 00:32:14 +0000