diff options
| author | Hugo Herbelin | 2018-04-13 19:47:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:27:50 +0200 |
| commit | 09482343fec8cd40b1f9523be8e5e2601eb0bbae (patch) | |
| tree | c03215fd6c6ef1416b159a33d59abc87d976a1b1 | |
| parent | a25a28e167aabca816a6af37c69a1a72a6be9388 (diff) | |
Minor cosmetic unifying of layout in pretyping.ml.
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 42491f4e40..4c3a001186 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -829,7 +829,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GLambda(name,bk,c1,c2) -> + | GLambda(name,bk,c1,c2) -> let tycon' = evd_comb1 (fun evd tycon -> match tycon with @@ -851,7 +851,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GProd(name,bk,c1,c2) -> + | GProd(name,bk,c1,c2) -> let j = pretype_type empty_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are @@ -875,7 +875,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre iraise (e, info) in inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GLetIn(name,c1,t,c2) -> + | GLetIn(name,c1,t,c2) -> let tycon1 = match t with | Some t -> |