diff options
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ddaf82a18a..2a98cae53b 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -509,7 +509,6 @@ let context operation path (t : constr) = | ((P_TYPE :: p), LetIn (n,b,t,c)) -> (mkLetIn (n,b,loop i p t,c)) | (p, _) -> - ppnl (Printer.pr_lconstr t); failwith ("abstract_path " ^ string_of_int(List.length p)) in loop 1 path t @@ -530,7 +529,6 @@ let occurence path (t : constr) = | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term | (p, _) -> - ppnl (Printer.pr_lconstr t); failwith ("occurence " ^ string_of_int(List.length p)) in loop path t |