diff options
Diffstat (limited to 'proofs/proof_trees.ml')
| -rw-r--r-- | proofs/proof_trees.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 8a655b3da2..4a8f8dfc6c 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -389,7 +389,7 @@ let ast_of_cvt_redexp = function (* Gives the ast corresponding to a tactic argument *) let ast_of_cvt_arg = function | Identifier id -> nvar (string_of_id id) - | Qualid qid -> nvar (string_of_qualid qid) + | Qualid qid -> nvar (Nametab.string_of_qualid qid) | Quoted_string s -> str s | Integer n -> num n | Command c -> ope ("COMMAND",[c]) |