aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Coercion API using EConstr.Pierre-Marie Pédrot
2017-02-14Classops API using EConstr.Pierre-Marie Pédrot
2017-02-14Typeclasses API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacred API using EConstr.Pierre-Marie Pédrot
2017-02-14Constr_matching API using EConstr.Pierre-Marie Pédrot
2017-02-14Patternops API using EConstr.Pierre-Marie Pédrot
2017-02-14Typing API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Recordops API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarsolve API using EConstr.Pierre-Marie Pédrot
2017-02-14Evardefine API using EConstr.Pierre-Marie Pédrot
2017-02-14Find_subterm API using EConstr.Pierre-Marie Pédrot
2017-02-14Cbv API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Nativenorm API using EConstr.Pierre-Marie Pédrot
2017-02-14Vnorm API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2017-02-14Merge PR#253: Sort Search results by relevanceMaxime Dénès
2017-02-14Test-suite: output of SearchArnaud Spiwack
2017-02-13Merge PR#349: Proofview: tclINDEPENDENTLMaxime Dénès
2017-02-10Proofview: tclINDEPENDENTLEnrico Tassi
2017-02-09Turning an anomaly on 'pat into a proper "unsupported" error message.Hugo Herbelin
2017-02-09Fixing bug #5346 (an unimplemented application of 'pat).Hugo Herbelin
2017-02-08Merge PR#405: Type cleanup in `Metasyntax`Maxime Dénès
2017-02-08Merge PR#393: Replace Typeops with Fast_typeopsMaxime Dénès
2017-02-07Revert "Extraction: avoid deprecated functions of module String"Pierre Letouzey
2017-02-07Extraction cosmetic: no whitespaces in printing empty modulesPierre Letouzey
2017-02-07Extraction: remove the "print to devnull" hack now that pp isn't lazy anymorePierre Letouzey
2017-02-07Extraction: avoid deprecated functions of module StringPierre Letouzey
2017-02-07Extraction: simplify the generated code for difficult name conflictsPierre Letouzey
2017-02-07Extraction : get_duplicates (via option) instead of check_duplicates (via Not...Pierre Letouzey
2017-02-07configure: avoid deprecated warningsPierre Letouzey
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2017-02-07Merge PR#425: [travis] [External CI] [geocoq] don't build slow fileMaxime Dénès
2017-02-07Add test-suite files for hintdb variables in Ltac.Théo Zimmermann
2017-02-07Remove hackish autounfoldify now that hintdb can be bound to Ltac variables.Théo Zimmermann
2017-02-07pre_ident can be bound to Ltac variables.Théo Zimmermann
2017-02-07[travis] [External CI] [geocoq] don't build slow fileEmilio Jesus Gallego Arias
2017-02-07Merge PR#424: [travis] [External CI] iris-coq: fix dependenciesMaxime Dénès
2017-02-07[travis] [External CI] iris-coq: fix dependenciesEmilio Jesus Gallego Arias
2017-02-07Type cleanup in `Metasyntax`Emilio Jesus Gallego Arias
2017-02-07Merge PR#421: [travis] Perform parallel testingMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-28 12:06:57 +0000