diff options
| author | Enrico Tassi | 2015-12-09 15:14:10 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-12-09 15:14:33 +0100 |
| commit | 38e70af82d33de8e977b9b7e347ff501fcd5c2d8 (patch) | |
| tree | 0a3016cd374b150c63590820699fdb399fed3152 | |
| parent | 9d45d45f3a8718581a001af4576ca87feb741073 (diff) | |
Print Assumptions: improve detection of case on an axiom of False
The name in the return clause has no semantic meaning, we must not
look at it.
| -rw-r--r-- | toplevel/assumptions.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index a6bd968efc..a71588fe05 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -158,7 +158,7 @@ let rec traverse current ctx accu t = match kind_of_term t with | Case (_,oty,c,[||]) -> (* non dependent match on an inductive with no constructors *) begin match Constr.(kind oty, kind c) with - | Lambda(Anonymous,_,oty), Const (kn, _) + | Lambda(_,_,oty), Const (kn, _) when Vars.noccurn 1 oty && not (Declareops.constant_has_body (lookup_constant kn)) -> let body () = Global.body_of_constant_body (lookup_constant kn) in |