aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-05-17Merge PR#457: Adding an even more compact goal hyps mode.Maxime Dénès
2017-05-16Simplified compaction criterion + tests.Pierre Courtieu
2017-05-05Merge PR#454: Printing unfocussed goals and toward a pg plugin.Maxime Dénès
2017-05-05Adapted to EConstr.Pierre Courtieu
2017-05-04Warning removed.Pierre Courtieu
2017-05-04labelizing argumentsPierre Courtieu
2017-05-04Adding an option "Printing Unfocused".Pierre Courtieu
2017-05-03Adding an even more compact mode for goal display.Pierre Courtieu
2017-05-03Allow flexible anonymous universes in instances and sorts.Gaetan Gilbert
2017-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] [ast] Switch Constrexpr AST to an extensible node type.Emilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Use located in misctypes.Emilio Jesus Gallego Arias
2017-04-24[location] More located use.Emilio Jesus Gallego Arias
2017-04-24[location] Use Loc.located for constr_expr.Emilio Jesus Gallego Arias
2017-04-24[constrexpr] Make patterns use Loc.located for location informationEmilio Jesus Gallego Arias
2017-04-24Merge PR#552: Miscelaneous commitsMaxime Dénès
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-20refactoring "Ppvernac.pr_extend"Matej Kosik
2017-04-12Merge PR#441: Port Toplevel to the Stm APIMaxime Dénès
2017-04-12[flags] Documentation and a minor tweak.Emilio Jesus Gallego Arias
2017-04-09Removing internal support for accepting "{struct x}" and co in "Theorem with".Hugo Herbelin
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-04-03Merge PR#417: No cast surgery in let inMaxime Dénès
2017-04-02Fix higher-order pattern variables not being printed as "@?" (bug #5431).Guillaume Melquiond
2017-03-30Merge PR#511: [stm] Remove some obsolete vernacs/classification.Maxime Dénès
2017-03-27Do so that "About" tells if a reference is a coercion.Hugo Herbelin
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-24Applying same convention as in Definition for printing type in a let in.Hugo Herbelin
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-03-24Unifying standard "constr_level" names for constructors of local_binder_expr.Hugo Herbelin
2017-03-24Renaming local_binder into local_binder_expr.Hugo Herbelin
2017-03-24"Standardizing" the name LocalPatten into LocalRawPattern.Hugo Herbelin
2017-03-21[pp] Move terminal-specific tagging to the toplevel.Emilio Jesus Gallego Arias
2017-03-21[pp] Prepare for serialization, remove opaque glue.Emilio Jesus Gallego Arias
2017-03-21[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Emilio Jesus Gallego Arias
2017-03-21[pp] Remove unused printing tagging infrastructure.Emilio Jesus Gallego Arias
2017-03-15Attempt to improve error message when "apply in" fail.Hugo Herbelin
2017-03-07Fixing Bug 5383 (Hyps Limit) + small refactoring.Pierre Courtieu
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:15:45 +0000