| Commit message (Expand) | Author | Age |
* | ReflOmegaCore: comment, reorganize, permut some constructors, etc | Pierre Letouzey | 2017-05-22 |
* | romega: add a tactic named unsafe_romega (for debugging, or bold users) | Pierre Letouzey | 2017-05-22 |
* | romega: no more normalization trace, replaced by some Coq-side computation | Pierre Letouzey | 2017-05-22 |
* | romega/const_omega : a few improvements (less try with, no gen equality) | Pierre Letouzey | 2017-05-22 |
* | romega: use N instead of nat for Tvar | Pierre Letouzey | 2017-05-22 |
* | romega: shorter trace (no more term lengths) | Pierre Letouzey | 2017-05-22 |
* | refl_omega: refactoring of normalize_equation | Pierre Letouzey | 2017-05-22 |
* | ReflOmegaCore: lots of dead code + a few refactored proofs | Pierre Letouzey | 2017-05-22 |
* | romega: if it bugs again, at least do it with a short and quick error | Pierre Letouzey | 2017-05-22 |
* | refl_omega: comment the lack of lifts when dealing with arrows | Pierre Letouzey | 2017-05-22 |
* | romega: discard constructor D_mono (shorter trace + fix a bug) | Pierre Letouzey | 2017-05-22 |
* | refl_omega: more refactoring (e.g. IntSets instead of sorted lists) | Pierre Letouzey | 2017-05-22 |
* | refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp) | Pierre Letouzey | 2017-05-22 |
* | ReflOmegaCore: discard useless cosntructor P_NOP | Pierre Letouzey | 2017-05-22 |
* | ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||]) | Pierre Letouzey | 2017-05-22 |
* | Removing trivial compatibility layer in refl_omega. | Pierre-Marie Pédrot | 2017-04-24 |
* | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 |
|\ |
|
| * | Moving the Ltac plugin to a pack-based one. | Pierre-Marie Pédrot | 2017-02-17 |
* | | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Tacmach API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
|/ |
|
* | Merging Stdarg and Constrarg. | Pierre-Marie Pédrot | 2016-09-21 |
* | Reduce warning noise when compiling the standard library. | Guillaume Melquiond | 2016-08-09 |
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey | 2016-07-03 |
* | Compilation via pack for plugins of the stdlib | Pierre Letouzey | 2016-06-08 |
* | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot | 2016-06-03 |
* | Feedback cleanup | Emilio Jesus Gallego Arias | 2016-05-31 |
* | Put the "generalize" tactic in the monad. | Pierre-Marie Pédrot | 2016-05-16 |
* | Removing dead code and unused opens. | Pierre-Marie Pédrot | 2016-05-08 |
* | Removing the special status of generic entries defined by Coq itself. | Pierre-Marie Pédrot | 2016-03-17 |
* | Making parentheses mandatory in tactic scopes. | Pierre-Marie Pédrot | 2016-03-04 |
* | Getting rid of the "<:tactic< ... >>" quotations. | Pierre-Marie Pédrot | 2016-02-24 |
* | Moving conversion functions to the new tactic API. | Pierre-Marie Pédrot | 2016-02-15 |
* | Fix some typos. | Guillaume Melquiond | 2015-12-07 |
* | Fix some typos. | Guillaume Melquiond | 2015-10-13 |
* | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
* | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin | 2014-12-07 |
* | "allows to", like "allowing to", is improper | Jason Gross | 2014-08-25 |
* | Clean up a comment in plugins/romega/ReflOmegaCore | Jason Gross | 2014-08-25 |
* | Grammar: "allowing to" is not proper English | Jason Gross | 2014-08-25 |
* | Reorganization of tactics: | Hugo Herbelin | 2014-08-18 |
* | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau | 2014-06-23 |
* | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot | 2014-05-12 |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
* | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack | 2013-11-02 |
* | More monomorphic List.mem + List.assoc + ... | letouzey | 2013-10-24 |
* | Turn many List.assoc into List.assoc_f | letouzey | 2013-10-24 |