diff options
Diffstat (limited to 'proofs/proof_trees.ml')
| -rw-r--r-- | proofs/proof_trees.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 18cd475cde..45fe9e5a47 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -407,7 +407,11 @@ let ast_of_cvt_arg = function | Constr_context _ -> anomalylabstrm "ast_of_cvt_arg" [<'sTR "Constr_context argument could not be used">] - | Clause idl -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl) + | Clause idl -> + let transl = function + | InHyp id -> ope ("INHYP", [nvar (string_of_id id)]) + | InHypType id -> ope ("INHYPTYPE", [nvar (string_of_id id)]) in + ope ("CLAUSE", List.map transl idl) | Bindings bl -> ope ("BINDINGS", List.map (ast_of_cvt_bind (fun x -> x)) bl) | Cbindings bl -> |