diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 22 |
4 files changed, 16 insertions, 16 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 465d1d80..cf9213dd 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: class_tactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: class_tactics.ml4 15025 2012-03-09 14:27:07Z glondu $ *) open Pp open Util @@ -219,7 +219,7 @@ let e_possible_resolve db_list local_db gl = let rec catchable = function | Refiner.FailError _ -> true - | Stdpp.Exc_located (_, e) -> catchable e + | Compat.Exc_located (_, e) -> catchable e | e -> Logic.catchable_exception e let is_dep gl gls = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index c4a2ef44..c7762c69 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: extratactics.ml4 15025 2012-03-09 14:27:07Z glondu $ *) open Pp open Pcoq @@ -580,7 +580,7 @@ let hResolve id c occ t gl = try Pretyping.Default.understand sigma env t_hole with - | Stdpp.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> + | Compat.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) in let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index fd3eeeb2..cf5fab0c 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1057,7 +1057,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = else tclIDTAC in tclTHENLIST [evartac; rewtac] gl with - | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) + | Compat.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> Refiner.tclFAIL_lazy 0 (lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints." 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 = |