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 /pretyping/classops.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 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index f754f9f3f..73534210c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -31,7 +31,7 @@ type cl_typ = | CL_SECVAR of variable | CL_CONST of constant | CL_IND of inductive - | CL_PROJ of projection + | CL_PROJ of constant type cl_info_typ = { cl_param : int @@ -196,7 +196,8 @@ let find_class_type sigma t = match kind_of_term t' with | Var id -> CL_SECVAR id, Univ.Instance.empty, args | Const (sp,u) -> CL_CONST sp, u, args - | Proj (p, c) -> CL_PROJ p, Univ.Instance.empty, c :: args + | Proj (p, c) when not (Projection.unfolded p) -> + CL_PROJ (Projection.constant p), Univ.Instance.empty, c :: args | Ind (ind_sp,u) -> CL_IND ind_sp, u, args | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, [] | Sort _ -> CL_SORT, Univ.Instance.empty, [] @@ -406,7 +407,7 @@ let reference_arity_length ref = let projection_arity_length p = let len = reference_arity_length (ConstRef p) in - let pb = Environ.lookup_projection p (Global.env ()) in + let pb = Environ.lookup_projection (Projection.make p false) (Global.env ()) in len - pb.Declarations.proj_npars let class_params = function |