diff options
| author | herbelin | 2002-05-14 21:27:10 +0000 |
|---|---|---|
| committer | herbelin | 2002-05-14 21:27:10 +0000 |
| commit | ce67352563f53a82c9cb310bd689f6e75d71edbd (patch) | |
| tree | 6c3b9594657e30441c63d09928c5726aaa1b5df9 /parsing/printer.ml | |
| parent | 5396eb3a05cc609b00645cfb3ee68411edd2de0a (diff) | |
Utilisation d'une construction spéciale SECVAR pour gérer la
globalisation des variables de section (en espérant plus de robustesse
vis à vis des bugs récurrents de Infix pour les variables avec
implicites)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2684 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index af0bcf1b28..dae3423bec 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -34,6 +34,11 @@ let global_const_name sp = with Not_found -> (* May happen in debug *) (str ("CONST("^(string_of_path sp)^")")) +let global_var_name id = + try pr_global (VarRef id) + with Not_found -> (* May happen in debug *) + (str ("SECVAR("^(string_of_id id)^")")) + let global_ind_name (sp,tyi) = try pr_global (IndRef (sp,tyi)) with Not_found -> (* May happen in debug *) @@ -50,6 +55,8 @@ let globpr gt = match gt with | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev))) | Node(_,"CONST",[Path(_,sl)]) -> global_const_name (section_path sl) + | Node(_,"SECVAR",[Nvar(_,s)]) -> + global_var_name s | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) -> global_ind_name (section_path sl, tyi) | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) -> |