diff options
| author | herbelin | 2003-04-09 10:44:09 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-09 10:44:09 +0000 |
| commit | 326a261ee30daa035716908fa0b89e1cfe056c14 (patch) | |
| tree | 72632a35f05a3d48ebdae97e332692d00401e660 | |
| parent | d434ab34709e0ce40f049d709332800d9a96bcc5 (diff) | |
Réorganisation de Impargs + mise en place d'une infrastructure
(notatemment des tables de parsing et d'affichage différenciées)
permettant au traducteur de changer les implicites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3875 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 5bd871bc9b..ed69806578 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -73,12 +73,13 @@ let implicit_args_to_ast_list sp mipv = let ast_list = ref [] in (Array.iteri (fun i mip -> - let imps = inductive_implicits_list(sp, i) in + let imps = implicits_of_global (IndRef (sp, i)) in (ast_list := implicit_args_id_to_ast_list mip.mind_typename imps !ast_list; Array.iteri (fun j idc -> - let impls = constructor_implicits_list ((sp,i), succ j) in + let impls = implicits_of_global + (ConstructRef ((sp,i),j+1)) in ast_list := implicit_args_id_to_ast_list idc impls !ast_list) mip.mind_consnames)) @@ -167,7 +168,7 @@ let constant_to_ast_list kn = let cb = Global.lookup_constant kn in let c = cb.const_body in let typ = cb.const_type in - let l = constant_implicits_list kn in + let l = implicits_of_global (ConstRef kn) in (match c with None -> make_variable_ast (id_of_label (label kn)) typ l @@ -176,7 +177,7 @@ let constant_to_ast_list kn = let variable_to_ast_list sp = let (id, c, v) = get_variable sp in - let l = implicits_of_var sp in + let l = implicits_of_global (VarRef sp) in (match c with None -> make_variable_ast id v l |