ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • 24523434a3 Fix API examples Benjamin Jorge 2025-01-23 11:11:54 +01:00
  • 667ab3ae79 Sandwich implementation Benjamin Jorge 2025-01-21 11:38:23 +01:00
  • 89646602d4 Rename pmodule by pmodule0 Benjamin Jorge 2025-01-21 11:38:23 +01:00
  • c1769ff469 Use Pmodule.mlw_file instead of Pmodule.pmodule Mstr.t in several places Benjamin Jorge 2025-01-21 11:13:50 +01:00
  • 8731d93074 Merge impl'of and some'scope Benjamin Jorge 2025-03-18 16:46:09 +01:00
  • c9f95bf6ee Introduce copy_module and use it in close_module_with_intf Benjamin Jorge 2025-03-13 14:53:02 +01:00
  • c604358fb7 Improve slightly the names in Pmodule.close_module_with_intf Benjamin Jorge 2025-03-17 16:50:52 +01:00
  • f2b4d2bf36 Move code from Typing.close_module to Pmodule.close_module_with_intf Benjamin Jorge 2025-11-19 19:31:48 +01:00
  • cdf7dd79d0 Move scope opening in close_module_with_intf Benjamin Jorge 2025-11-19 18:35:07 +01:00
  • 1ee30b5b07 Improve module interface API Benjamin Jorge 2025-03-17 15:25:18 +01:00
  • 12f83fcfcc Extract inst_of_clones from clone_export Benjamin Jorge 2025-03-12 19:23:15 +01:00
  • db547d5b47 Extract clone_meta_arg from clone_export Benjamin Jorge 2025-03-12 19:20:58 +01:00
  • 13e02033dc Extract transpose_inst from mi_impl Benjamin Jorge 2025-03-12 19:11:29 +01:00
  • 52d4c44cfb Better idents and Glob references for modules with interface Benjamin Jorge 2025-03-14 13:45:19 +01:00
  • ddedf3d524 Rename interface exceptions Benjamin Jorge 2025-11-19 18:50:35 +01:00
  • cb0a4a1e60 Fix coq realizations Benjamin Jorge 2025-04-25 18:22:59 +02:00
  • 19f2fc7297 Delay ident creation to Theory.close_theory Benjamin Jorge 2025-04-23 15:31:06 +02:00
  • d47088c6d3 Merge branch 'fix_doc_for_loop' into 'master' MARCHE Claude 2025-11-19 14:33:15 +01:00
  • e5f6a089fe fix doc of for loops Claude Marche 2025-11-19 13:18:39 +01:00
  • ed0388367f Merge branch 'cleaning-schorr-waite' into 'master' Jean-Christophe Filliâtre 2025-11-18 16:19:29 +01:00
  • c437d7d907 gallery: cleaning Schorr-Waite with autodereference and more recent provers Jean-Christophe Filliatre 2025-11-18 09:44:26 +01:00
  • d1d3fb9bda Compute status for unproved VC in why3 Johannes Kanig 2025-11-14 11:53:41 +09:00
  • eea70d139c Merge branch 'topic/kanig-mr-approve' into 'master' Johannes Kanig 2025-11-14 09:32:45 +00:00
  • 31e47057af Approve MR in addition to creating it, plus skip CI Johannes Kanig 2025-11-14 17:25:49 +09:00
  • 964b243357 Merge branch 'topic/kanig-ast' into 'master' Johannes Kanig 2025-11-12 11:06:26 +00:00
  • e6c44bb771 Follow AST change in gnat2why Johannes Kanig 2025-11-06 14:59:01 +09:00
  • c13da9842d Merge branch 'topic/kanig-338-fix' into 'master' Johannes Kanig 2025-11-11 11:52:16 +00:00
  • 176dada6b1 Fix use of 'target_branch' Johannes Kanig 2025-11-11 20:16:58 +09:00
  • 848a78f42a Merge branch 'topic/update-submodule' into 'master' Johannes Kanig 2025-11-11 11:03:33 +00:00
  • 0c77e284c4 Add comment Johannes Kanig 2025-11-10 10:05:58 +09:00
  • 75b425a559 Review comments and reformatting Johannes Kanig 2025-11-10 09:53:05 +09:00
  • 8f2c5841e7 Merge branch 'typo-mach-bv' into 'master' MARCHE Claude 2025-11-07 16:30:24 +01:00
  • d0516805c3 Merge branch 'fix-ring-buffer' into 'master' Mario Pereira 2025-11-07 14:29:31 +00:00
  • 4d3adc9a7d Fix type invariant for the ring buffer example Mario Pereira 2025-11-07 14:29:31 +00:00
  • 608224819c Automatic submodule commit Johannes Kanig 2025-09-01 09:57:34 +09:00
  • 5e95911997 Merge branch 'new-example-priority-queue' into 'master' Jean-Christophe Filliâtre 2025-11-05 20:14:25 +01:00
  • 14ba8b392d gallery: priority queues Jean-Christophe Filliatre 2025-11-05 17:57:04 +01:00
  • febb62d125 Fix mach/bv.mlw Benjamin Jorge 2025-09-03 11:37:01 +02:00
  • 883154fa71 Merge branch 'topic/fsf_merge_269/20251022' into 'fsf' Marc Poulhiès 2025-11-04 08:55:01 +01:00
  • 6f0a133594 Merge commit 'c8134ce4f2a54bf65d3e42d5d5b1772fc63792c9' into topic/fsf_merge_269/20251022 Marc Poulhiès 2025-11-03 15:28:59 +01:00
  • 51e0579b35 Merge branch 'multi-spans' into 'master' XIA Li-Yao 2025-10-29 17:31:55 +01:00
  • 061ff8cc12 Merge branch 'coma-errors-2' into 'master' XIA Li-Yao 2025-10-29 11:30:30 +01:00
  • 59c33b7a73 Merge branch 'coma-errors' into 'master' XIA Li-Yao 2025-10-29 11:29:38 +01:00
  • e25794ab12 ide: Open multiple files associated to the same goal Li-yao Xia 2025-10-17 17:22:09 +02:00
  • ea57d79058 coma: Allow annotating function calls with source locations Li-yao Xia 2025-10-17 16:54:37 +02:00
  • f0d09ca4fd coma: Track callers in VC generation Li-yao Xia 2025-10-17 16:19:41 +02:00
  • 5ef8115d8d Update term to carry multiple locations Li-yao Xia 2025-10-17 15:46:36 +02:00
  • b9a59a9ebb coma: Add field for function call locations Li-yao Xia 2025-10-17 14:15:55 +02:00
  • 81affec0ed Merge branch 'lident_doc' into 'master' MARCHE Claude 2025-10-17 17:01:47 +02:00
  • b380cb66bd Merge branch 'post-release-181' into 'master' MARCHE Claude 2025-10-17 17:01:01 +02:00
  • 85ff1f8bae Merge branch '925-make-some-warnings-more-visible-or-even-errors-by-default' into 'master' MARCHE Claude 2025-10-17 15:14:51 +02:00
  • c24878ec9f fix warnings in IDE Claude Marche 2025-10-17 14:00:15 +02:00
  • 64b6266f58 coma: locate some error messages Li-yao Xia 2025-10-17 12:42:46 +02:00
  • 40c4493907 Merge branch '923-pdflatex-manual-tex-fails' into 'master' MARCHE Claude 2025-10-17 12:10:32 +02:00
  • 340fc7b46e coma: better better type error messages Li-yao Xia 2025-10-17 10:14:13 +02:00
  • d949b4639b make output of Kim accent simpler Claude Marche 2025-10-17 10:52:15 +02:00
  • 7064223432 coma: typing better error messages Paul Patault 2025-09-03 10:51:44 +02:00
  • bc4034559b Merge branch 'gnome-sort-variant-improved' into 'master' Jean-Christophe Filliâtre 2025-10-15 11:44:09 +02:00
  • 052039edbc Merge branch 'yet-another-sudoku-solver' into 'master' Jean-Christophe Filliâtre 2025-10-15 11:10:21 +02:00
  • 830473fcbf gnome-sort: improved variant Jean-Christophe Filliatre 2025-10-15 09:48:01 +02:00
  • c8134ce4f2 Merge branch 'topic/kanig-1029-1.8.2' into 'master' Johannes Kanig 2025-10-15 00:49:09 +00:00
  • e981539d23 Commit configure after why3 changes Johannes Kanig 2025-10-14 10:47:56 +09:00
  • 6271ca4ab4 Revert "[Debug_option] Use default ppxlib ast for better compatibility" Johannes Kanig 2025-10-14 10:47:14 +09:00
  • a2807b3ddb Merge 1.8.2 into AdaCore master Johannes Kanig 2025-10-14 10:32:03 +09:00
  • 3b8cd4aac9 fix issue with file Ids in sessions Claude Marche 2025-06-11 10:08:46 +02:00
  • b37dee0e79 update release doc Claude Marche 2025-06-04 11:15:46 +02:00
  • becf440dfd Merge branch 'fix_numeric_lse' into 'master' MARCHE Claude 2025-10-08 12:18:30 +02:00
  • e802169b43 Improve numeric examples on exp and log MARCHE Claude 2025-10-08 12:18:30 +02:00
  • fa7f8f6177 yet another Sudoku solver Jean-Christophe Filliatre 2025-10-08 11:16:11 +02:00
  • d5877421a9 Merge branch 'fix_numeric_sessions' into 'master' MARCHE Claude 2025-09-30 14:41:52 +02:00
  • d344b75294 fix proofs in subdir numeric Claude Marche 2025-09-30 13:34:10 +02:00
  • b7ba76b7cd Merge branch '926-the-reduction-engine-does-not-work-well-with-triggers' into 'master' MARCHE Claude 2025-09-29 19:52:11 +02:00
  • 6f2e594fa1 reproducer and fix Claude Marche 2025-09-29 13:45:26 +02:00
  • cc8da27af9 Merge branch 'compile_with_rocq' into 'master' MARCHE Claude 2025-09-17 17:03:25 +02:00
  • 609cd64dae Fix build with Rocq Stdlib 9.0 MARCHE Claude 2025-09-17 17:03:24 +02:00
  • 3eaf43f78e missing CHANGE from version 1.8.2 Claude Marche 2025-09-16 15:17:23 +02:00
  • 88b18b1ae3 Version 1.8.2 Claude Marche 2025-09-16 17:37:32 +02:00
  • 021688820f missing CHANGEs Claude Marche 2025-09-16 15:17:23 +02:00
  • 3f5b3c1dd1 [Debug_option] Use default ppxlib ast for better compatibility François Bobot 2025-06-11 09:28:16 +02:00
  • 91f19aeb00 Adapt ppx_debug_optim to ppxlib Benjamin Jorge 2025-06-06 16:45:29 +02:00
  • 71fed79f48 update oracles Claude Marche 2025-09-16 13:53:09 +02:00
  • d5cedf4c44 check-ce are done with AE 2.6.0 Claude Marche 2025-09-16 10:37:15 +02:00
  • 868636f1f9 Merge branch 'topic/fsf_merge_269/20250903' into 'fsf' Marc Poulhiès 2025-09-16 10:14:30 +02:00
  • f2505afa0c Drop AdaCore CI Marc Poulhiès 2025-09-16 10:06:59 +02:00
  • 8dc1ad1f1f Merge commit 'fa7bfb38628a6bfc7bf19fb274605375a8ab2399' into topic/fsf_merge_269/20250903 Marc Poulhiès 2025-09-16 10:06:18 +02:00
  • 506efc97c6 update ae version for CE checking Claude Marche 2025-09-15 15:03:51 +02:00
  • 9edb02fc65 Fix build with Rocq Stdlib 9.0 Claude Marche 2025-09-15 14:01:08 +02:00
  • 16f1d43b2a Version 1.8.2 Claude Marche 2025-09-12 14:44:32 +02:00
  • 351afd9af7 update changes for v1.8.2 Claude Marche 2025-09-12 14:40:43 +02:00
  • ccf38d4890 Compile again programs extracted to OCaml and JS Claude Marche 2025-04-02 14:37:47 +02:00
  • 2f81410a1c update release instructions after release Claude Marche 2025-06-06 10:21:52 +02:00
  • 7650683aed There is no symbol ae.sqrt_real parsed by Alt-Ergo 2.6 Claude Marche 2025-06-11 10:08:46 +02:00
  • c23f9e5aff fix issue with file Ids in sessions Claude Marche 2025-06-11 10:08:46 +02:00
  • 4e4e13edaa Alt-Ergo 2.6 driver, functions on reals, float rounding Johannes Kanig 2025-06-06 12:00:50 +02:00
  • db3fe92912 update release doc Claude Marche 2025-06-04 11:15:46 +02:00
  • d2a8e9ad43 Merge branch 'v182git' into 'master' MARCHE Claude 2025-09-15 13:38:49 +02:00
  • e053e2ef6b update after release 1.8.2 MARCHE Claude 2025-09-15 13:38:49 +02:00
  • a594d1c33c Merge branch 'improved-union-find-example' into 'master' Jean-Christophe Filliâtre 2025-09-02 16:29:14 +02:00
  • 2698cee666 gallery: improved union-find Jean-Christophe Filliatre 2025-09-02 15:19:50 +02:00
  • fa7bfb3862 Merge branch 'topic/kanig-typo' into 'master' 26.0 Johannes Kanig 2025-08-29 00:01:54 +00:00