| task option dans task |
|
More...
|
about 14 years ago
|
| parsing des annotations dans les programmes |
|
More...
|
about 14 years ago
|
| put the proposed interface for transformations into Task.Tr |
|
More...
|
about 14 years ago
|
| "I want to believe" commit. |
|
More...
|
about 14 years ago
|
| ajout de la transformation split_to_cnf qui met en une forme presque cnf. Une CNF où on garde la position des négations et implications. L'interet est au moins pour la visualisation. On retrouve (normalement) une cnf simplement en poussant les négations. |
|
More...
|
about 14 years ago
|
| add Task -- so far, without create_task or split_goal |
|
More...
|
about 14 years ago
|
| add Theory2 to take place of Theory later |
|
More...
|
about 14 years ago
|
| ajout de output-dir, output-file, stdin, stdout |
|
More...
|
about 14 years ago
|
| Simplifie et complète le code pour pouvoir selectionner plusieurs buts sur la ligne de commande |
|
More...
|
about 14 years ago
|
| alt-ergo.ml : decl_type avec arguments main.ml : possibilité de mettre specifier plusieurs theories ou buts split_goals : ajout d'un argument supplémentaire pour ne selectionner que certains buts. |
|
More...
|
about 14 years ago
|
| Theory : Correction de l'exception renvoyé quand une théorie n'est pas trouvé par la fonction retrieve. |
|
More...
|
about 14 years ago
|
| Start the separation of contexts and tasks. |
|
More...
|
about 14 years ago
|
| ajout de l'option print_debug |
|
More...
|
about 14 years ago
|
| driver utilise maintenant en interne des context list Transform.t dans les drivers il n'y a qu'une seul liste de transformations |
|
More...
|
about 14 years ago
|
| - make the interface to ls_defn more straightforward - assure generation of new variables on create_ls_defn |
|
More...
|
about 14 years ago
|
| dynlink_compat : en faisant un vrai test de ocaml 3.11 ou superieur |
|
More...
|
about 14 years ago
|
| minor |
|
More...
|
about 14 years ago
|
| use Driver instructions in Why3 |
|
More...
|
about 14 years ago
|
| move find_ts/find_ls/find_pr functions to Theory, provide ns_find_prop and ns_find_fmla for convenience |
|
More...
|
about 14 years ago
|
| stock prop*fmla in namespaces, necessary if we want to use proposition names as propositional variables |
|
More...
|
about 14 years ago
|
| Ajoiut des context list t dans transform |
|
More...
|
about 14 years ago
|
| introduce suitable combinators for the expr type |
|
More...
|
about 14 years ago
|
| "Please, don't shoot, I can explain everything" commit |
|
More...
|
about 14 years ago
|
| message informatif quand is_native n'est pas défini |
|
More...
|
about 14 years ago
|
| oups pardon on revert correctement |
|
More...
|
about 14 years ago
|
| pour ocaml 3.10 pour le dynlink |
|
More...
|
about 14 years ago
|
| parameters of logic fun were not forgotten by alt-ergo printer |
|
More...
|
about 14 years ago
|
| alt-ergo driver adjusments; |
|
More...
|
about 14 years ago
|
| propagate the driver parameter across Why3 |
|
More...
|
about 14 years ago
|
| check inductive definitions |
|
More...
|
about 14 years ago
|
