From 84544396cbbf34848be2240acf181b4d5f1f42d2 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 27 Sep 2014 16:08:02 +0200 Subject: Add a boolean to indicate the unfolding state of a primitive projection, so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections. --- kernel/mod_subst.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'kernel/mod_subst.ml') diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index cfe46152e..b65fdb3ac 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -342,13 +342,15 @@ let rec map_kn f f' c = let func = map_kn f f' in match kind_of_term c with | Const kn -> (try snd (f' kn) with No_subst -> c) - | Proj (kn,t) -> - let kn' = try fst (f' (kn,Univ.Instance.empty)) - with No_subst -> kn + | Proj (p,t) -> + let p' = + try + Projection.map (fun kn -> fst (f' (kn,Univ.Instance.empty))) p + with No_subst -> p in let t' = func t in - if kn' == kn && t' == t then c - else mkProj (kn', t') + if p' == p && t' == t then c + else mkProj (p', t') | Ind ((kn,i),u) -> let kn' = f kn in if kn'==kn then c else mkIndU ((kn',i),u) -- cgit v1.2.3