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/nativelambda.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'kernel/nativelambda.ml') diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 34ed33f94..ba45c329f 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -586,7 +586,8 @@ let rec lambda_of_constr env sigma c = | Construct _ -> lambda_of_app env sigma c empty_args | Proj (p, c) -> - mkLapp (Lproj (get_const_prefix !global_env p, p)) [|lambda_of_constr env sigma c|] + let kn = Projection.constant p in + mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in -- cgit v1.2.3