diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 16 | ||||
| -rw-r--r-- | vernac/himsg.ml | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 4 | ||||
| -rw-r--r-- | vernac/obligations.ml | 10 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
5 files changed, 19 insertions, 19 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 2a41a50ddf..3de7fe06bd 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 3c4fcf7145..1add1f4860 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 *) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 3d627d2f6e..3c7ede3c99 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -334,8 +334,8 @@ let universe_proof_terminator compute_guard hook = Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff = match opaque with - | Vernacexpr.Transparent -> false, true - | Vernacexpr.Opaque -> true, false + | Transparent -> false, true + | Opaque -> true, false in let proof = get_proof proof compute_guard (hook (Some (proof.Proof_global.universes))) is_opaque in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1e7721f8fe..3bf0ca0a87 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -849,12 +849,12 @@ let obligation_terminator name num guard hook auto pf = let obl = obls.(num) in let status = match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () - | (true, _), Vernacexpr.Opaque -> err_not_transp () - | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> + | (_, Evar_kinds.Expand), Opaque -> err_not_transp () + | (true, _), Opaque -> err_not_transp () + | (false, _), Opaque -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Transparent -> Evar_kinds.Define false - | (_, status), Vernacexpr.Transparent -> status + | (_, status), Transparent -> status in let obl = { obl with obl_status = false, status } in let ctx = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index eae8167c41..e1ce4e194c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -518,7 +518,7 @@ let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) let status = Pfedit.by (Tactics.exact_proof c) in - save_proof (Vernacexpr.(Proved(Opaque,None))); + save_proof (Vernacexpr.(Proved(Proof_global.Opaque,None))); if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = @@ -855,7 +855,7 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance ~atts abst sup inst props pri = let global = not (make_section_locality atts.locality) in - Dumpglob.dump_constraint inst false "inst"; + Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; let program_mode = Flags.is_program_mode () in ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri) @@ -1268,7 +1268,7 @@ let vernac_reserve bl = let vernac_generalizable ~atts = let local = make_non_locality atts.locality in - Implicit_quantifiers.declare_generalizable local + Implicit_quantifiers.declare_generalizable ~local let _ = declare_bool_option |