diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/dune | 2 | ||||
| -rw-r--r-- | proofs/refine.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/proofs/dune b/proofs/dune index 36e9799998..f8e7661997 100644 --- a/proofs/dune +++ b/proofs/dune @@ -1,6 +1,6 @@ (library (name proofs) (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure") - (public_name coq.proofs) + (public_name coq-core.proofs) (wrapped false) (libraries pretyping)) diff --git a/proofs/refine.ml b/proofs/refine.ml index ac410a958f..ce04c35e11 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -129,7 +129,6 @@ let solve_constraints = tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Unsafe.tclEVARSADVANCE sigma - with e -> - (* XXX this is absorbing anomalies? *) + with e when CErrors.noncritical e -> let info = Exninfo.reify () in tclZERO ~info e |