aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--checker/environ.ml24
-rw-r--r--checker/environ.mli2
-rw-r--r--kernel/environ.ml23
-rw-r--r--kernel/environ.mli4
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--test-suite/coqchk/primproj2.v10
6 files changed, 25 insertions, 42 deletions
diff --git a/checker/environ.ml b/checker/environ.ml
index 3830cd0dc..bbd043c8e 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -126,7 +126,7 @@ let add_constant kn cs env =
env_constants = new_constants } in
{ env with env_globals = new_globals }
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
(* Constant types *)
@@ -148,18 +148,16 @@ exception NotEvaluableConst of const_evaluation_result
let constant_value env (kn,u) =
let cb = lookup_constant kn env in
- if cb.const_proj = None then
- match cb.const_body with
- | Def l_body ->
- let b = force_constr l_body in
- begin
- match cb.const_universes with
- | Monomorphic_const _ -> b
- | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
- end
- | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
- | Undef _ -> raise (NotEvaluableConst NoBody)
- else raise (NotEvaluableConst IsProj)
+ match cb.const_body with
+ | Def l_body ->
+ let b = force_constr l_body in
+ begin
+ match cb.const_universes with
+ | Monomorphic_const _ -> b
+ | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
+ end
+ | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+ | Undef _ -> raise (NotEvaluableConst NoBody)
(* A global const is evaluable if it is defined and not opaque *)
let evaluable_constant cst env =
diff --git a/checker/environ.mli b/checker/environ.mli
index ba62ed519..36e0ea027 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -52,7 +52,7 @@ val check_constraints : Univ.constraints -> env -> bool
val lookup_constant : Constant.t -> env -> Cic.constant_body
val add_constant : Constant.t -> Cic.constant_body -> env -> env
val constant_type : env -> Constant.t puniverses -> constr Univ.constrained
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
val constant_value : env -> Constant.t puniverses -> constr
val evaluable_constant : Constant.t -> env -> bool
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 93dc2f9a7..738ecc6e1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -254,31 +254,10 @@ let constant_context env kn =
| Monomorphic_const _ -> Univ.AUContext.empty
| Polymorphic_const ctx -> ctx
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
-let constant_value env (kn,u) =
- let cb = lookup_constant kn env in
- if cb.const_proj = None then
- match cb.const_body with
- | Def l_body ->
- begin
- match cb.const_universes with
- | Monomorphic_const _ ->
- (Mod_subst.force_constr l_body, Univ.Constraint.empty)
- | Polymorphic_const _ ->
- let csts = constraints_of cb u in
- (subst_instance_constr u (Mod_subst.force_constr l_body), csts)
- end
- | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
- | Undef _ -> raise (NotEvaluableConst NoBody)
- else raise (NotEvaluableConst IsProj)
-
-let constant_opt_value env cst =
- try Some (constant_value env cst)
- with NotEvaluableConst _ -> None
-
let constant_value_and_type env (kn, u) =
let cb = lookup_constant kn env in
if Declareops.constant_is_polymorphic cb then
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7cc541258..69d811a64 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -146,13 +146,11 @@ val type_in_type_constant : Constant.t -> env -> bool
body and [NotEvaluableConst IsProj] if [c] is a projection
and [Not_found] if it does not exist in [env] *)
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
-val constant_value : env -> Constant.t puniverses -> constr constrained
val constant_type : env -> Constant.t puniverses -> types constrained
-val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.Constraint.t) option
val constant_value_and_type : env -> Constant.t puniverses ->
constr option * types * Univ.Constraint.t
(** The universe context associated to the constant, empty if not
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 5a522e06a..f682143f8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -60,9 +60,7 @@ let value_of_evaluable_ref env evref u =
match evref with
| EvalConstRef con ->
let u = Unsafe.to_instance u in
- EConstr.of_constr (try constant_value_in env (con,u)
- with NotEvaluableConst IsProj ->
- raise (Invalid_argument "value_of_evaluable_ref"))
+ EConstr.of_constr (constant_value_in env (con, u))
| EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get
let evaluable_of_global_reference env = function
diff --git a/test-suite/coqchk/primproj2.v b/test-suite/coqchk/primproj2.v
new file mode 100644
index 000000000..f73c627ee
--- /dev/null
+++ b/test-suite/coqchk/primproj2.v
@@ -0,0 +1,10 @@
+Set Primitive Projections.
+
+Record Pack (A : Type) := pack { unpack : A }.
+
+Definition p : Pack bool.
+Proof.
+refine (pack _ true).
+Qed.
+
+Definition boom : unpack bool p = let u := unpack _ in u p := eq_refl.