diff options
| author | herbelin | 1999-12-15 15:24:13 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-15 15:24:13 +0000 |
| commit | d44846131cf2fab2d3c45d435b84d802b1af8d43 (patch) | |
| tree | 20de854b9ba4de7cbd01470559e956451a1d5d8e /parsing/printer.ml | |
| parent | 490c8fa3145e861966dd83f6dc9478b0b96de470 (diff) | |
Nouveaux types 'constructor' et 'inductive' dans Term;
les fonctions sur les inductifs prennent maintenant des 'inductive' en
paramètres; elle n'ont plus besoin de faire des appels dangereux
aux find_m*type qui centralisent la levée de raise Induc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index fcda9fb93e..3920786110 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -38,15 +38,15 @@ let pr_qualified sp id = else [< 'sTR(string_of_path sp) >] -let pr_constant sp = pr_qualified sp (basename sp) +let pr_constant (sp,_) = pr_qualified sp (basename sp) -let pr_existential ev = [< 'sTR ("?" ^ string_of_int ev) >] +let pr_existential (ev,_) = [< 'sTR ("?" ^ string_of_int ev) >] -let pr_inductive (sp,tyi as ind_sp) = +let pr_inductive (sp,tyi as ind_sp,_) = let id = id_of_global (MutInd ind_sp) in pr_qualified sp id -let pr_constructor ((sp,tyi),i as cstr_sp) = +let pr_constructor ((sp,tyi),i as cstr_sp,_) = let id = id_of_global (MutConstruct cstr_sp) in pr_qualified sp id @@ -62,16 +62,16 @@ let globpr k gt = match gt with | Nvar(_,s) -> [< 'sTR s >] | Node(_,"EVAR", (Num (_,ev))::_) -> if !print_arguments then dfltpr gt - else pr_existential ev + else pr_existential (ev,[]) | Node(_,"CONST",(Path(_,sl,s))::_) -> if !print_arguments then dfltpr gt - else pr_constant (section_path sl s) + else pr_constant (section_path sl s,[]) | Node(_,"MUTIND",(Path(_,sl,s))::(Num(_,tyi))::_) -> if !print_arguments then (dfltpr gt) - else pr_inductive (section_path sl s,tyi) + else pr_inductive ((section_path sl s,tyi),[]) | Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) -> if !print_arguments then (dfltpr gt) - else pr_constructor ((section_path sl s,tyi),i) + else pr_constructor (((section_path sl s,tyi),i),[]) | gt -> dfltpr gt let apply_prec = Some (("Term",(9,0,0)),Extend.L) |