diff options
| author | Kazuhiko Sakaguchi | 2021-03-06 22:19:41 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2021-03-09 18:10:23 +0900 |
| commit | 4bbbaff29bb748800636c7c737fdbda3a2ee819d (patch) | |
| tree | c97c213dbe52313d9c761e2d20026af4d62bb20d /pretyping/pretyping.ml | |
| parent | b55216ab3509f48e45aac035f1b799529d068f51 (diff) | |
Replace cl_index with cl_typ in coercionops.ml
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
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 e86a8a28c9..3ccc6ea125 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1398,7 +1398,7 @@ let understand_ltac flags env sigma lvar kind c = let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let path_convertible env sigma i p q = +let path_convertible env sigma cl p q = let open Coercionops in let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in @@ -1423,7 +1423,7 @@ let path_convertible env sigma i p q = p' | [] -> (* identity function for the class [i]. *) - let cl,params = class_info_from_index i in + let params = (class_info cl).cl_param in let clty = match cl with | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false}) @@ -1434,8 +1434,7 @@ let path_convertible env sigma i p q = | CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p)) in let names = - List.init params.cl_param - (fun n -> Id.of_string ("x" ^ string_of_int n)) + List.init params (fun n -> Id.of_string ("x" ^ string_of_int n)) in List.fold_right (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@ |