aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/coq_micromega.ml
Commit message (Expand)AuthorAge
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)Gravatar Frédéric Besson2016-04-18
* Renaming functions in Typing to stick to the standard e_* scheme.Gravatar Pierre-Marie Pédrot2016-02-15
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Preventing an unwanted warning 5 "this function application is partial"Gravatar Hugo Herbelin2015-11-07
* | Indexing Proofview.goals with a stage.Gravatar Pierre-Marie Pédrot2015-10-20
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
* | micromega : options to limit proof searchGravatar Frédéric Besson2015-05-26
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
* | maintenance micromega pluginGravatar Frédéric Besson2015-04-28
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Writing the raw introduction tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-11-05
* Compatibility for compilation with ocaml 3.12 (at least).Gravatar Hugo Herbelin2014-08-01
* micromega : improve efficiency/termination of type-checkingGravatar Frédéric Besson2014-08-01
* micromega : refification recognises @eq T for T convertible with Z or RGravatar Frédéric Besson2014-07-31
* Fix semantics of change p with c to typecheck c at each specific occurrence o...Gravatar Matthieu Sozeau2014-06-23
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
* Fixing some generic equalities in Micromega.Gravatar Pierre-Marie Pédrot2014-03-03
* bugfix micromega: solved an ambiguous symbol resolutionGravatar fbesson2013-11-15
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* Restrict (try...with...) to avoid catching critical exn (part 11)Gravatar letouzey2013-03-13
* Modulification of identifierGravatar ppedrot2012-12-14
* Ensure that a function declared with a label is used with itGravatar letouzey2012-12-08
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* More cleaningGravatar ppedrot2012-06-01
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* coq_micromega.ml: fix order of recursive calls to rconstantGravatar glondu2012-01-14
* More newlines in debugging output of psatzlGravatar glondu2012-01-14
* Coq_micromega: generic = on constr replaced by eq_constrGravatar puech2011-07-29
* Q2R -> IQRGravatar fbesson2011-05-25
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...Gravatar fbesson2011-05-23
* added support to handle division by a constant over RGravatar fbesson2011-05-20
* apply zeta reduction before syntaxificationGravatar fbesson2011-05-18
* Improved lia + experimental nliaGravatar fbesson2011-05-09
* Definitions of positive, N, Z moved in Numbers/BinNums.vGravatar letouzey2011-05-05
* Solve name conflict about pow introduced by commit 13546.Gravatar letouzey2010-10-21
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Modify the test for csdp and associated message.Gravatar fkirchne2010-05-28
* ...Gravatar fkirchne2010-05-28
* Look for csdp in $PATH at runtime, remove -csdpdir configure optionGravatar glondu2010-04-11
* Application des patches envoyés par F. Besson pour micromegaGravatar notin2010-03-08
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03