From 2defd4c15467736b73f69adb501e3a4fe2111ce5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 29 Jun 2015 21:30:19 +0200
Subject: Assumptions: more informative print for False axiom (Close: #4054)

When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).

E.g.

  Lemma w : True.
  Proof. case demon. Qed.

  Lemma x y : y = 0 /\ True /\ forall w, w = y.
  Proof. split. case demon. split; [ exact w | case demon ]. Qed.

  Print Assumptions x.

Prints:

  Axioms:
  demon : False
   used in x to prove: forall w : nat, w = y
   used in w to prove: True
   used in x to prove: y = 0
---
 pretyping/termops.ml  | 15 +++++++++------
 pretyping/termops.mli |  4 ++++
 2 files changed, 13 insertions(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9f04faa839..937471cf76 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -453,26 +453,29 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
    index) which is processed by [g] (which typically add 1 to [n]) at
    each binder traversal; it is not recursive *)
 
-let fold_constr_with_binders g f n acc c = match kind_of_term c with
+let fold_constr_with_full_binders g f n acc c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (_,t,c) -> f (g n) (f n acc t) c
-  | Lambda (_,t,c) -> f (g n) (f n acc t) c
-  | LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
+  | Prod (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let n' = iterate g (Array.length tl) n in
+      let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let n' = iterate g (Array.length tl) n in
+      let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
+let fold_constr_with_binders g f n acc c =
+  fold_constr_with_full_binders (fun _ x -> g x) f n acc c
+
 (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
    subterms of [c]; it carries an extra data [acc] which is processed by [g] at
    each binder traversal; it is not recursive and the order with which
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 2552c67e61..4581e23100 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -84,6 +84,10 @@ val map_constr_with_full_binders :
 val fold_constr_with_binders :
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
+val fold_constr_with_full_binders :
+  (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
+    'a -> 'b -> constr -> 'b
+
 val iter_constr_with_full_binders :
   (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
     constr -> unit
-- 
cgit v1.2.3