diff options
Diffstat (limited to 'parsing/termast.ml')
| -rw-r--r-- | parsing/termast.ml | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml index f7c1a88d1c..7025bfde44 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -54,18 +54,6 @@ let with_coercions f = with_option print_coercions f (**********************************************************************) (* conversion of references *) -(* -let ids_of_rctxt ctxt = - Array.to_list - (Array.map - (function - | RRef (_,RVar id) -> id - | _ -> - error - "Termast: arbitrary substitution of references not yet implemented") - ctxt) -*) - let ids_of_ctxt ctxt = Array.to_list (Array.map @@ -116,6 +104,10 @@ let ast_of_ref pr r = | VarRef sp -> ast_of_ident (basename sp) | EvarRef ev -> ast_of_existential_ref pr (ev,ctxt) +let ast_of_qualid p = + let dir, s = repr_qualid p in + let args = List.map nvar (dir@[s]) in + ope ("QUALID", args) (**********************************************************************) (* conversion of patterns *) |