diff options
| author | ppedrot | 2012-06-22 15:14:30 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-22 15:14:30 +0000 |
| commit | 6b45f2d36929162cf92272bb60c2c245d9a0ead3 (patch) | |
| tree | 93aa975697b7de73563c84773d99b4c65b92173b /pretyping/pretyping.ml | |
| parent | fea214f82954197d23fda9a0e4e7d93e0cbf9b4c (diff) | |
Added an indirection with respect to Loc in Compat. As many [open Compat]
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bcd2a1ad15..a494e2f932 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -21,7 +21,6 @@ (* Secondary maintenance: collective *) -open Compat open Pp open Errors open Util @@ -74,7 +73,7 @@ let search_guard loc env possible_indexes fixdefs = let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with - | e -> if loc = dummy_loc then raise e else Loc.raise loc e); + | e -> if loc = Loc.ghost then raise e else Loc.raise loc e); indexes else (* we now search recursively amoungst all combinations *) @@ -87,7 +86,7 @@ let search_guard loc env possible_indexes fixdefs = with TypeError _ -> ()) (list_combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in - if loc = dummy_loc then error errmsg else + if loc = Loc.ghost then error errmsg else user_err_loc (loc,"search_guard", Pp.str errmsg) with Found indexes -> indexes) @@ -428,7 +427,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional_loc - (join_loc floc argloc) env !evdref + (Loc.merge floc argloc) env !evdref resj [hj] in let resj = apply_rec env 1 fj candargs args in |