diff options
| author | filliatr | 1999-12-03 11:34:33 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-03 11:34:33 +0000 |
| commit | 76b16e44285d06236b9c00e24659138c376d54f3 (patch) | |
| tree | 03bb85046c204828901f26d84e2196c37abaa7f2 /kernel | |
| parent | f20dbafa3e49c35414640e01c3549ad1c802d331 (diff) | |
modules profile, Coqinit et Coqtop (=main)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index a6e878e6b8..5ac91dc00d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -2,7 +2,6 @@ (* $Id$ *) open Pp -open System open Util open Names open Sign @@ -15,7 +14,9 @@ open Abstraction (* The type of environments. *) -type import = string * time_stamp +type checksum = int + +type import = string * checksum type global = Constant | Inductive | Abstraction @@ -217,7 +218,7 @@ let evaluable_constant env k = type compiled_env = { cenv_id : string; - cenv_stamp : time_stamp; + cenv_stamp : checksum; cenv_needed : import list; cenv_constants : (section_path * constant_body) list; cenv_inductives : (section_path * mutual_inductive_body) list; @@ -235,7 +236,7 @@ let exported_objects env = let export env id = let (cst,ind,abs) = exported_objects env in { cenv_id = id; - cenv_stamp = get_time_stamp (); + cenv_stamp = 0; cenv_needed = env.env_globals.env_imports; cenv_constants = cst; cenv_inductives = ind; @@ -246,7 +247,7 @@ let check_imports env needed = let check (id,stamp) = try let actual_stamp = List.assoc id imports in - if compare_time_stamps stamp actual_stamp <> 0 then + if stamp <> actual_stamp then error ("Inconsistent assumptions over module " ^ id) with Not_found -> error ("Reference to unknown module " ^ id) |