aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
AgeCommit message (Expand)Author
2016-11-24Lazily load constants in micromega (bug #5134).Guillaume Melquiond
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
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-06-06micromega : fix silly timeoutFrédéric Besson
2015-05-26micromega : options to limit proof searchFrédéric Besson
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-04-28maintenance micromega pluginFrédéric Besson
2015-04-02Fix some typos.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-11-05Writing the raw introduction tactic in the new monad.Pierre-Marie Pédrot
2014-10-22Bugfix 3604 : more robust Unix.lockfFrédéric Besson
2014-10-01Simpl less (so that cbn will not simpl too much)Pierre Boutillier
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-25Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",Xavier Clerc
2014-09-25Remove some 'deprecated' warnings.Xavier Clerc
2014-08-25Correct a spelling mistakeJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:09:20 +0000