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/term.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 3b6b69a28..ab678666f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -89,7 +89,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.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 type values = Constr.values -- cgit v1.2.3