← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/dp/fol.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/dp/fol.mli
 
1
 
 
2
(* Polymorphic First-Order Logic (that is Why's input logic) *)
 
3
 
 
4
type typ = 
 
5
  | Tvar of string
 
6
  | Tid of string * typ list
 
7
 
 
8
type term =   
 
9
  | Cst of int
 
10
  | Plus of term * term
 
11
  | Moins of term * term
 
12
  | Mult of term * term
 
13
  | Div of term * term
 
14
  | App of string * term list
 
15
 
 
16
and atom =   
 
17
  | Eq of term * term
 
18
  | Le of term * term
 
19
  | Lt of term * term
 
20
  | Ge of term * term
 
21
  | Gt of term * term
 
22
  | Pred of string * term list
 
23
 
 
24
and form = 
 
25
  | Fatom of atom
 
26
  | Imp of form * form
 
27
  | Iff of form * form
 
28
  | And of form * form
 
29
  | Or of form * form
 
30
  | Not of form
 
31
  | Forall of string * typ * form
 
32
  | Exists of string * typ * form
 
33
  | True
 
34
  | False
 
35
 
 
36
(* the integer indicates the number of type variables *)
 
37
type decl =
 
38
  | DeclType of string * int
 
39
  | DeclFun of string * int * typ list * typ
 
40
  | DeclPred of string * int * typ list
 
41
  | Axiom of string * form
 
42
 
 
43
type query = decl list * form
 
44
 
 
45
 
 
46
(* prover result *)
 
47
 
 
48
type prover_answer = 
 
49
  | Valid of string option 
 
50
  | Invalid
 
51
  | DontKnow
 
52
  | Timeout
 
53
  | NoAnswer
 
54
  | Failure of string
 
55