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 /tactics/eauto.ml | |
| parent | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff) | |
| parent | fc579fdc83b751a44a18d2373e86ab38806e7306 (diff) | |
Merge PR #244.
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index ba9a2d95c..ba2195070 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -97,8 +97,8 @@ let prolog_tac l n = in let l = List.map map l in try (prolog l n gl) - with UserError ("Refiner.tclFIRST",_) -> - errorlabstrm "Prolog.prolog" (str "Prolog failed.") + with UserError (Some "Refiner.tclFIRST",_) -> + user_err ~hdr:"Prolog.prolog" (str "Prolog failed.") end open Auto @@ -431,7 +431,7 @@ let cons a l = a :: l let autounfolds db occs cls gl = let unfolds = List.concat (List.map (fun dbname -> let db = try searchtable_map dbname - with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) + with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname) in let (ids, csts) = Hint_db.unfolds db in let hyps = pf_ids_of_hyps gl in @@ -498,7 +498,7 @@ let autounfold_one db cl = let st = List.fold_left (fun (i,c) dbname -> let db = try searchtable_map dbname - with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) + with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname) in let (ids, csts) = Hint_db.unfolds db in (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db |