aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-05-05More fixes in the Generalized Rewriting chapter.Théo Zimmermann
2018-05-05[sphinx] Replace remaining `@natural` by `@num`.Théo Zimmermann
2018-05-05[sphinx] More use of cmd references in Extraction chapter.Théo Zimmermann
2018-05-05[sphinx] Use references for command Info.Théo Zimmermann
2018-05-05[sphinx] More reference fixes.Théo Zimmermann
2018-05-05[sphinx] Fix a porting mistake.Théo Zimmermann
2018-05-05[sphinx] Use references for Print.Théo Zimmermann
2018-05-05Fix error messages and make them consistent.Théo Zimmermann
2018-05-05Add direct reference to congruence with.Théo Zimmermann
2018-05-05Clean-up around options.Théo Zimmermann
2018-05-05debug trivial and debug auto were not in the tactic index.Théo Zimmermann
2018-05-05Fix failing example in refman.Théo Zimmermann
2018-05-05[sphinx] Fix some references.Théo Zimmermann
2018-05-05[sphinx] Use option direct reference.Théo Zimmermann
2018-05-05[sphinx] Fix a typo that appeared during the migration.Théo Zimmermann
2018-05-05[sphinx] Fix a hardcoded reference.Théo Zimmermann
2018-05-05[sphinx] Backport reformulation.Théo Zimmermann
2018-05-05[sphinx] Backport fix of typo.Théo Zimmermann
2018-05-05Fix typo in Coercions chapter.Théo Zimmermann
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-05-04Merge PR #7416: Fix #7415. Printing Width was not applied to error messages.Emilio Jesus Gallego Arias
2018-05-04Merge branch 'master' of https://github.com/ybertot/plugin_tutorialsYves Bertot
2018-05-04adds an explanation to Cmd8Yves Bertot
2018-05-04remove a typoYves Bertot
2018-05-04remove errors in the documentationYves Bertot
2018-05-04remove errors in the documentationYves Bertot
2018-05-04adds a comment in simple_print.ml and a plugin declaration in g_tuto1.ml4Yves Bertot
2018-05-04.gitignore fine-tuningYves Bertot
2018-05-04Now a command to access the value of a constantYves Bertot
2018-05-04adds more packaging boilerplate in tuto0Yves Bertot
2018-05-04finished type-checking examplesYves Bertot
2018-05-04Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Pierre-Marie Pédrot
2018-05-04Fix #7413: coqdep warning on repeated filesGaëtan Gilbert
2018-05-04follows G. Gilbert's suggestion to have polymorphism following a flagYves Bertot
2018-05-04A modified version that includes code proposed by G. GilbertYves Bertot
2018-05-04This revision contains a simple Check command.Yves Bertot
2018-05-03little cleanup on the defining command, and question in commentsYves Bertot
2018-05-03Merge PR #7134: When an error comes from loading the prelude, tell it happene...Emilio Jesus Gallego Arias
2018-05-03This version contains a simple command that defines a new constantYves Bertot
2018-05-03Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_substPierre-Marie Pédrot
2018-05-03Fix #7415. Printing Width was not applied to error messages.Pierre Courtieu
2018-05-03Add .byte targets for every bestocaml targetGaëtan Gilbert
2018-05-03Merge PR #7304: Make `intro`/`intros` progress on existential variables.Pierre-Marie Pédrot
2018-05-03Fixes issue #7083 / Windows build: Unify build logging to console (for appvey...Michael Soegtrop
2018-05-03Fixes issue #7081 / Windows build: strip in lablgtk build can fail randomlyMichael Soegtrop
2018-05-03Merge PR #7400: ci-vst.sh: use -o progsEmilio Jesus Gallego Arias
2018-05-03Merge PR #7402: [ci]: add pidetop (fix #7336)Emilio Jesus Gallego Arias
2018-05-02Making explicit that errors happen in one of five executation phases.Hugo Herbelin
2018-05-02Reporting when an error occurs at initialization time.Hugo Herbelin
2018-05-02Make "intro"/"intros" progress on existential variables.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 01:18:04 +0000