diff options
| author | Gaëtan Gilbert | 2019-11-21 16:46:11 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-21 16:46:11 +0100 |
| commit | c0f34539209842735ccb93f3c069632b7eee4d6c (patch) | |
| tree | 32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /pretyping/classops.ml | |
| parent | b680b06b31c27751a7d551d95839aea38f7fbea1 (diff) | |
| parent | d016f69818b30b75d186fb14f440b93b0518fc66 (diff) | |
Merge PR #11010: [coq] Untabify the whole ML codebase.
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 57dbfb2580..c12a236d8e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -195,7 +195,7 @@ let subst_cl_typ subst ct = match ct with pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value))) | CL_IND i -> let i' = subst_ind subst i in - if i' == i then ct else CL_IND i' + if i' == i then ct else CL_IND i' (*CSC: here we should change the datatype for coercions: it should be possible to declare any term as a coercion *) @@ -267,7 +267,7 @@ let lookup_path_between env sigma (s,t) = let (s,(t,p)) = apply_on_class_of env sigma s (fun i -> apply_on_class_of env sigma t (fun j -> - lookup_path_between_class (i,j))) in + lookup_path_between_class (i,j))) in (s,t,p) let lookup_path_to_fun_from env sigma s = @@ -323,7 +323,7 @@ let warn_ambiguous_path = let different_class_params env i = let ci = class_info_from_index i in if (snd ci).cl_param > 0 then true - else + else match fst ci with | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i) | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c) @@ -351,16 +351,16 @@ let add_coercion_in_graph env sigma (ic,source,target) = ClPairMap.iter (fun (s,t) p -> if not (Bijint.Index.equal s t) then begin - if Bijint.Index.equal t source then begin + if Bijint.Index.equal t source then begin try_add_new_path1 (s,target) (p@[ic]); ClPairMap.iter - (fun (u,v) q -> + (fun (u,v) q -> if not (Bijint.Index.equal u v) && Bijint.Index.equal u target && not (List.equal coe_info_typ_equal p q) then - try_add_new_path1 (s,v) (p@[ic]@q)) + try_add_new_path1 (s,v) (p@[ic]@q)) old_inheritance_graph end; if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p) - end) + end) old_inheritance_graph end; match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths |
