diff options
| author | Hugo Herbelin | 2018-09-26 14:30:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 13:28:36 +0200 |
| commit | 4865687c8c5641170080a47c72ee26c75eece49d (patch) | |
| tree | 5643372d9537c095c975e5bd904dac6a1a68c9b0 | |
| parent | 9afe18c3190bb0210e03bf40f3af101a7c5604da (diff) | |
Using Constant.change_label (better level of abstraction to build kernel names).
| -rw-r--r-- | vernac/auto_ind_decl.ml | 18 |
1 files changed, 6 insertions, 12 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index eb51d2341a..dee7541d37 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -389,13 +389,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = | Const (cst,_) -> (* Works in specific situations where the args have to be already declared as a Parameter (see example "J" in test file SchemeEquality.v) *) - ( - let mp,dir,lbl = Constant.repr3 cst in - mkConst (Constant.make3 mp dir (Label.make ( - if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) - else ((Label.to_string lbl)^"_lb") - ))) - ) + let lbl = Label.to_string (Constant.label cst) in + let newlbl = if Int.equal offset 1 then ("eq_" ^ lbl) else (lbl ^ "_lb") in + mkConst (Constant.change_label cst (Label.make newlbl)) | _ -> raise (ConstructorWithNonParametricInductiveType (fst hd)) in @@ -453,11 +449,9 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = | Const (cst,_) -> (* Works in specific situations where the args have to be already declared as a Parameter (see example "J" in test file SchemeEquality.v) *) - let mp,dir,lbl = Constant.repr3 cst in - mkConst (Constant.make3 mp dir (Label.make ( - if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) - else ((Label.to_string lbl)^"_bl") - ))) + let lbl = Label.to_string (Constant.label cst) in + let newlbl = if Int.equal offset 1 then ("eq_" ^ lbl) else (lbl ^ "_bl") in + mkConst (Constant.change_label cst (Label.make newlbl)) | _ -> raise (ConstructorWithNonParametricInductiveType (fst hd)) in |