diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 19:24:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 19:24:57 +0000 |
| commit | a9f6f227bb6d51edce4293aaa013d543308282a3 (patch) | |
| tree | c573844795b2315c006bea9d83fd65b25db5adff /proofs | |
| parent | 28e3b1fde11b019a5dd01c417edacc20c8dd8f56 (diff) | |
Renommage bdize -> ast_of_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@385 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_trees.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index a9c65d50c..f4990659c 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -432,14 +432,15 @@ let ast_of_cvt_arg = function | Integer n -> num n | Command c -> ope ("COMMAND",[c]) | Constr c -> - ope ("COMMAND",[bdize false (assumptions_for_print []) c]) + ope ("COMMAND",[ast_of_constr false (assumptions_for_print []) c]) | Clause idl -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl) | Bindings bl -> ope ("BINDINGS", List.map (ast_of_cvt_bind (fun x -> x)) bl) | Cbindings bl -> ope ("BINDINGS", List.map - (ast_of_cvt_bind (bdize false (assumptions_for_print []))) bl) + (ast_of_cvt_bind + (ast_of_constr false (assumptions_for_print []))) bl) | Tacexp ast -> ope ("TACTIC",[ast]) | Redexp (s,args) -> ope ("REDEXP", [ope(s,args)]) | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); |