Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
85
Issues
85
List
Boards
Labels
Milestones
Merge Requests
10
Merge Requests
10
Packages
Packages
Container Registry
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Repository
9a3608201dd12c708eb4adb4322e2e3f4835d501
Switch branch/tag
why3
tests
History
Find file
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
Download this directory
zip
tar.gz
tar.bz2
tar
OCaml extraction:
· 9f6a9955
Mário Pereira
authored
Mar 14, 2019
proper extraction of named and optional arguments in functions with polymorphic arguments.
9f6a9955
Name
Last commit
Last update
..
PGCD
Loading commit data...
add_list
Loading commit data...
computation
Loading commit data...
demo-itp
Loading commit data...
example-add
Loading commit data...
jessie
Loading commit data...
label
Loading commit data...
old
Loading commit data...
python
Loading commit data...
test-extraction
Loading commit data...
test-ind
Loading commit data...
test-settheory
Loading commit data...
test-shape
Loading commit data...
test-smoke-detector
Loading commit data...
test_args_parsing
Loading commit data...
test_compute
Loading commit data...
test_itp
Loading commit data...
test_merge
Loading commit data...
test_smoke
Loading commit data...
PGCD.mlw
Loading commit data...
SimpleDBPath.why
Loading commit data...
SimpleDBPathSansListes.why
Loading commit data...
add_list.mlw
Loading commit data...
array_eq.mlw
Loading commit data...
bug-transf.why
Loading commit data...
computation.why
Loading commit data...
course2.mlw
Loading commit data...
demo-itp.mlw
Loading commit data...
dubious_axioms.mlw
Loading commit data...
example-add.mlw
Loading commit data...
extract_ghost.mlw
Loading commit data...
label.mlw
Loading commit data...
multiassign.mlw
Loading commit data...
my_cosine.c
Loading commit data...
my_cosine.mlw
Loading commit data...
old.mlw
Loading commit data...
sum_list00.mlw
Loading commit data...
test-and.why
Loading commit data...
test-bobot.why
Loading commit data...
test-claude.mlw
Loading commit data...
test-claude.why
Loading commit data...
test-div-cvc3.why
Loading commit data...
test-eval.why
Loading commit data...
test-gappa2.why
Loading commit data...
test-ghost.mlw
Loading commit data...
test-ind.why
Loading commit data...
test-literals.mlw
Loading commit data...
test-match.why
Loading commit data...
test-poly.why
Loading commit data...
test-polyrec.why
Loading commit data...
test-settheory.why
Loading commit data...
test-shape.why
Loading commit data...
test-smoke-detector.why
Loading commit data...
test-zenon.why
Loading commit data...
test_args_parsing.mlw
Loading commit data...
test_argument.why
Loading commit data...
test_argument.whyitp
Loading commit data...
test_compute.why
Loading commit data...
test_exec.mlw
Loading commit data...
test_extraction.mlw
Loading commit data...
test_ghost.mlw
Loading commit data...
test_itp.mlw
Loading commit data...
test_loc.why
Loading commit data...
test_merge.mlw
Loading commit data...
test_ne.mlw
Loading commit data...
test_range.mlw
Loading commit data...
test_rewrite.mlw
Loading commit data...
test_smoke.mlw
Loading commit data...
test_theory_expl.why
Loading commit data...
test_tptp.ml
Loading commit data...
tests-boolean.mlw
Loading commit data...
tests-uint32.mlw
Loading commit data...
