diff options
| author | herbelin | 2000-03-31 12:53:55 +0000 |
|---|---|---|
| committer | herbelin | 2000-03-31 12:53:55 +0000 |
| commit | e6c8c552cff89a45e696261aec441bf690a3e963 (patch) | |
| tree | 7172d2919f2d1ebb2f3f2214ba6bcaa092a428aa /toplevel | |
| parent | e65106b4799afd27eb1aecf6d2d42b098fe7ec89 (diff) | |
Portage (pour la forme) de minicoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@360 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/fhimsg.ml | 2 | ||||
| -rw-r--r-- | toplevel/minicoq.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index 419488a37b..45a922d7f1 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -53,7 +53,7 @@ module Make = functor (P : Printer) -> struct [< sign_env; db_env >] let pr_ne_ctx header k = function - | ENVIRON (([],[]),[]) -> [< >] + | ENVIRON (s1,s2) when s1=nil_sign & s2=nil_dbsign -> [< >] | env -> [< header; pr_env k env >] diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index a5e421feda..7af018585a 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -23,7 +23,7 @@ let lookup_var id = in look 1 -let args sign = Array.of_list (List.map (fun id -> VAR id) (fst sign)) +let args sign = Array.of_list (List.map (fun id -> VAR id) (ids_of_sign sign)) let rec globalize bv = function | VAR id -> lookup_var id bv @@ -51,7 +51,7 @@ let check c = let definition id ty c = let c = globalize [] c in let ty = option_app (globalize []) ty in - let ce = { const_entry_body = c; const_entry_type = ty } in + let ce = { const_entry_body = Cooked c; const_entry_type = ty } in let sp = make_path [] id CCI in env := add_constant sp ce !env; mSGNL (hOV 0 [< print_id id; 'sPC; 'sTR"is defined"; 'fNL >]) |