aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega
Commit message (Expand)AuthorAge
* 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
* Try to make the use of Unix.lockf in micromega compatible with Win32Gravatar letouzey2012-08-06
* Ring_polynom : a restricted simpl instead of a unfold;foldGravatar letouzey2012-07-07
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
* rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteGravatar letouzey2012-07-05
* More cleanup in Ring_polynom and EnvRingGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Cleaning opening of the standard List module.Gravatar ppedrot2012-06-28