Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
c546d1ff
Commit
c546d1ff
authored
Feb 24, 2010
by
Jean-Christophe Filliâtre
Browse files
headers
parent
5494f677
Changes
19
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
c546d1ff
##########################################################################
# #
# Copyright (C) Francois Bobot, Jean-Christophe Filliatre, #
# Johannes Kanig and Andrei Paskevich. #
# Copyright (C) 2010- #
# Francois Bobot #
# Jean-Christophe Filliatre #
# Johannes Kanig #
# Andrei Paskevich #
# #
# This software is free software; you can redistribute it and/or #
# modify it under the terms of the GNU Library General Public #
...
...
configure.in
View file @
c546d1ff
##########################################################################
# #
# Copyright (C) Francois Bobot, Jean-Christophe Filliatre, #
# Johannes Kanig and Andrei Paskevich. #
# Copyright (C) 2010- #
# Francois Bobot #
# Jean-Christophe Filliatre #
# Johannes Kanig #
# Andrei Paskevich #
# #
# This software is free software; you can redistribute it and/or #
# modify it under the terms of the GNU Library General Public #
...
...
src/env.ml
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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
open
Pp
...
...
src/env.mli
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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
Ty
open
Term
...
...
src/lexer.mli
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/lexer.mll
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/main.ml
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/name.ml
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/name.mli
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/parser.mly
View file @
c546d1ff
/**************************************************************************/
/*
*/
/*
Copyright
(
C
)
Francois
Bobot
,
Jean
-
Christophe
Filliatre
,
*/
/*
Johannes
Kanig
and
Andrei
Paskevich
.
*/
/*
Copyright
(
C
)
2010
-
*/
/*
Francois
Bobot
*/
/*
Jean
-
Christophe
Filliatre
*/
/*
Johannes
Kanig
*/
/*
Andrei
Paskevich
*/
/*
*/
/*
This
software
is
free
software
;
you
can
redistribute
it
and
/
or
*/
/*
modify
it
under
the
terms
of
the
GNU
Library
General
Public
*/
...
...
src/pretty.ml
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/pretty.mli
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/ptree.mli
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/term.ml
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/term.mli
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/ty.ml
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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
...
...
src/ty.mli
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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. *)
(* *)
(**************************************************************************)
(** Types *)
...
...
src/typing.ml
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
src/typing.mli
View file @
c546d1ff
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment