Skip to content

GitLab

why3
why3
Commit 2e3c6fa7 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

headers (pour faire plaisir a Andrei)

parent d4db3bf7
Hide whitespace changes
Inline Side-by-side
Showing with 150 additions and 0 deletions
lib/loc.ml
View file @ 2e3c6fa7
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
let join (b,_) (_,e) = (b,e)
......
lib/loc.mli
View file @ 2e3c6fa7
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
......
lib/util.ml
View file @ 2e3c6fa7
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
let map_fold_left f acc l =
let acc, rev =
......
lib/util.mli
View file @ 2e3c6fa7
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
val map_fold_left :
('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
src/lexer.mli
View file @ 2e3c6fa7
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
type error
......
src/lexer.mll
View file @ 2e3c6fa7
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
{
open Format
......
src/parser.mly
View file @ 2e3c6fa7
/**************************************************************************/
/* */
/* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, */
/* Johannes Kanig and Andrei Paskevich. */
/* */
/* This software is free software; you can redistribute it and/or */
/* modify it under the terms of the GNU Library General Public */
/* License version 2.1, with the special exception on linking */
/* described in file LICENSE. */
/* */
/* This software is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. */
/* */
/**************************************************************************/
%{
......
src/ptree.mli
View file @ 2e3c6fa7
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(*s Parse trees. *)
......
src/typing.ml
View file @ 2e3c6fa7
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Util
open Format
......
src/typing.mli
View file @ 2e3c6fa7
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Term
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment