aboutsummaryrefslogtreecommitdiff
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-11-21 16:46:11 +0100
committerGaëtan Gilbert2019-11-21 16:46:11 +0100
commitc0f34539209842735ccb93f3c069632b7eee4d6c (patch)
tree32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /pretyping/classops.ml
parentb680b06b31c27751a7d551d95839aea38f7fbea1 (diff)
parentd016f69818b30b75d186fb14f440b93b0518fc66 (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.ml14
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