GitLab

  in the logic language into (more or less) higher-order style.
  For example,

    logic func (x : int, y : int, 'a list) : (int, 'a) map list

    logic pred (bool, int * real)

  is now written:
    
    logic func (x y : int) (list 'a) : list (map int 'a)

    logic pred bool (int, real)

  Note that types use prefix notation (as in Coq) and the types
  of tuples are now written as (type1, type2, ..., typeN).

- Use the same syntax of type expressions in the program language.

- Allow binders of the form (x y:int) in the program language.
  

programs: the type-checker is back and the bug in vacid_0_sparse_array is now fixed; make bench is back

programs: complete rewrite of the type-checker in progress (in particular, types dterm and dfmla have been moved to Denv, together with some functions); make does not compile whyml anymore; make bench will stop at the first program test; with my apologies if I messed up somewhere...

No commit message

- move exception reporting for Ty, Pattern, Term, and Decl
  to Pretty, as it occasionnaly requires some pretty-printing

bench : ajout d'un bench pour tester tous les provers sur des buts triviaux. Cela peut permettre de détecter un mauvais driver ou printer.

began implementing dynamic dependency graph in hypothesis_selection.ml

alt-ergo : trigger pas sur l'égalité