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. --- library/heads.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/heads.ml') diff --git a/library/heads.ml b/library/heads.ml index 31908816b..8b28f0500 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -84,7 +84,7 @@ let kind_of_head env t = | Meta _ | Evar _ -> NotImmediatelyComputableHead | App (c,al) -> aux k (Array.to_list al @ l) c b | Proj (p,c) -> - (try on_subterm k (c :: l) b (constant_head p) + (try on_subterm k (c :: l) b (constant_head (Projection.constant p)) with Not_found -> assert false) | Case (_,_,c,_) -> aux k [] c true -- cgit v1.2.3