aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
AgeCommit message (Expand)Author
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24Removing tactic compatibility layer in Micromega.Pierre-Marie Pédrot
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-22Remove duplicate lemmas.Guillaume Melquiond
2017-03-09Micromega: removing a constant preventing micromega to be loaded before Logic.v.Hugo Herbelin
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Micromega API using EConstr.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Tactics 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-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-24Lazily load constants in micromega (bug #5134).Guillaume Melquiond
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-16Make the Coq codebase independent from Ltac-related code.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
2016-09-07micromega : more robust generation of proof termsFrédéric Besson
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-01Fixed Bug #5003 : more careful generalisation of dependent terms.Frédéric Besson
2016-08-31Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Frédéric Besson
2016-08-30plugin micromega : nra also handles non-linear rational arithmetic over Q (Fi...Frédéric Besson
2016-08-30micromega cache files are now hidden files (cf #4156)Frédéric Besson
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
2016-07-05Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Maxime Dénès
2016-07-04Merge remote-tracking branch 'github/pr/229' into trunkMaxime Dénès
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29Makefile: no bytecode compilation in make world, see make byte insteadPierre Letouzey
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-20Disable memoization rather than failing when files cannot be opened.Guillaume Melquiond
2016-05-19Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...Pierre Letouzey
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-04-18Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)Frédéric Besson
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-01Fix typos.Guillaume Melquiond
2015-12-21Changing the toplevel type of the int_or_var generic type to int.Pierre-Marie Pédrot
2015-11-07Preventing an unwanted warning 5 "this function application is partial"Hugo Herbelin
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 00:13:17 +0000