diff options
| author | Emilio Jesus Gallego Arias | 2020-05-13 02:49:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-13 02:49:27 +0200 |
| commit | 4a5944448e31022593df7d6e7e0318cfea92ea98 (patch) | |
| tree | 643d10e4058af9db9efbf84d7c91c4d8eeb152e1 /vernac | |
| parent | 0992c2669324a2ab911f5a4c08c27dc97f2bf371 (diff) | |
| parent | c5fdfe6ffef15795ecfde8f18f332ddefd35605e (diff) | |
Merge PR #12307: Cleaning up the legacy proof engine
Reviewed-by: ejgallego
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 41f2ab9c63..9d67ce3757 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1096,7 +1096,7 @@ let explain_typeclass_error env sigma = function (* Refiner errors *) let explain_refiner_bad_type env sigma arg ty conclty = - let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in + let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_leconstr_env env sigma conclty) in str "Refiner was given an argument" ++ brk(1,1) ++ pr_lconstr_env env sigma arg ++ spc () ++ str "of type" ++ brk(1,1) ++ pm ++ spc () ++ @@ -1112,16 +1112,9 @@ let explain_refiner_cannot_apply env sigma t harg = pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ pr_lconstr_env env sigma harg ++ str "." -let explain_refiner_not_well_typed env sigma c = - str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed." - let explain_intro_needs_product () = str "Introduction tactics needs products." -let explain_does_not_occur_in env sigma c hyp = - str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++ - str "does not occur in" ++ spc () ++ Id.print hyp ++ str "." - let explain_non_linear_proof env sigma c = str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++ spc () ++ str "because a metavariable has several occurrences." @@ -1137,9 +1130,7 @@ let explain_refiner_error env sigma = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg - | NotWellTyped c -> explain_refiner_not_well_typed env sigma c | IntroNeedsProduct -> explain_intro_needs_product () - | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp | NonLinearProof c -> explain_non_linear_proof env sigma c | MetaInType c -> explain_meta_in_type env sigma c | NoSuchHyp id -> explain_no_such_hyp id |