- | Ast.AnnotatedFormula (name, (Ast.Axiom | Ast.Hypothesis), f,_,_) :: tl->
- aux (p@[Ast.Constant name,trans_formulae ~neg:false f]) n tl
- | Ast.AnnotatedFormula (name, Ast.Negated_conjecture, f,_,_) :: tl ->
- assert (n = []);
- aux p (n@[Ast.Constant name, trans_formulae ~neg:true f]) tl
+ | Ast.AnnotatedFormula (name,
+ (Ast.Axiom | Ast.Hypothesis|Ast.Negated_conjecture), f,_,_) :: tl->
+ let is_positive, f = trans_formulae f in
+ if is_positive then aux (p@[Ast.Constant name,f]) n tl
+ else aux p (n@[Ast.Constant name,f]) tl