From 38e70af82d33de8e977b9b7e347ff501fcd5c2d8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Dec 2015 15:14:10 +0100 Subject: 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. --- toplevel/assumptions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index a6bd968ef..a71588fe0 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 -- cgit v1.2.3