diff options
author | 2001-08-10 14:42:22 +0000 | |
---|---|---|
committer | 2001-08-10 14:42:22 +0000 | |
commit | 8e92ee787e7d1fd48cae1eccf67a9b05e739743e (patch) | |
tree | b33191fbaba0cad4b14a96cf5d7786dd2c07c3d7 /toplevel/command.ml | |
parent | c0a3b41ad2f2afba3f060e0d4001bd7aceea0831 (diff) |
Parsing
- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
lieu de string)
Table des noms qualifiés
- Remplacement de la table de visibilité par une table qui ne cache
plus les noms de modules et sections mais seulement les noms des
constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
module A déjà existant : seuls les noms de constructions de l'ancien
A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
constantes définies à l'intérieur de sections et simplification
connexes (suppression de END-SECTION, une seule table de noms qui ne
survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
Require and co, tests de cohérence; pour être cohérent avec la non
survie des tables de noms à la sortie des section, les require à
l'intérieur d'une section eux aussi sont refaits à la fermeture de la
section
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r-- | toplevel/command.ml | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 0384ca804..b3a34e2ce 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -28,9 +28,9 @@ open Proof_type open Tacmach let mkCastC(c,t) = ope("CAST",[c;t]) -let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)]) +let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some x,b)]) let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) -let mkProdC (x,a,b) = ope("PROD",[a;slam(Some (string_of_id x),b)]) +let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)]) let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) (* Commands of the interface *) @@ -102,13 +102,13 @@ let syntax_definition ident com = let parameter_def_var ident c = let c = interp_type Evd.empty (Global.env()) c in - let sp = declare_parameter (id_of_string ident) c in - if_verbose message (ident ^ " is assumed"); + let sp = declare_parameter ident c in + if_verbose message ((string_of_id ident) ^ " is assumed"); sp let declare_global_assumption ident c = let sp = parameter_def_var ident c in - wARNING [< 'sTR ident; 'sTR" is declared as a parameter"; + wARNING [< pr_id ident; 'sTR" is declared as a parameter"; 'sTR" because it is at a global level" >]; ConstRef sp @@ -118,11 +118,10 @@ let hypothesis_def_var is_refining ident n c = | DischargeAt disch_sp -> if Lib.is_section_p disch_sp then begin let t = interp_type Evd.empty (Global.env()) c in - let sp = declare_variable (id_of_string ident) - (SectionLocalAssum t,n,false) in - if_verbose message (ident ^ " is assumed"); + let sp = declare_variable ident (SectionLocalAssum t,n,false) in + if_verbose message ((string_of_id ident) ^ " is assumed"); if is_refining then - mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; + mSGERRNL [< 'sTR"Warning: Variable "; pr_id ident; 'sTR" is not visible from current goals" >]; VarRef sp end @@ -437,7 +436,7 @@ let apply_tac_not_declare id pft = function let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const) strength = begin match strength with - | DischargeAt disch_sp when Lib.is_section_p disch_sp -> + | DischargeAt disch_sp when Lib.is_section_p disch_sp (*&& not opacity*) -> let c = constr_of_constr_entry const in let _ = declare_variable id (SectionLocalDef c,strength,opacity) in () | NeverDischarge | DischargeAt _ -> @@ -464,12 +463,12 @@ let check_anonymity id save_ident = let save_anonymous opacity save_ident = let id,(const,strength) = Pfedit.cook_proof () in check_anonymity id save_ident; - save opacity (id_of_string save_ident) const strength + save opacity save_ident const strength let save_anonymous_with_strength strength opacity save_ident = let id,(const,_) = Pfedit.cook_proof () in check_anonymity id save_ident; - save opacity (id_of_string save_ident) const strength + save opacity save_ident const strength let get_current_context () = try Pfedit.get_current_goal_context () |