diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 14:56:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 15:41:16 +0200 |
| commit | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch) | |
| tree | f76fd37023c71c20520e34e4a51c487e7a0388a0 /plugins/funind/glob_term_to_relation.ml | |
| parent | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff) | |
| parent | fc579fdc83b751a44a18d2373e86ab38806e7306 (diff) | |
Merge PR #244.
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 4d02c77c8..de2e5ea4e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -631,7 +631,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ + user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in @@ -663,7 +663,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ + user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in @@ -1198,7 +1198,7 @@ let rec compute_cst_params relnames params = function | GSort _ -> params | GHole _ -> params | GIf _ | GRec _ | GCast _ -> - raise (UserError("compute_cst_params", str "Not handled case")) + raise (UserError(Some "compute_cst_params", str "Not handled case")) and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) |