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/constr.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/constr.mli') diff --git a/kernel/constr.mli b/kernel/constr.mli index 58f248b03..da7ac6a0d 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -103,7 +103,7 @@ val mkConst : constant -> constr val mkConstU : pconstant -> constr (** Constructs a projection application *) -val mkProj : (constant * constr) -> constr +val mkProj : (projection * constr) -> constr (** Inductive types *) @@ -190,7 +190,7 @@ type ('constr, 'types) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of constant * 'constr + | Proj of projection * 'constr (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative -- cgit v1.2.3