diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-24 16:05:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-24 16:05:02 +0200 |
| commit | 71ee5fcd23c3585801e7c7534171e2af3fd939ce (patch) | |
| tree | 778c93a623800d752da172f1c79e0af7841d9c1d /vernac | |
| parent | e43b85c925c0c9c87e1dde69760d9ea343c5cfa8 (diff) | |
| parent | 5ec974962c7be7a7280a8094da733e32c232f5e0 (diff) | |
Merge PR #7177: Unifying names of "smart" combinators + adding combinators in CArray
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 16 | ||||
| -rw-r--r-- | vernac/himsg.ml | 2 |
2 files changed, 9 insertions, 9 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 2a41a50dd..3de7fe06b 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -400,9 +400,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = lb_type_of_p >>= fun (lb_type_of_p,eff) -> Proofview.tclEVARMAP >>= fun sigma -> let lb_args = Array.append (Array.append - (Array.map (fun x -> x) v) - (Array.map (fun x -> do_arg sigma x 1) v)) - (Array.map (fun x -> do_arg sigma x 2) v) + v + (Array.Smart.map (fun x -> do_arg sigma x 1) v)) + (Array.Smart.map (fun x -> do_arg sigma x 2) v) in let app = if Array.is_empty lb_args then lb_type_of_p else mkApp (lb_type_of_p,lb_args) in @@ -471,9 +471,9 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = user_err err_msg in let bl_args = Array.append (Array.append - (Array.map (fun x -> x) v) - (Array.map (fun x -> do_arg sigma x 1) v)) - (Array.map (fun x -> do_arg sigma x 2) v ) + v + (Array.Smart.map (fun x -> do_arg sigma x 1) v)) + (Array.Smart.map (fun x -> do_arg sigma x 2) v ) in let app = if Array.is_empty bl_args then bl_t1 else mkApp (bl_t1,bl_args) @@ -923,7 +923,7 @@ let compute_dec_tact ind lnamesparrec nparrec = (* left *) Tacticals.New.tclTHENLIST [ simplest_left; - apply (EConstr.of_constr (mkApp(blI,Array.map(fun x->mkVar x) xargs))); + apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs))); Auto.default_auto ] ; @@ -939,7 +939,7 @@ let compute_dec_tact ind lnamesparrec nparrec = assert_by (Name freshH3) (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))) (Tacticals.New.tclTHENLIST [ - apply (EConstr.of_constr (mkApp(lbI,Array.map (fun x->mkVar x) xargs))); + apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs))); Auto.default_auto ]); Equality.general_rewrite_bindings_in true diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 3c4fcf714..1add1f486 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -86,7 +86,7 @@ let j_nf_betaiotaevar env sigma j = uj_type = Reductionops.nf_betaiota env sigma j.uj_type } let jv_nf_betaiotaevar env sigma jl = - Array.map (fun j -> j_nf_betaiotaevar env sigma j) jl + Array.Smart.map (fun j -> j_nf_betaiotaevar env sigma j) jl (** Printers *) |