diff options
| author | filliatr | 2000-07-21 17:31:35 +0000 |
|---|---|---|
| committer | filliatr | 2000-07-21 17:31:35 +0000 |
| commit | ba18968685be05d370bb0a82fc3f5e403cdced9f (patch) | |
| tree | 018cf8f6724fec016715d01851f10b29ab37e8df /kernel | |
| parent | 2a8ac977519aa0c980d2906b60bb8fb258900d28 (diff) | |
retablissement minicoq (pour Jacek)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@565 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 14 |
2 files changed, 4 insertions, 13 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 48692008cb..d4b610a8e8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -463,6 +463,3 @@ let import = import let env_of_safe_env e = e -(*s Machines with information. *) - -type information = Logic | Inf of unsafe_judgment diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 4ed912d4cf..5f6b9b073e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -53,16 +53,17 @@ val import : compiled_env -> safe_environment -> safe_environment val env_of_safe_env : safe_environment -> env -(*i For debug -(*s Typing without information. *) + +(*s Typing judgments (only used in minicoq). *) + type judgment val j_val : judgment -> constr val j_type : judgment -> constr val safe_machine : safe_environment -> constr -> judgment * constraints -val safe_machine_type : safe_environment -> constr -> typed_type * constraints +(*i For debug val fix_machine : safe_environment -> constr -> judgment * constraints val fix_machine_type : safe_environment -> constr -> typed_type * constraints @@ -71,14 +72,7 @@ val unsafe_machine_type : safe_environment -> constr -> typed_type * constraints val type_of : safe_environment -> constr -> constr -(*i obsolète val type_of_type : safe_environment -> constr -> constr val unsafe_type_of : safe_environment -> constr -> constr i*) - -(*s Typing with information (extraction). *) - -type information = Logic | Inf of judgment -i*) - |