diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 11:41:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 11:41:58 +0000 |
| commit | f3e237894067f3d3548d6cba5a64c2b8193a88d3 (patch) | |
| tree | a53be7ef3cb3dfccabade87c53889faaa6dd5535 /parsing/termast.ml | |
| parent | eb6d5b6acaca83d13063f0d7fc414b4dbee6572e (diff) | |
Changement de représentation du contexte des réf dans rawconstr et pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@377 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/termast.ml')
| -rw-r--r-- | parsing/termast.ml | 10 |
1 files changed, 6 insertions, 4 deletions
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]) (**********************************************************************) |