From f3e237894067f3d3548d6cba5a64c2b8193a88d3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 28 Apr 2000 11:41:58 +0000 Subject: Changement de représentation du contexte des réf dans rawconstr et pattern MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@377 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/termast.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'parsing/termast.ml') diff --git a/parsing/termast.ml b/parsing/termast.ml index bcdc21f05..3587ba01e 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -50,6 +50,7 @@ let with_coercions f = with_option print_coercions f (**********************************************************************) (* conversion of references *) +(* let ids_of_rctxt ctxt = Array.to_list (Array.map @@ -59,6 +60,7 @@ let ids_of_rctxt ctxt = error "Termast: arbitrary substitution of references not yet implemented") ctxt) +*) let ids_of_ctxt ctxt = Array.to_list @@ -122,14 +124,14 @@ let ast_of_inductive_ref ((sp,tyi) as ind_sp,ids) = let ast_of_inductive (ev,ctxt) = ast_of_inductive_ref (ev,ids_of_ctxt ctxt) let ast_of_ref = function - | RConst (sp,ctxt) -> ast_of_constant_ref (sp,ids_of_rctxt ctxt) + | RConst (sp,ctxt) -> ast_of_constant_ref (sp,ids_of_ctxt ctxt) | RAbst (sp) -> ope("ABST", (path_section dummy_loc sp) ::(List.map ast_of_ident (* on triche *) [])) - | RInd (ind,ctxt) -> ast_of_inductive_ref (ind,ids_of_rctxt ctxt) - | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_rctxt ctxt) + | RInd (ind,ctxt) -> ast_of_inductive_ref (ind,ids_of_ctxt ctxt) + | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_ctxt ctxt) | RVar id -> nvar (string_of_id id) - | REVar (ev,ctxt) -> ast_of_existential_ref (ev,ids_of_rctxt ctxt) + | REVar (ev,ctxt) -> ast_of_existential_ref (ev,ids_of_ctxt ctxt) | RMeta n -> ope("META",[num n]) (**********************************************************************) -- cgit v1.2.3