Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
595cb370
Commit
595cb370
authored
Jul 01, 2011
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fix frame in headers (sed is the best girl's friend)
parent
ba8bd4b5
Changes
190
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
190 changed files
with
577 additions
and
569 deletions
+577
-569
Makefile.in
Makefile.in
+4
-4
configure.in
configure.in
+3
-3
misc/headache.sh
misc/headache.sh
+8
-0
misc/header.txt
misc/header.txt
+3
-3
src/bench/bench.ml
src/bench/bench.ml
+3
-3
src/bench/bench.mli
src/bench/bench.mli
+3
-3
src/bench/benchdb.ml
src/bench/benchdb.ml
+3
-3
src/bench/benchdb.mli
src/bench/benchdb.mli
+3
-3
src/bench/benchrc.ml
src/bench/benchrc.ml
+3
-3
src/bench/benchrc.mli
src/bench/benchrc.mli
+3
-3
src/bench/whybench.ml
src/bench/whybench.ml
+3
-3
src/config/whyconfig.ml
src/config/whyconfig.ml
+3
-3
src/coq-plugin/g_whytac.ml4
src/coq-plugin/g_whytac.ml4
+3
-3
src/coq-plugin/whytac.ml
src/coq-plugin/whytac.ml
+3
-3
src/core/decl.ml
src/core/decl.ml
+3
-3
src/core/decl.mli
src/core/decl.mli
+3
-3
src/core/env.ml
src/core/env.ml
+3
-3
src/core/env.mli
src/core/env.mli
+3
-3
src/core/ident.ml
src/core/ident.ml
+3
-3
src/core/ident.mli
src/core/ident.mli
+3
-3
src/core/pattern.ml
src/core/pattern.ml
+3
-3
src/core/pattern.mli
src/core/pattern.mli
+3
-3
src/core/pretty.ml
src/core/pretty.ml
+3
-3
src/core/pretty.mli
src/core/pretty.mli
+3
-3
src/core/printer.ml
src/core/printer.ml
+3
-3
src/core/printer.mli
src/core/printer.mli
+3
-3
src/core/task.ml
src/core/task.ml
+3
-3
src/core/task.mli
src/core/task.mli
+3
-3
src/core/term.ml
src/core/term.ml
+3
-3
src/core/term.mli
src/core/term.mli
+3
-3
src/core/theory.ml
src/core/theory.ml
+3
-3
src/core/theory.mli
src/core/theory.mli
+3
-3
src/core/trans.ml
src/core/trans.ml
+3
-3
src/core/trans.mli
src/core/trans.mli
+3
-3
src/core/ty.ml
src/core/ty.ml
+3
-3
src/core/ty.mli
src/core/ty.mli
+3
-3
src/driver/autodetection.ml
src/driver/autodetection.ml
+3
-3
src/driver/autodetection.mli
src/driver/autodetection.mli
+3
-3
src/driver/call_provers.ml
src/driver/call_provers.ml
+3
-3
src/driver/call_provers.mli
src/driver/call_provers.mli
+3
-3
src/driver/driver.ml
src/driver/driver.ml
+3
-3
src/driver/driver.mli
src/driver/driver.mli
+3
-3
src/driver/driver_ast.ml
src/driver/driver_ast.ml
+3
-3
src/driver/driver_lexer.mll
src/driver/driver_lexer.mll
+3
-3
src/driver/driver_parser.mly
src/driver/driver_parser.mly
+3
-3
src/driver/whyconf.ml
src/driver/whyconf.ml
+3
-3
src/driver/whyconf.mli
src/driver/whyconf.mli
+3
-3
src/ide/db.ml
src/ide/db.ml
+3
-3
src/ide/db.mli
src/ide/db.mli
+3
-3
src/ide/gconfig.ml
src/ide/gconfig.ml
+3
-3
src/ide/gconfig.mli
src/ide/gconfig.mli
+3
-3
src/ide/newmain.ml
src/ide/newmain.ml
+3
-3
src/ide/replay.ml
src/ide/replay.ml
+3
-3
src/ide/session.ml
src/ide/session.ml
+3
-3
src/ide/session.mli
src/ide/session.mli
+3
-3
src/ide/termcode.ml
src/ide/termcode.ml
+3
-3
src/ide/termcode.mli
src/ide/termcode.mli
+3
-3
src/ide/worker.ml
src/ide/worker.ml
+3
-3
src/ide/xml.mli
src/ide/xml.mli
+3
-3
src/ide/xml.mll
src/ide/xml.mll
+3
-3
src/main.ml
src/main.ml
+3
-3
src/parser/denv.ml
src/parser/denv.ml
+3
-3
src/parser/denv.mli
src/parser/denv.mli
+3
-3
src/parser/lexer.mli
src/parser/lexer.mli
+3
-3
src/parser/lexer.mll
src/parser/lexer.mll
+3
-3
src/parser/parser.mly
src/parser/parser.mly
+3
-3
src/parser/ptree.ml
src/parser/ptree.ml
+3
-3
src/parser/typing.ml
src/parser/typing.ml
+3
-3
src/parser/typing.mli
src/parser/typing.mli
+3
-3
src/printer/alt_ergo.ml
src/printer/alt_ergo.ml
+3
-3
src/printer/alt_ergo.mli
src/printer/alt_ergo.mli
+3
-3
src/printer/coq.ml
src/printer/coq.ml
+3
-3
src/printer/cvc3.ml
src/printer/cvc3.ml
+3
-3
src/printer/gappa.ml
src/printer/gappa.ml
+3
-3
src/printer/print_real.ml
src/printer/print_real.ml
+3
-3
src/printer/print_real.mli
src/printer/print_real.mli
+3
-3
src/printer/simplify.ml
src/printer/simplify.ml
+3
-3
src/printer/smt.ml
src/printer/smt.ml
+3
-3
src/printer/smt.mli
src/printer/smt.mli
+3
-3
src/printer/smt2.ml
src/printer/smt2.ml
+3
-3
src/printer/tptp.ml
src/printer/tptp.ml
+3
-3
src/printer/tptp.mli
src/printer/tptp.mli
+3
-3
src/printer/why3.ml
src/printer/why3.ml
+3
-3
src/printer/why3.mli
src/printer/why3.mli
+3
-3
src/programs/pgm_effect.ml
src/programs/pgm_effect.ml
+3
-3
src/programs/pgm_effect.mli
src/programs/pgm_effect.mli
+3
-3
src/programs/pgm_env.ml
src/programs/pgm_env.ml
+3
-3
src/programs/pgm_env.mli
src/programs/pgm_env.mli
+3
-3
src/programs/pgm_fastwp.ml
src/programs/pgm_fastwp.ml
+3
-3
src/programs/pgm_main.ml
src/programs/pgm_main.ml
+3
-3
src/programs/pgm_module.ml
src/programs/pgm_module.ml
+3
-3
src/programs/pgm_module.mli
src/programs/pgm_module.mli
+3
-3
src/programs/pgm_pretty.ml
src/programs/pgm_pretty.ml
+3
-3
src/programs/pgm_pretty.mli
src/programs/pgm_pretty.mli
+3
-3
src/programs/pgm_ttree.ml
src/programs/pgm_ttree.ml
+3
-3
src/programs/pgm_types.ml
src/programs/pgm_types.ml
+3
-3
src/programs/pgm_types.mli
src/programs/pgm_types.mli
+3
-3
src/programs/pgm_typing.ml
src/programs/pgm_typing.ml
+3
-3
src/programs/pgm_typing.mli
src/programs/pgm_typing.mli
+3
-3
src/programs/pgm_wp.ml
src/programs/pgm_wp.ml
+3
-3
src/programs/pgm_wp.mli
src/programs/pgm_wp.mli
+3
-3
src/tools/cpulimit.c
src/tools/cpulimit.c
+3
-3
src/tptp2why/tptp2whymain.ml
src/tptp2why/tptp2whymain.ml
+3
-3
src/tptp2why/tptpLexer.mll
src/tptp2why/tptpLexer.mll
+3
-3
src/tptp2why/tptpParser.mly
src/tptp2why/tptpParser.mly
+3
-3
src/tptp2why/tptpTranslate.ml
src/tptp2why/tptpTranslate.ml
+3
-3
src/tptp2why/tptpTranslate.mli
src/tptp2why/tptpTranslate.mli
+3
-3
src/tptp2why/tptpTree.ml
src/tptp2why/tptpTree.ml
+3
-3
src/transform/abstraction.ml
src/transform/abstraction.ml
+3
-3
src/transform/abstraction.mli
src/transform/abstraction.mli
+3
-3
src/transform/close_epsilon.ml
src/transform/close_epsilon.ml
+3
-3
src/transform/close_epsilon.mli
src/transform/close_epsilon.mli
+3
-3
src/transform/discriminate.ml
src/transform/discriminate.ml
+3
-3
src/transform/discriminate.mli
src/transform/discriminate.mli
+3
-3
src/transform/eliminate_algebraic.ml
src/transform/eliminate_algebraic.ml
+3
-3
src/transform/eliminate_algebraic.mli
src/transform/eliminate_algebraic.mli
+3
-3
src/transform/eliminate_definition.ml
src/transform/eliminate_definition.ml
+3
-3
src/transform/eliminate_definition.mli
src/transform/eliminate_definition.mli
+3
-3
src/transform/eliminate_if.ml
src/transform/eliminate_if.ml
+3
-3
src/transform/eliminate_if.mli
src/transform/eliminate_if.mli
+3
-3
src/transform/eliminate_inductive.ml
src/transform/eliminate_inductive.ml
+3
-3
src/transform/eliminate_inductive.mli
src/transform/eliminate_inductive.mli
+3
-3
src/transform/eliminate_let.ml
src/transform/eliminate_let.ml
+3
-3
src/transform/eliminate_let.mli
src/transform/eliminate_let.mli
+3
-3
src/transform/encoding.ml
src/transform/encoding.ml
+3
-3
src/transform/encoding.mli
src/transform/encoding.mli
+3
-3
src/transform/encoding_bridge.ml
src/transform/encoding_bridge.ml
+3
-3
src/transform/encoding_bridge.mli
src/transform/encoding_bridge.mli
+3
-3
src/transform/encoding_decorate.ml
src/transform/encoding_decorate.ml
+3
-3
src/transform/encoding_decorate.mli
src/transform/encoding_decorate.mli
+3
-3
src/transform/encoding_explicit.ml
src/transform/encoding_explicit.ml
+3
-3
src/transform/encoding_explicit.mli
src/transform/encoding_explicit.mli
+3
-3
src/transform/encoding_guard.ml
src/transform/encoding_guard.ml
+3
-3
src/transform/encoding_instantiate.ml
src/transform/encoding_instantiate.ml
+3
-3
src/transform/encoding_instantiate.mli
src/transform/encoding_instantiate.mli
+3
-3
src/transform/encoding_select.ml
src/transform/encoding_select.ml
+3
-3
src/transform/encoding_select.mli
src/transform/encoding_select.mli
+3
-3
src/transform/encoding_sort.ml
src/transform/encoding_sort.ml
+3
-3
src/transform/encoding_twin.ml
src/transform/encoding_twin.ml
+3
-3
src/transform/encoding_twin.mli
src/transform/encoding_twin.mli
+3
-3
src/transform/eval_match.ml
src/transform/eval_match.ml
+3
-3
src/transform/eval_match.mli
src/transform/eval_match.mli
+3
-3
src/transform/filter_trigger.ml
src/transform/filter_trigger.ml
+3
-3
src/transform/hypothesis_selection.ml
src/transform/hypothesis_selection.ml
+3
-3
src/transform/inlining.ml
src/transform/inlining.ml
+3
-3
src/transform/inlining.mli
src/transform/inlining.mli
+3
-3
src/transform/introduction.ml
src/transform/introduction.ml
+4
-4
src/transform/introduction.mli
src/transform/introduction.mli
+3
-3
src/transform/libencoding.ml
src/transform/libencoding.ml
+3
-3
src/transform/libencoding.mli
src/transform/libencoding.mli
+3
-3
src/transform/lift_epsilon.ml
src/transform/lift_epsilon.ml
+3
-3
src/transform/lift_epsilon.mli
src/transform/lift_epsilon.mli
+3
-3
src/transform/protect_enumeration.ml
src/transform/protect_enumeration.ml
+3
-3
src/transform/protect_enumeration.mli
src/transform/protect_enumeration.mli
+3
-3
src/transform/simplify_array.ml
src/transform/simplify_array.ml
+3
-3
src/transform/simplify_formula.ml
src/transform/simplify_formula.ml
+3
-3
src/transform/simplify_formula.mli
src/transform/simplify_formula.mli
+3
-3
src/transform/simplify_recursive_definition.ml
src/transform/simplify_recursive_definition.ml
+3
-3
src/transform/simplify_recursive_definition.mli
src/transform/simplify_recursive_definition.mli
+3
-3
src/transform/split_goal.ml
src/transform/split_goal.ml
+3
-3
src/transform/split_goal.mli
src/transform/split_goal.mli
+3
-3
src/util/cmdline.ml
src/util/cmdline.ml
+3
-3
src/util/cmdline.mli
src/util/cmdline.mli
+3
-3
src/util/debug.ml
src/util/debug.ml
+3
-3
src/util/debug.mli
src/util/debug.mli
+3
-3
src/util/exn_printer.ml
src/util/exn_printer.ml
+3
-3
src/util/exn_printer.mli
src/util/exn_printer.mli
+3
-3
src/util/hashcons.ml
src/util/hashcons.ml
+3
-3
src/util/hashcons.mli
src/util/hashcons.mli
+3
-3
src/util/hashweak.ml
src/util/hashweak.ml
+3
-3
src/util/hashweak.mli
src/util/hashweak.mli
+3
-3
src/util/loc.ml
src/util/loc.ml
+3
-3
src/util/loc.mli
src/util/loc.mli
+3
-3
src/util/plugin.ml
src/util/plugin.ml
+3
-3
src/util/plugin.mli
src/util/plugin.mli
+3
-3
src/util/pp.ml
src/util/pp.ml
+3
-3
src/util/pp.mli
src/util/pp.mli
+3
-3
src/util/print_tree.ml
src/util/print_tree.ml
+3
-3
src/util/print_tree.mli
src/util/print_tree.mli
+3
-3
src/util/rc.mli
src/util/rc.mli
+3
-3
src/util/rc.mll
src/util/rc.mll
+3
-3
src/util/sysutil.ml
src/util/sysutil.ml
+3
-3
src/util/sysutil.mli
src/util/sysutil.mli
+3
-3
src/util/util.ml
src/util/util.ml
+3
-3
src/util/util.mli
src/util/util.mli
+3
-3
src/why.ml
src/why.ml
+3
-3
src/why3doc/doc_html.ml
src/why3doc/doc_html.ml
+3
-3
src/why3doc/doc_html.mli
src/why3doc/doc_html.mli
+3
-3
src/why3doc/doc_main.ml
src/why3doc/doc_main.ml
+3
-3
src/why3doc/to_html.mll
src/why3doc/to_html.mll
+3
-3
No files found.
Makefile.in
View file @
595cb370
##########################################################################
# #
# Copyright (C) 2010-2011 #
# François Bobot #
# Jean-Christophe Filliâtre #
# Claude Marché #
# François Bobot
#
# Jean-Christophe Filliâtre
#
# Claude Marché
#
# Andrei Paskevich #
# #
# This software is free software; you can redistribute it and/or #
...
...
@@ -1153,7 +1153,7 @@ $(DISTRIB_TAR): doc/manual.pdf
###############
headers
:
headache
-c
misc/headache_config.txt
-h
misc/header.txt
\
misc/headache.sh
\
Makefile.in configure.in src/
*
.ml
*
src/
*
/
*
.ml
*
\
src/tools/cpulimit.c
...
...
configure.in
View file @
595cb370
##########################################################################
# #
# Copyright (C) 2010-2011 #
# François Bobot #
# Jean-Christophe Filliâtre #
# Claude Marché #
# François Bobot
#
# Jean-Christophe Filliâtre
#
# Claude Marché
#
# Andrei Paskevich #
# #
# This software is free software; you can redistribute it and/or #
...
...
misc/headache.sh
0 → 100755
View file @
595cb370
#!/bin/sh
headache
-c
misc/headache_config.txt
-h
misc/header.txt
"
$@
"
sed
-i
-e
'
s/Francois Bobot/François Bobot/g;
s/Jean-Christophe Filliatre/Jean-Christophe Filliâtre/g;
s/Claude Marche/Claude Marché/g'
--
"
$@
"
misc/header.txt
View file @
595cb370
Copyright (C) 2010-2011
Fran
ç
ois Bobot
Jean-Christophe Filli
â
tre
Claude March
é
Fran
c
ois Bobot
Jean-Christophe Filli
a
tre
Claude March
e
Andrei Paskevich
This software is free software; you can redistribute it and/or
...
...
src/bench/bench.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/bench/bench.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/bench/benchdb.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/bench/benchdb.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/bench/benchrc.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/bench/benchrc.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/bench/whybench.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/config/whyconfig.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/coq-plugin/g_whytac.ml4
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/coq-plugin/whytac.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/decl.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/decl.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/env.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/env.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/ident.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/ident.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/pattern.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/pattern.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/pretty.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/pretty.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/printer.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/printer.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/task.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/task.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/term.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/term.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/theory.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/theory.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/trans.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/trans.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/ty.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/core/ty.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/driver/autodetection.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/driver/autodetection.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/driver/call_provers.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/driver/call_provers.mli
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
...
...
src/driver/driver.ml
View file @
595cb370
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* François Bobot
*)
(* Jean-Christophe Filliâtre
*)
(* Claude Marché
*)
(* Andrei Paskevich *)