aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega
Commit message (Expand)AuthorAge
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Fix some typos.Gravatar Guillaume Melquiond2015-04-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* 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
* Bugfix 3604 : more robust Unix.lockfGravatar Frédéric Besson2014-10-22
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",Gravatar Xavier Clerc2014-09-25
* Remove some 'deprecated' warnings.Gravatar Xavier Clerc2014-09-25
* Correct a spelling mistakeGravatar Jason Gross2014-08-25
* More proofs independent of the names generated by induction/elim overGravatar Hugo Herbelin2014-08-05
* micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Gravatar Frédéric Besson2014-08-01
* 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
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
* Fixing some generic equalities in Micromega.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Relaunch all Unix.waitpid when they ended with EINTRGravatar Pierre Letouzey2014-01-30
* micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...Gravatar Frédéric Besson2013-12-20
* Silence compilation warning by avoiding some deprecated constructs.Gravatar Guillaume Melquiond2013-12-03
* bugfix micromega: solved an ambiguous symbol resolutionGravatar fbesson2013-11-15
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Oups, repair the compilation (micromega + Morphism_prop)Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* Reintroduce "or" instead of "||" as the latter is redifined in "sos_lib.ml" w...Gravatar xclerc2013-10-16
* Remove some uses of local modules (some were unused, some were costly).Gravatar xclerc2013-10-14
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* micromega: remove empty file CheckerMakerGravatar letouzey2013-08-22
* Restrict (try...with...) to avoid catching critical exn (part 15)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 11)Gravatar letouzey2013-03-13
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* 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
* still some more dead code removalGravatar letouzey2012-10-06
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08