aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2018-02-20Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Hugo Herbelin
2018-02-20Notations: Do not consider a non-occurring variable as a binder-only variable.Hugo Herbelin
2018-02-20More precise explanation when a notation is not reversible for printing.Hugo Herbelin
2018-02-20Adding support for re-folding notation referring to isolated "forall '(x,y), t".Hugo Herbelin
2018-02-20Again one more step in fixing #5762 ("where" clause).Hugo Herbelin
2018-02-19ci: add elpiEnrico Tassi
2018-02-19record: restore API declare_projections (removed in e414c07e1)Enrico Tassi
2018-02-19pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)Enrico Tassi
2018-02-19Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...Maxime Dénès
2018-02-19Merge PR #6761: Remove unused argument in Record.declare_structureMaxime Dénès
2018-02-19Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Maxime Dénès
2018-02-19Merge PR #6753: [toplevel] Make toplevel state into a record.Maxime Dénès
2018-02-19Fix #6529: nf_evar_info and check the env evars' not just the conclMatthieu Sozeau
2018-02-19Merge PR #6230: Better Cemitcodes API + compact relocation representationMaxime Dénès
2018-02-19Merge PR #6759: detype_case predicate is not optionalMaxime Dénès
2018-02-19Merge PR #6772: Cleanup inferCumulativityMaxime Dénès
2018-02-19Merge PR #6648: [tactics] make apply_type safeMaxime Dénès
2018-02-19Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...Maxime Dénès
2018-02-19Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Maxime Dénès
2018-02-19Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.Maxime Dénès
2018-02-19Merge PR #6571: Fix ci-all targetMaxime Dénès
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2018-02-17Implement name mangling optionJasper Hugunin
2018-02-16apply_type: add option "typecheck" passed down to refineEnrico Tassi
2018-02-16Cleaner treatment of parameters in inferCumulativityGaëtan Gilbert
2018-02-16Fix reduction flags in inferCumulativityGaëtan Gilbert
2018-02-16Adding a test for the construction that was broken in Coccinelle.Pierre-Marie Pédrot
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2018-02-15Adding a test for variance subtyping in the module system.Pierre-Marie Pédrot
2018-02-15Adding a sanity check on inductive variance subtyping.Pierre-Marie Pédrot
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
2018-02-15[ide] Localize a IDE-specific flag.Emilio Jesus Gallego Arias
2018-02-15Merge PR #1073: new quick2vo target: like vio2vo, but smarterMaxime Dénès
2018-02-15disable tests: vio2vo is broken in WindowsRalf Jung
2018-02-15also test vio2voRalf Jung
2018-02-15test "make quick2vo"Ralf Jung
2018-02-15new quick2vo target: like vio2vo, but smarterRalf Jung
2018-02-15Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectMaxime Dénès
2018-02-15coq_makefile: Support "" as the prefix in _CoqProjectJoachim Breitner
2018-02-15Merge PR #6760: CHANGES for 8.7.2.Maxime Dénès
2018-02-14Extend `zify_N` with knowledge about `N.pred`Joachim Breitner
2018-02-14CHANGES for 8.7.2.Théo Zimmermann
2018-02-14Remove unused argument in Record.declare_structureGaëtan Gilbert
2018-02-14Factorize the relocations in the on-disk VM representation.Pierre-Marie Pédrot
2018-02-14Use a more compact representation for bytecode relocations stored on disk.Pierre-Marie Pédrot
2018-02-14Do not use global variables for VM bytecode compilation in Cemitcodes.Pierre-Marie Pédrot
2018-02-14Remove the unsafe bytes conversion function in Cemitcodes.Pierre-Marie Pédrot
2018-02-14Move the call to the computation of bytecode inside Cemitcodes.Pierre-Marie Pédrot
2018-02-14Abstract further the type of VM bytecode compilation.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 00:06:34 +0000