diff options
| author | Matthieu Sozeau | 2014-09-27 16:08:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-27 20:41:04 +0200 |
| commit | 84544396cbbf34848be2240acf181b4d5f1f42d2 (patch) | |
| tree | 72d398f334bdc7b1c6a0ee333a05940c34780f12 /kernel/cooking.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/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 2d316fc1d9..5f6aebc4e0 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -123,12 +123,13 @@ let expmod_constr cache modlist c = | Proj (p, c') -> (try - let p' = share_univs (ConstRef p) Univ.Instance.empty modlist in + let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in + let make c = Projection.make c (Projection.unfolded p) in match kind_of_term p' with - | Const (p',_) -> mkProj (p', substrec c') + | Const (p',_) -> mkProj (make p', substrec c') | App (f, args) -> (match kind_of_term f with - | Const (p', _) -> mkProj (p', substrec c') + | Const (p', _) -> mkProj (make p', substrec c') | _ -> assert false) | _ -> assert false with Not_found -> map_constr substrec c) |