diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 16:08:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:04 +0200 |
| commit | 84544396cbbf34848be2240acf181b4d5f1f42d2 (patch) | |
| tree | 72d398f334bdc7b1c6a0ee333a05940c34780f12 /kernel/indtypes.ml | |
| parent | 0efba04058ba28889c83553224309be216873298 (diff) | |
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.
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 4feec40e8..73a23ef05 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -692,14 +692,15 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params | Name id -> let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in let ty = substl subst (liftn 1 j t) in - let term = mkProj (kn, mkRel 1) in + let term = mkProj (Projection.make kn true, mkRel 1) in + let fterm = mkProj (Projection.make kn false, mkRel 1) in let compat = compat_body ty (j - 1) in let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in let body = { proj_ind = fst ind; proj_npars = nparamargs; proj_arg = i; proj_type = ty; proj_eta = etab, etat; proj_body = compat } in - (i + 1, j + 1, kn :: kns, body :: pbs, term :: subst) + (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst) | Anonymous -> raise UndefinableExpansion in let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in |