diff options
| author | Emilio Jesus Gallego Arias | 2018-10-28 15:01:04 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-28 15:01:04 +0100 |
| commit | 38a2e8c383228e9cb3a3437d981d30a488f5a084 (patch) | |
| tree | ca838f17ba0aecd7257ed8bde1ebbfbf652ee5dc | |
| parent | 665146168720c094ce4fbb3d7d044d9904099f95 (diff) | |
[error printing] Fix improper grounding of open terms in printing.
Fixes #8224, fixes #8427 .
| -rw-r--r-- | engine/eConstr.ml | 8 | ||||
| -rw-r--r-- | engine/eConstr.mli | 2 | ||||
| -rw-r--r-- | vernac/himsg.ml | 5 |
3 files changed, 12 insertions, 3 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 3385b78958..cfc4bea85f 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -99,6 +99,14 @@ let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false + +let rec isType sigma c = match kind sigma c with + | Sort s -> (match ESorts.kind sigma s with + | Sorts.Type _ -> true + | _ -> false ) + | Cast (c,_,_) -> isType sigma c + | _ -> false + let isVarId sigma id c = match kind sigma c with Var id' -> Id.equal id id' | _ -> false let isRelN sigma n c = diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 1edc0ee12b..6532e08e9d 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -157,6 +157,8 @@ val isCoFix : Evd.evar_map -> t -> bool val isCase : Evd.evar_map -> t -> bool val isProj : Evd.evar_map -> t -> bool +val isType : Evd.evar_map -> constr -> bool + type arity = rel_context * ESorts.t val destArity : Evd.evar_map -> types -> arity val isArity : Evd.evar_map -> t -> bool diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ca77e03707..45eaa4ba1e 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -391,11 +391,10 @@ let explain_unexpected_type env sigma actual_type expected_type = str "where" ++ spc () ++ prexp ++ str " was expected." let explain_not_product env sigma c = - let c = EConstr.to_constr sigma c in - let pr = pr_lconstr_env env sigma c in + let pr = pr_econstr_env env sigma c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ - (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." + (if EConstr.isType sigma c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) |