diff options
| author | Emilio Jesus Gallego Arias | 2018-04-27 14:36:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-04-27 14:36:30 +0200 |
| commit | 53fb4203b80da48e2ac9b06803c57e81df702a0a (patch) | |
| tree | 0dc2a8efe8012190fcfcda50faf65365e30a3bad /kernel/uGraph.ml | |
| parent | c65a1637b5e6cb60222963f29fc7c01bd7d1ee0b (diff) | |
| parent | 285bd0778bfa829e1969598cccd5d7c504d5fa90 (diff) | |
Merge PR #7351: Always print explanation for univ inconsistency, rm Flags.univ_print
Diffstat (limited to 'kernel/uGraph.ml')
| -rw-r--r-- | kernel/uGraph.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 5d1644614d..b4ea04a56b 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -21,7 +21,7 @@ open Univ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *) -let error_inconsistency o u v (p:explanation option) = +let error_inconsistency o u v p = raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p)) (* Universes are stratified by a partial ordering $\le$. @@ -557,8 +557,7 @@ let get_explanation strict u v g = else match traverse strict u with Some exp -> exp | None -> assert false let get_explanation strict u v g = - if !Flags.univ_print then Some (get_explanation strict u v g) - else None + Some (lazy (get_explanation strict u v g)) (* To compare two nodes, we simply do a forward search. We implement two improvements: |