diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 6a11384b..929f1013 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 14677 2011-11-17 22:19:38Z herbelin $ *) +(* $Id: tacinterp.ml 15025 2012-03-09 14:27:07Z glondu $ *) open Constrintern open Closure @@ -93,15 +93,15 @@ let dloc = dummy_loc let catch_error call_trace tac g = if call_trace = [] then tac g else try tac g with | LtacLocated _ as e -> raise e - | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e + | Compat.Exc_located (_,LtacLocated _) as e -> raise e | e -> let (nrep,loc',c),tail = list_sep_last call_trace in - let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in + let loc,e' = match e with Compat.Exc_located(loc,e) -> loc,e | _ ->dloc,e in if tail = [] then let loc = if loc = dloc then loc' else loc in - raise (Stdpp.Exc_located(loc,e')) + raise (Compat.Exc_located(loc,e')) else - raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e'))) + raise (Compat.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e'))) (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = @@ -1979,14 +1979,14 @@ and eval_with_fail ist is_lazy goal tac = VRTactic (catch_error trace tac goal) | a -> a) with - | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) - | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) -> + | FailError (0,s) | Compat.Exc_located(_, FailError (0,s)) + | Compat.Exc_located(_,LtacLocated (_,FailError (0,s))) -> raise (Eval_fail (Lazy.force s)) | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located(s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) - | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> - raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s')))) + | Compat.Exc_located(s,FailError (lvl,s')) -> + raise (Compat.Exc_located(s,FailError (lvl - 1, s'))) + | Compat.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + raise (Compat.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s')))) (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist gl llc u = |