diff options
| author | Gaëtan Gilbert | 2019-06-13 15:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 13:06:22 +0200 |
| commit | 2ded4c25e532c5dfca0483c211653768ebed01a7 (patch) | |
| tree | a04b2f787490c8971590e6bdf7dd1ec4220e0290 /vernac/assumptions.ml | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'vernac/assumptions.ml')
| -rw-r--r-- | vernac/assumptions.ml | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 2bb4bac9a4..848cd501c6 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -179,7 +179,7 @@ let rec traverse current ctx accu t = | Construct (((mind, _), _) as cst, _) -> traverse_inductive accu mind (ConstructRef cst) | Meta _ | Evar _ -> assert false -| Case (_,oty,c,[||]) -> +| Case (_,oty,_,c,[||]) -> (* non dependent match on an inductive with no constructors *) begin match Constr.(kind oty, kind c) with | Lambda(_,_,oty), Const (kn, _) @@ -306,6 +306,13 @@ let traverse current t = considering terms out of any valid environment, so use with caution. *) let type_of_constant cb = cb.Declarations.const_type +let uses_uip mib = + Array.exists (fun mip -> + mip.mind_relevance == Sorts.Irrelevant + && Array.length mip.mind_nf_lc = 1 + && List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt) + mib.mind_packets + let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = (* Only keep the transitive dependencies *) let (_, graph, ax2ty) = traverse (label_of gr) t in @@ -363,5 +370,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in + let accu = + if not (uses_uip mind) then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (UIP m, l)) Constr.mkProp accu + in accu in GlobRef.Map_env.fold fold graph ContextObjectMap.empty |