| don't clash if the same symbol is reused in namespace |
|
More...
|
over 14 years ago
|
| [no comment] |
|
More...
|
over 14 years ago
|
| fix an invariant violation in the previous commit: the [Duse] declaration are preserved on Context.use_export, so that ctxt_known can be always restored from ctxt_decls. |
|
More...
|
over 14 years ago
|
| refactor theory.ml: |
|
More...
|
over 14 years ago
|
| [no comment] |
|
More...
|
over 14 years ago
|
| typage des predicats inductifs |
|
More...
|
over 14 years ago
|
| typage des predicats inductifs |
|
More...
|
over 14 years ago
|
| typage des predicats inductifs |
|
More...
|
over 14 years ago
|
| deplacement de transform |
|
More...
|
over 14 years ago
|
| add f_open_forall + move around the code in term.ml |
|
More...
|
over 14 years ago
|
| var dans fmla |
|
More...
|
over 14 years ago
|
| l'attaque des clones |
|
More...
|
over 14 years ago
|
| clone_export (en cours) |
|
More...
|
over 14 years ago
|
| Theory.ctxt |
|
More...
|
over 14 years ago
|
| decl_or_use devient decl |
|
More...
|
over 14 years ago
|
| typage des match |
|
More...
|
over 14 years ago
|
| inductive (en cours) |
|
More...
|
over 14 years ago
|
| typage des triggers |
|
More...
|
over 14 years ago
|
| linearite des patterns |
|
More...
|
over 14 years ago
|
| typage du cast |
|
More...
|
over 14 years ago
|
| typage des quantificateurs |
|
More...
|
over 14 years ago
|
| patterns - unfinished |
|
More...
|
over 14 years ago
|
| fix the syntax of quantifiers |
|
More...
|
over 14 years ago
|
| join fsymbol and psymbol into the common lsymbol type |
|
More...
|
over 14 years ago
|
| prefix et infix (cf prelude.why) |
|
More...
|
over 14 years ago
|
| ajout de la trnasformation flatten |
|
More...
|
over 14 years ago
|
| typage de PPnamed |
|
More...
|
over 14 years ago
|
| typage de PPnamed |
|
More...
|
over 14 years ago
|
| typage du let |
|
More...
|
over 14 years ago
|
| ajout dans le main |
|
More...
|
over 14 years ago
|
