diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-03 16:04:21 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-03 16:04:21 +0000 |
| commit | 436ed028434916e58f697593834cbfcc220f8c13 (patch) | |
| tree | 5d2b58e2e91564203ab27229645367ba1666c31c /parsing | |
| parent | 80b8609c3b3aca8ac5b8af145b12956a41ab78f9 (diff) | |
la table PARAMETER n'existe plus (mergé dans la table CONSTANT)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3369 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/prettyp.ml | 4 | ||||
| -rw-r--r-- | parsing/search.ml | 3 |
2 files changed, 3 insertions, 4 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index efcb5c8af..4621f1bb2 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -313,7 +313,7 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = match (oname,tag) with | (_,"VARIABLE") -> print_section_variable (basename sp) ++ fnl () - | (_,("CONSTANT"|"PARAMETER")) -> + | (_,"CONSTANT") -> print_constant with_values sep kn ++ fnl () | (_,"INDUCTIVE") -> print_inductive kn ++ fnl () @@ -504,7 +504,7 @@ let print_local_context () = and print_last_const = function | (oname,Lib.Leaf lobj)::rest -> (match object_tag lobj with - | "CONSTANT" | "PARAMETER" -> + | "CONSTANT" -> let kn = snd oname in let {const_body=val_0;const_type=typ} = Global.lookup_constant kn in diff --git a/parsing/search.ml b/parsing/search.ml index c771a7737..c1e897fd0 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -58,8 +58,7 @@ let crible (fn : global_reference -> env -> constr -> unit) ref = let (idc,_,typ) = get_variable (basename sp) in if (head_const typ) = const then fn (VarRef idc) env typ with Not_found -> (* we are in a section *) ()) - | "CONSTANT" - | "PARAMETER" -> + | "CONSTANT" -> let kn=locate_constant (qualid_of_sp sp) in let {const_type=typ} = Global.lookup_constant kn in if (head_const typ) = const then fn (ConstRef kn) env typ |