aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-06-16
* Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Function.Gravatar Hugo Herbelin2016-06-16
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* | Remove inappropriate comment.Gravatar Maxime Dénès2016-06-16
| * Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
* | ssrmatching: giving proper credits to the original author(s)Gravatar Enrico Tassi2016-06-15
* | ssrmatching: ltac argument parsing made more robustGravatar Enrico Tassi2016-06-15
* | ssrmatching: debug prints sent via msg_debugGravatar Enrico Tassi2016-06-15
* | Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"Gravatar Enrico Tassi2016-06-15
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | port ssrmatching plugin to the new makefileGravatar Enrico Tassi2016-06-14
* | Merge remote-tracking branch 'origin/pr/146' into trunkGravatar Enrico Tassi2016-06-14
|\ \
* \ \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \
* \ \ \ Merge remote-tracking branch 'github/evarunsafe' into trunkGravatar Matthieu Sozeau2016-06-14
|\ \ \ \
| * | | | newring: fix for hack using evars as integers.Gravatar Matthieu Sozeau2016-06-09
* | | | | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
|/ / / /
* | | | Officially discontinue the experimental coq build via ocamlbuildGravatar Pierre Letouzey2016-06-08
| * | | STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
|/ / /
* | | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\ \ \
* | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * | | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
* | | | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
| * | | Extraction/Projections: Fix bug #4710Gravatar Matthieu Sozeau2016-05-23
| * | | Disable memoization rather than failing when files cannot be opened.Gravatar Guillaume Melquiond2016-05-20
* | | | Extraction: code cleanup in CommonGravatar Pierre Letouzey2016-05-20
| * | | Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | | | Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | | | Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...Gravatar Pierre Letouzey2016-05-19
* | | | Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
* | | | Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | | Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | | | Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
* | | | More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
* | | | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| | |
| * | | Fix Haskell extraction for terms over 45 characters longGravatar Nickolai Zeldovich2016-05-04
| * | | Handle primitive projections inside types when extracting (bug #4616).Gravatar Guillaume Melquiond2016-05-04
* | | | Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t...Gravatar Pierre Letouzey2016-05-04
|\ \ \ \
| | * | | Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 17:34:20 +0000