aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-19Merge PR#784: API additions for coq-dpdgraphMaxime Dénès
2017-06-19Merge PR#755: "There are pending proofs" error message now lists the name of ...Maxime Dénès
2017-06-18Addressing #5434 (ltac pattern-matching refusing to match anonymous variables).Hugo Herbelin
2017-06-18[ide] Add route_id parameter to query call.Emilio Jesus Gallego Arias
2017-06-18[ide] Better exn printing. [fixes BZ#5524]Emilio Jesus Gallego Arias
2017-06-16Remove -j ${NJOBS} from make invocations in the ciJason Gross
2017-06-16Pass GNU Make jobserver on to the ci jobsJason Gross
2017-06-16Fix ci-fiat-crypto to have a proper lite targetJason Gross
2017-06-16Merge PR#804: Increase the time limit on 4366.v to make gitlab work better.Maxime Dénès
2017-06-16romega: avoid potential slowdown when changing concl by reified versionPierre Letouzey
2017-06-16Merge PR#759: don't leak unqualified identifiers from the macroMaxime Dénès
2017-06-16Merge PR#730: Protecting from warnings while compiling 8.6Maxime Dénès
2017-06-16Add coq-dpdgraph to gitlab CIGaëtan Gilbert
2017-06-16"There are pending proofs" error message now lists the name of the proofs.Théo Zimmermann
2017-06-16Increase the time limit on 4366.v to make gitlab work better.Gaëtan Gilbert
2017-06-16Each user overlay goes into its own file.Théo Zimmermann
2017-06-16Removing Proof_type from the API.Pierre-Marie Pédrot
2017-06-16Refactor documentation of records.Théo Zimmermann
2017-06-16Remove the last use of the low-level Proof_type API in ssr.Pierre-Marie Pédrot
2017-06-16Merge PR#767: Document named evars (including Show ident)Maxime Dénès
2017-06-16Fix a bug in cumulativityAmin Timany
2017-06-16A short cleanupAmin Timany
2017-06-16use map_constr more efficientlyAmin Timany
2017-06-16OptimizationAmin Timany
2017-06-16Use a smart map_constrAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Move (part of) tests from checker to successAmin Timany
2017-06-16Remove Warnings: unused value ...Amin Timany
2017-06-16Checker add test for non-trivial constraintsAmin Timany
2017-06-16Properly instantiate contexts before pushingAmin Timany
2017-06-16Enable the checking of ind subtyping in checkerAmin Timany
2017-06-16Document cumulativity for inductive typesAmin Timany
2017-06-16Change the option to Set Inductive CumulativityAmin Timany
2017-06-16Add printing of cumulativity in inductive typesAmin Timany
2017-06-16Move univops from kernel to libraryAmin Timany
2017-06-16Correct coqchk checking subtyping relation for inductivesAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2017-06-16Simplify Univ.mlAmin Timany
2017-06-16Fix a bugAmin Timany
2017-06-16Disable debug printingAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-16Make unification use subtyping info of inductivesAmin Timany
2017-06-16Fix cum/conv for inductive typesAmin Timany
2017-06-16Use inductive subtyping for conv/cumulAmin Timany
2017-06-16Change the place of inference after sect dischargeAmin Timany
2017-06-16Subtyping inference for inductoves and recordsAmin Timany
2017-06-16Add subtyping inference for inductive typesAmin Timany
2017-06-16Correct subtyping check for constructorsAmin Timany
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 16:44:45 +0000