aboutsummaryrefslogtreecommitdiff
path: root/plugins/romega
AgeCommit message (Expand)Author
2017-05-22romega: discard constructor D_mono (shorter trace + fix a bug)Pierre Letouzey
2017-05-22refl_omega: more refactoring (e.g. IntSets instead of sorted lists)Pierre Letouzey
2017-05-22refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)Pierre Letouzey
2017-05-22ReflOmegaCore: discard useless cosntructor P_NOPPierre Letouzey
2017-05-22ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||])Pierre Letouzey
2017-04-24Removing trivial compatibility layer in refl_omega.Pierre-Marie Pédrot
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-08-09Reduce warning noise when compiling the standard library.Guillaume Melquiond
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
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-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-02-24Getting rid of the "<:tactic< ... >>" quotations.Pierre-Marie Pédrot
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25Clean up a comment in plugins/romega/ReflOmegaCoreJason Gross
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-06-23Fix semantics of change p with c to typecheck c at each specific occurrence o...Matthieu Sozeau
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 15)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 11)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 7)letouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-18No more constant named "int" in Coq theories (cf bug #2878)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:20:36 +0000