diff options
| -rw-r--r-- | checker/environ.ml | 24 | ||||
| -rw-r--r-- | checker/environ.mli | 2 | ||||
| -rw-r--r-- | kernel/environ.ml | 23 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 4 | ||||
| -rw-r--r-- | test-suite/coqchk/primproj2.v | 10 |
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. |