← Back to branch summary

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

« back to all changes in this revision

Viewing changes to kernel/safe_typing.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:
kernel/safe_typing.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: safe_typing.mli 10664 2008-03-14 11:27:37Z soubiran $ i*)
 
10
 
 
11
(*i*)
 
12
open Names
 
13
open Term
 
14
open Declarations
 
15
open Entries
 
16
(*i*)
 
17
 
 
18
(*s Safe environments. Since we are now able to type terms, we can
 
19
  define an abstract type of safe environments, where objects are
 
20
  typed before being added.
 
21
 
 
22
  We also add [open_structure] and [close_section], [close_module] to
 
23
  provide functionnality for sections and interactive modules 
 
24
*)
 
25
 
 
26
type safe_environment
 
27
 
 
28
val env_of_safe_env : safe_environment -> Environ.env
 
29
 
 
30
val empty_environment : safe_environment
 
31
val is_empty : safe_environment -> bool
 
32
 
 
33
(* Adding and removing local declarations (Local or Variables) *)
 
34
val push_named_assum :
 
35
  identifier * types -> safe_environment ->
 
36
    Univ.constraints * safe_environment
 
37
val push_named_def :
 
38
  identifier * constr * types option -> safe_environment ->
 
39
    Univ.constraints * safe_environment
 
40
 
 
41
(* Adding global axioms or definitions *)
 
42
type global_declaration = 
 
43
  | ConstantEntry of constant_entry
 
44
  | GlobalRecipe of Cooking.recipe
 
45
 
 
46
val add_constant : 
 
47
  dir_path -> label -> global_declaration -> safe_environment -> 
 
48
      constant * safe_environment
 
49
 
 
50
(* Adding an inductive type *)
 
51
val add_mind : 
 
52
  dir_path -> label -> mutual_inductive_entry -> safe_environment ->
 
53
    mutual_inductive * safe_environment
 
54
 
 
55
(* Adding a module *)
 
56
val add_module :
 
57
  label -> module_entry -> safe_environment 
 
58
    -> module_path * safe_environment
 
59
 
 
60
(* Adding a module alias*)
 
61
val add_alias :
 
62
  label -> module_path -> safe_environment 
 
63
    -> module_path * safe_environment
 
64
(* Adding a module type *)
 
65
val add_modtype :
 
66
  label -> module_struct_entry -> safe_environment 
 
67
    -> module_path * safe_environment
 
68
 
 
69
(* Adding universe constraints *)
 
70
val add_constraints : 
 
71
  Univ.constraints -> safe_environment -> safe_environment
 
72
 
 
73
(* Settin the strongly constructive or classical logical engagement *)
 
74
val set_engagement : engagement -> safe_environment -> safe_environment
 
75
 
 
76
 
 
77
(*s Interactive module functions *)
 
78
val start_module : 
 
79
  label -> safe_environment -> module_path * safe_environment
 
80
val end_module :
 
81
  label -> module_struct_entry option 
 
82
      -> safe_environment -> module_path * safe_environment 
 
83
 
 
84
val add_module_parameter :
 
85
  mod_bound_id -> module_struct_entry -> safe_environment -> safe_environment
 
86
 
 
87
val start_modtype :
 
88
  label -> safe_environment -> module_path * safe_environment
 
89
 
 
90
val end_modtype :
 
91
  label -> safe_environment -> module_path * safe_environment
 
92
 
 
93
val add_include :
 
94
  module_struct_entry -> safe_environment -> safe_environment
 
95
 
 
96
val current_modpath : safe_environment -> module_path
 
97
val current_msid : safe_environment -> mod_self_id
 
98
 
 
99
 
 
100
(* Loading and saving compilation units *)
 
101
 
 
102
(* exporting and importing modules *)
 
103
type compiled_library
 
104
 
 
105
val start_library : dir_path -> safe_environment 
 
106
      -> module_path * safe_environment
 
107
 
 
108
val export : safe_environment -> dir_path  
 
109
      -> mod_self_id * compiled_library
 
110
 
 
111
val import : compiled_library -> Digest.t -> safe_environment 
 
112
      -> module_path * safe_environment
 
113
 
 
114
(* Remove the body of opaque constants *)
 
115
 
 
116
val lighten_library : compiled_library -> compiled_library
 
117
 
 
118
(*s Typing judgments *)
 
119
 
 
120
type judgment
 
121
 
 
122
val j_val : judgment -> constr
 
123
val j_type : judgment -> constr
 
124
 
 
125
(* Safe typing of a term returning a typing judgment and universe
 
126
   constraints to be added to the environment for the judgment to
 
127
   hold. It is guaranteed that the constraints are satisfiable
 
128
 *)
 
129
val safe_infer : safe_environment -> constr -> judgment * Univ.constraints
 
130
 
 
131
val typing : safe_environment -> constr -> judgment
 
132
 
 
133
 
 
134
 
 
135
(*spiwack: safe retroknowledge functionalities *)
 
136
 
 
137
open Retroknowledge
 
138
 
 
139
val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
 
140
 
 
141
val register : safe_environment -> field -> Retroknowledge.entry -> constr
 
142
                                         -> safe_environment