diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 20 | ||||
| -rw-r--r-- | theories/Vectors/VectorDef.v | 8 | ||||
| -rw-r--r-- | toplevel/command.ml | 5 |
4 files changed, 20 insertions, 18 deletions
@@ -7,6 +7,11 @@ Changes from V8.3 to V8.4 - New proof engine +- Maximal implicit arguments can now be set locally by { }. The registration + traverses fixpoints and lambdas. Because there is conversion in types, maximal + implicit arguments aren't taken into account in partial applications. Use eta + expansion. + Tactics - New tactics constr_eq, is_evar and has_evar. diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 428ddd6ab..bc067a2f5 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -294,27 +294,31 @@ let implicit_application env ?(allow_partial=true) f ty = in c, avoid let implicits_of_glob_constr ?(with_products=true) l = - let rec aux i c = - let abs loc na bk t b = - let rest = aux (succ i) b in - if bk = Implicit then + let add_impl i na bk l = + if bk = Implicit then let name = match na with | Name id -> Some id | Anonymous -> None in - (ExplByPos (i, name), (true, true, true)) :: rest - else rest + (ExplByPos (i, name), (true, true, true)) :: l + else l in + let rec aux i c = + let abs na bk b = + add_impl i na bk (aux (succ i) b) in match c with | GProd (loc, na, bk, t, b) -> - if with_products then abs loc na bk t b + if with_products then abs na bk b else (if bk = Implicit then msg_warning (str "Ignoring implicit status of product binder " ++ pr_name na ++ str " and following binders"); []) - | GLambda (loc, na, bk, t, b) -> abs loc na bk t b + | GLambda (loc, na, bk, t, b) -> abs na bk b | GLetIn (loc, na, t, b) -> aux i b + | GRec (_, fix_kind, nas, args, tys, bds) -> + let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in + list_fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) | _ -> [] in aux 1 l diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 807748edd..cff72c11b 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -269,14 +269,6 @@ end. End ITERATORS. -Implicit Arguments rectS. -Implicit Arguments rect2. -Implicit Arguments fold_left. -Implicit Arguments fold_right. -Implicit Arguments map. -Implicit Arguments fold_left2. - - Section SCANNING. Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop := |Forall_nil: Forall P [] diff --git a/toplevel/command.ml b/toplevel/command.ml index ae173f6c3..90376a431 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -68,13 +68,14 @@ let interp_definition bl red_option c ctypopt = let env = Global.env() in let evdref = ref Evd.empty in let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in + let nb_args = List.length ctx in let imps,ce = match ctypopt with None -> let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c in let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in check_evars env Evd.empty !evdref body; - imps1@imps2, + imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; const_entry_type = None; const_entry_opaque = false } @@ -85,7 +86,7 @@ let interp_definition bl red_option c ctypopt = let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in check_evars env Evd.empty !evdref body; check_evars env Evd.empty !evdref typ; - imps1@imps2, + imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; const_entry_type = Some typ; const_entry_opaque = false } |