aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-08Change the toplevel representation of Ltac values to an untyped one.Pierre-Marie Pédrot
2016-05-08Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
2016-05-04typoEnrico Tassi
2016-05-04NPeano : improve compatibility for this deprecated file via compat notationsPierre Letouzey
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-05-04Interpretation function can return any untyped value.Pierre-Marie Pédrot
2016-05-04Removing external uses of Val.inject and making Geninterp.interp return Val.tPierre-Marie Pédrot
2016-05-04Removing the Value.of_* API for parameterized types.Pierre-Marie Pédrot
2016-05-04Do not generate generic arguments for data which only requires toplevel values.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Simplifying the code of Tacinterp.Pierre-Marie Pédrot
2016-05-04Getting rid of the Geninterp.generic_interp function.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
2016-05-04Moving Ftactic and Geninterp to the engine folder.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04Int.v: simplify Jason's commit 5b4e3acePierre Letouzey
2016-05-04Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...Pierre Letouzey
2016-05-04Fixing subst.out after changing spacing in goal output (24a125b77).Hugo Herbelin
2016-05-04Fix Haskell extraction for terms over 45 characters longNickolai Zeldovich
2016-05-04Handle primitive projections inside types when extracting (bug #4616).Guillaume Melquiond
2016-05-04Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.Maxime Dénès
2016-05-04Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t...Pierre Letouzey
2016-05-04Increase the size of the dumpglob buffer for cooking notations (bug #4708).Guillaume Melquiond
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
2016-05-03Fix bug #4707: clearbody much slower in 8.5pl1.Pierre-Marie Pédrot
2016-05-03Fix bug #3825: Universe annotations on notations should pass through or be re...Pierre-Marie Pédrot
2016-05-03Test file for #4695: Slow Qed.Maxime Dénès
2016-05-03Fix bug #4292: Unexpected functor objects.Pierre-Marie Pédrot
2016-05-03Use the canonical name when looking for an eliminator (bug #4670).Guillaume Melquiond
2016-05-03A note concerning the "Drop" command.Matej Kosik
2016-05-03Fix bug #4705: coqtop accepts both -emacs and -ideslave.Pierre-Marie Pédrot
2016-05-03setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug.Matej Kosik
2016-05-03Call hooks when terminating a definition proof (bug #4663).Guillaume Melquiond
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-05-02Make votour a bit more robust/forgiving with respect to user commands (bug #4...Guillaume Melquiond
2016-05-02Properly handle notations containing spaces (bug #4538).Guillaume Melquiond
2016-05-02Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Guillaume Melquiond
2016-05-02Generate parsing rules for ML tactics in the same order as before a7917a32.Pierre-Marie Pédrot
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-02Useless code in Tacentries.Pierre-Marie Pédrot
2016-04-29Reduce ide/coq.png to 256x256.Guillaume Melquiond
2016-04-29Fix incorrect cbv reduction of primitive projections. (Bug #4634)Guillaume Melquiond
2016-04-28Make the language grammar much more precise. (Fix bugs #4682 and #4683)Guillaume Melquiond
2016-04-28Update tutorial (fix bug #4699).Guillaume Melquiond
2016-04-28Fix missing newline in coqchk engagement (bug #4694).Guillaume Melquiond
2016-04-28An example for cd139311e, showing a consequence of not convertingHugo Herbelin
2016-04-27Revert "A heuristic to add parentheses in the presence of rules such as"Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:33:10 +0000