aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/coq_micromega.ml
AgeCommit message (Expand)Author
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
2011-05-18apply zeta reduction before syntaxificationfbesson
2011-05-09Improved lia + experimental nliafbesson
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
2010-10-21Solve name conflict about pow introduced by commit 13546.letouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-28Modify the test for csdp and associated message.fkirchne
2010-05-28...fkirchne
2010-04-11Look for csdp in $PATH at runtime, remove -csdpdir configure optionglondu
2010-03-08Application des patches envoyés par F. Besson pour micromeganotin
2009-11-03OrderedType implementation for various numerical datatypes + min/max structuresletouzey
2009-10-04Removal of trailing spaces.serpyc
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:48:42 +0000