aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
* 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
* 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
* | | Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing printing of Function."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Adding printers for ring and field commands."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing a mispelling coma -> comma."Gravatar Hugo Herbelin2016-04-27
* | | Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
* | | Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-04-27
* | | Fixing printing of Function.Gravatar Hugo Herbelin2016-04-27
* | | Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-04-27
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\ \ \ | | |/ | |/|
* | | Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)Gravatar Frédéric Besson2016-04-18
* | | Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\ \ \
| | * | Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vGravatar Nickolai Zeldovich2016-04-09
| |/ /
| * | Fixing a source of inefficiency and an artificial dependency in theGravatar Daniel de Rauglaudre2016-04-08
* | | Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
* | | Moving the proof mode parsing management to Pcoq.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Removing the special status of generic arguments defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Adding a universe argument to Pcoq.create_generic_entry.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* | | Removing OCaml deprecated function names from the Lazy module.Gravatar Pierre-Marie Pédrot2016-03-10
* | | Removing useless grammar.cma dependencies.Gravatar Pierre-Marie Pédrot2016-03-06
* | | Splitting the nsatz ML module into an implementation and a grammar files.Gravatar Pierre-Marie Pédrot2016-03-06
* | | Moving Eauto to a simple ML file.Gravatar Pierre-Marie Pédrot2016-03-06
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\| |
* | | Using build_selector from Equality as a replacement of the selectorGravatar Hugo Herbelin2016-03-05
| * | Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* | | Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* | | Getting rid of the "<:tactic< ... >>" quotations.Gravatar Pierre-Marie Pédrot2016-02-24
* | | Moving the Tauto tactic to proper Ltac.Gravatar Pierre-Marie Pédrot2016-02-22
* | | The tactic generic argument now returns a value rather than a glob_expr.Gravatar Pierre-Marie Pédrot2016-02-22