aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/coq_micromega.ml
AgeCommit message (Expand)Author
2017-06-01Bump year in headers.Maxime Dénès
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-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-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
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-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
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-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-01-12Update headers.Maxime Dénès
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-08-01Compatibility for compilation with ocaml 3.12 (at least).Hugo Herbelin
2014-08-01micromega : improve efficiency/termination of type-checkingFrédéric Besson
2014-07-31micromega : refification recognises @eq T for T convertible with Z or RFrédéric Besson
2014-06-23Fix semantics of change p with c to typecheck c at each specific occurrence o...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-01Fixing ml-doc.Pierre-Marie Pédrot
2014-03-03Fixing some generic equalities in Micromega.Pierre-Marie Pédrot
2013-11-15bugfix micromega: solved an ambiguous symbol resolutionfbesson
2013-08-22Misc changes around coqtop.ml :letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 11)letouzey
2012-12-14Modulification of identifierppedrot
2012-12-08Ensure that a function declared with a label is used with itletouzey
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-01More cleaningppedrot
2012-04-12lib directory is cut in 2 cma.pboutill
2012-01-14coq_micromega.ml: fix order of recursive calls to rconstantglondu
2012-01-14More newlines in debugging output of psatzlglondu
2011-07-29Coq_micromega: generic = on constr replaced by eq_constrpuech
2011-05-25Q2R -> IQRfbesson
2011-05-23git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...fbesson
2011-05-20added support to handle division by a constant over Rfbesson
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:26:53 +0000