diff options
47 files changed, 522 insertions, 282 deletions
@@ -69,6 +69,9 @@ Tactics hypotheses of the form "~True" or "t<>t" (possible source of incompatibilities because of more successes in automation, but generally a more intuitive strategy). +- Option "Injection On Proofs" was renamed "Keep Proof Equalities". When + enabled, injection and inversion do not drop equalities between objects + in Prop. Still disabled by default. Hints diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d23a49bc6..2da12c8d6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2289,6 +2289,12 @@ giving \texttt{injection {\term} as} (with an empty list of names). To obtain this behavior, the option {\tt Set Structural Injection} must be activated. This option is off by default. +By default, \texttt{injection} only creates new equalities between +terms whose type is in sort \texttt{Type} or \texttt{Set}, thus +implementing a special behavior for objects that are proofs +of a statement in \texttt{Prop}. This behavior can be turned off +by setting the option \texttt{Set Keep Proof Equalities}. +\optindex{Keep Proof Equalities} \subsection{\tt inversion \ident} \tacindex{inversion} @@ -2308,6 +2314,14 @@ latter is first introduced in the local context using stock the lemmas whenever the same instance needs to be inverted several times. See Section~\ref{Derive-Inversion}. +\Rem Part of the behavior of the \texttt{inversion} tactic is to generate +equalities between expressions that appeared in the hypothesis that is +being processed. By default, no equalities are generated if they relate +two proofs (i.e. equalities between terms whose type is in +sort \texttt{Prop}). This behavior can be turned off by using the option +\texttt{Set Keep Proof Equalities.} +\optindex{Keep Proof Equalities} + \begin{Variants} \item \texttt{inversion \num} diff --git a/engine/termops.ml b/engine/termops.ml index b2c9492e1..5e65652c0 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -976,11 +976,8 @@ let smash_rel_context sign = let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init -let rec mem_named_context id ctxt = - match ctxt with - | decl :: _ when Id.equal id (NamedDecl.get_id decl) -> true - | _ :: sign -> mem_named_context id sign - | [] -> false +let mem_named_context_val id ctxt = + try Environ.lookup_named_val id ctxt; true with Not_found -> false let compact_named_context sign = let compact l decl = diff --git a/engine/termops.mli b/engine/termops.mli index a7f45d28a..7d6e99acc 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -237,7 +237,7 @@ val map_rel_context_with_binders : val fold_named_context_both_sides : ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> Context.Named.t -> init:'a -> 'a -val mem_named_context : Id.t -> Context.Named.t -> bool +val mem_named_context_val : Id.t -> named_context_val -> bool val compact_named_context : Context.Named.t -> Context.Compacted.t val clear_named_body : Id.t -> env -> env diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 9890a518c..6fbed38fb 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -705,6 +705,7 @@ let rec tmpp v loc = | VernacSetStrategy _ as x -> xmlTODO loc x | VernacUnsetOption _ as x -> xmlTODO loc x | VernacSetOption _ as x -> xmlTODO loc x + | VernacSetAppendOption _ as x -> xmlTODO loc x | VernacAddOption _ as x -> xmlTODO loc x | VernacRemoveOption _ as x -> xmlTODO loc x | VernacMemOption _ as x -> xmlTODO loc x diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 786f15b40..235e6e24f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1399,7 +1399,40 @@ let rec intern_pat genv aliases pat = check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten pl') +(* [check_no_patcast p] raises an error if [p] contains a cast. This code is a + bit ad-hoc, and is due to current restrictions on casts in patterns. We + support them only in local binders and only at top level. In fact, they are + currently eliminated by the parser. The only reason why they are in the + [cases_pattern_expr] type is that the parser needs to factor the "(c : t)" + notation with user defined notations (such as the pair). In the long term, we + will try to support such casts everywhere, and use them to print the domains + of lambdas in the encoding of match in constr. We put this check here and not + in the parser because it would require to duplicate the levels of the + [pattern] rule. *) +let rec check_no_patcast = function + | CPatCast (loc,_,_) -> + CErrors.user_err ~loc ~hdr:"check_no_patcast" + (Pp.strbrk "Casts are not supported here.") + | CPatDelimiters(_,_,p) + | CPatAlias(_,p,_) -> check_no_patcast p + | CPatCstr(_,_,opl,pl) -> + Option.iter (List.iter check_no_patcast) opl; + List.iter check_no_patcast pl + | CPatOr(_,pl) -> + List.iter check_no_patcast pl + | CPatNotation(_,_,subst,pl) -> + check_no_patcast_subst subst; + List.iter check_no_patcast pl + | CPatRecord(_,prl) -> + List.iter (fun (_,p) -> check_no_patcast p) prl + | CPatAtom _ | CPatPrim _ -> () + +and check_no_patcast_subst (pl,pll) = + List.iter check_no_patcast pl; + List.iter (List.iter check_no_patcast) pll + let intern_cases_pattern genv scopes aliases pat = + check_no_patcast pat; intern_pat genv aliases (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat) @@ -1408,6 +1441,7 @@ let _ = fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p let intern_ind_pattern genv scopes pat = + check_no_patcast pat; let no_not = try drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat @@ -2002,14 +2036,14 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a = tmp_scope = None; scopes = []; impls = impls} false (empty_ltac_sign, vl) a in (* Translate and check that [c] has all its free variables bound in [vars] *) - let a = notation_constr_of_glob_constr nenv c in + let a, reversible = notation_constr_of_glob_constr nenv c in (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in let vars = Id.Map.map (fun (isonlybinding, sc, typ) -> (!isonlybinding, out_scope !sc, typ)) vl in (* Returns [a] and the ordered list of variables with their scopes *) - vars, a + vars, a, reversible (* Interpret binders and contexts *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index eea76aa31..61e7c6f5c 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -186,7 +186,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr val interp_notation_constr : ?impls:internalization_env -> notation_interp_env -> constr_expr -> (bool * subscopes * notation_var_internalization_type) Id.Map.t * - notation_constr + notation_constr * reversibility_flag (** Globalization options *) val parsing_explicit : bool ref diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index fca1c7904..d7f283e95 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -323,6 +323,7 @@ let compare_recursive_parts found f f' (iterator,subc) = let notation_constr_and_vars_of_glob_constr a = let found = ref ([],[],[]) in + let has_ltac = ref false in let rec aux c = let keepfound = !found in (* n^2 complexity but small and done only once per notation *) @@ -368,7 +369,9 @@ let notation_constr_and_vars_of_glob_constr a = NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) | GSort (_,s) -> NSort s - | GHole (_,w,naming,arg) -> NHole (w, naming, arg) + | GHole (_,w,naming,arg) -> + if arg != None then has_ltac := true; + NHole (w, naming, arg) | GRef (_,r,_) -> NRef r | GEvar _ | GPatVar _ -> error "Existential variables not allowed in notations." @@ -376,9 +379,10 @@ let notation_constr_and_vars_of_glob_constr a = in let t = aux a in (* Side effect *) - t, !found + t, !found, !has_ltac -let check_variables nenv (found,foundrec,foundrecbinding) = +let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = + let injective = ref true in let recvars = nenv.ninterp_rec_vars in let fold _ y accu = Id.Set.add y accu in let useless_vars = Id.Map.fold fold recvars Id.Set.empty in @@ -401,7 +405,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = error (Id.to_string x ^ " should not be bound in a recursive pattern of the right-hand side.") - else nenv.ninterp_only_parse <- true + else injective := false in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then @@ -421,12 +425,13 @@ let check_variables nenv (found,foundrec,foundrecbinding) = with Not_found -> check_bound x end | NtnInternTypeIdent -> check_bound x in - Id.Map.iter check_type vars + Id.Map.iter check_type vars; + !injective let notation_constr_of_glob_constr nenv a = - let a, found = notation_constr_and_vars_of_glob_constr a in - let () = check_variables nenv found in - a + let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in + let injective = check_variables_and_reversibility nenv found in + a, not has_ltac && injective (**********************************************************************) (* Substitution of kernel names, avoiding a list of bound identifiers *) @@ -436,7 +441,6 @@ let notation_constr_of_constr avoiding t = let nenv = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; - ninterp_only_parse = false; } in notation_constr_of_glob_constr nenv t @@ -454,7 +458,7 @@ let rec subst_notation_constr subst bound raw = | NRef ref -> let ref',t = subst_global subst ref in if ref' == ref then raw else - notation_constr_of_constr bound t + fst (notation_constr_of_constr bound t) | NVar _ -> raw diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 4ebd3ddd8..c8fcbf741 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -29,7 +29,7 @@ val ldots_var : Id.t bound by the notation; also interpret recursive patterns *) val notation_constr_of_glob_constr : notation_interp_env -> - glob_constr -> notation_constr + glob_constr -> notation_constr * reversibility_flag (** Re-interpret a notation as a [glob_constr], taking care of binders *) diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 883b01772..1ab9980a5 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -73,10 +73,11 @@ type interpretation = (Id.t * (subscopes * notation_var_instance_type)) list * notation_constr +type reversibility_flag = bool + type notation_interp_env = { ninterp_var_type : notation_var_internalization_type Id.Map.t; ninterp_rec_vars : Id.t Id.Map.t; - mutable ninterp_only_parse : bool; } type grammar_constr_prod_item = diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ca1be3b3d..7424fd85a 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -428,6 +428,7 @@ type vernac_expr = (Conv_oracle.level * reference or_by_notation list) list | VernacUnsetOption of Goptions.option_name | VernacSetOption of Goptions.option_name * option_value + | VernacSetAppendOption of Goptions.option_name * string | VernacAddOption of Goptions.option_name * option_ref_value list | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index d475f097c..fe9ec5794 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -270,11 +270,9 @@ let info_env info = info.i_cache.i_env open Context.Named.Declaration -let rec assoc_defined id = function -| [] -> raise Not_found -| LocalAssum _ :: ctxt -> assoc_defined id ctxt -| LocalDef (id', c, _) :: ctxt -> - if Id.equal id id' then c else assoc_defined id ctxt +let assoc_defined id env = match Environ.lookup_named id env with +| LocalDef (_, c, _) -> c +| _ -> raise Not_found let ref_value_cache ({i_cache = cache} as infos) ref = try @@ -291,7 +289,7 @@ let ref_value_cache ({i_cache = cache} as infos) ref = | None -> raise Not_found | Some t -> lift n t end - | VarKey id -> assoc_defined id (named_context cache.i_env) + | VarKey id -> assoc_defined id cache.i_env | ConstKey cst -> constant_value_in cache.i_env cst in let v = cache.i_repr infos body in diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 925214899..40595f944 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -191,7 +191,7 @@ and slot_for_fv env fv = let nv = Pre_env.lookup_named_val id env in begin match force_lazy_val nv with | None -> - env.env_named_context |> Context.Named.lookup id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun + env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> diff --git a/kernel/environ.ml b/kernel/environ.ml index 8a147a659..1d44cac5b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -56,14 +56,14 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let universes env = env.env_stratification.env_universes -let named_context env = env.env_named_context -let named_context_val env = env.env_named_context,env.env_named_vals +let named_context env = env.env_named_context.env_named_ctx +let named_context_val env = env.env_named_context let rel_context env = env.env_rel_context let opaque_tables env = env.indirect_pterms let set_opaque_tables env indirect_pterms = { env with indirect_pterms } let empty_context env = - match env.env_rel_context, env.env_named_context with + match env.env_rel_context, env.env_named_context.env_named_ctx with | [], [] -> true | _ -> false @@ -99,14 +99,12 @@ let fold_rel_context f env ~init = (* Named context *) -let named_context_of_val = fst -let named_vals_of_val = snd +let named_context_of_val c = c.env_named_ctx (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) -let map_named_val f = - on_fst (Context.Named.map f) +let map_named_val = map_named_val let empty_named_context = Context.Named.empty @@ -118,8 +116,8 @@ let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named id env = Context.Named.lookup id env.env_named_context -let lookup_named_val id (ctxt,_) = Context.Named.lookup id ctxt +let lookup_named = lookup_named +let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) let eq_named_context_val c1 c2 = c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) @@ -139,10 +137,9 @@ let evaluable_named id env = | Some _ -> true | _ -> false -let reset_with_named_context (ctxt,ctxtv) env = +let reset_with_named_context ctxt env = { env with env_named_context = ctxt; - env_named_vals = ctxtv; env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0 } @@ -157,11 +154,11 @@ let pop_rel_context n env = let fold_named_context f env ~init = let rec fold_right env = - match env.env_named_context with - | [] -> init - | d::ctxt -> + match match_named_context_val env.env_named_context with + | None -> init + | Some (d, v, rem) -> let env = - reset_with_named_context (ctxt,List.tl env.env_named_vals) env in + reset_with_named_context rem env in f env d (fold_right env) in fold_right env @@ -493,66 +490,47 @@ let compile_constant_body = Cbytegen.compile_constant_body false exception Hyp_not_found -let apply_to_hyp (ctxt,vals) id f = - let rec aux rtail ctxt vals = - match ctxt, vals with - | d::ctxt, v::vals -> +let apply_to_hyp ctxt id f = + let rec aux rtail ctxt = + match match_named_context_val ctxt with + | Some (d, v, ctxt) -> if Id.equal (get_id d) id then - (f ctxt d rtail)::ctxt, v::vals + push_named_context_val_val (f ctxt.env_named_ctx d rtail) v ctxt else - let ctxt',vals' = aux (d::rtail) ctxt vals in - d::ctxt', v::vals' - | [],[] -> raise Hyp_not_found - | _, _ -> assert false - in aux [] ctxt vals - -let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = - let rec aux ctxt vals = - match ctxt,vals with - | d::ctxt, v::vals -> + let ctxt' = aux (d::rtail) ctxt in + push_named_context_val_val d v ctxt' + | None -> raise Hyp_not_found + in aux [] ctxt + +let apply_to_hyp_and_dependent_on ctxt id f g = + let rec aux sign = + match match_named_context_val sign with + | Some (d, v, sign) -> if Id.equal (get_id d) id then - let sign = ctxt,vals in push_named_context_val (f d sign) sign else - let (ctxt,vals as sign) = aux ctxt vals in + let sign = aux sign in push_named_context_val (g d sign) sign - | [],[] -> raise Hyp_not_found - | _,_ -> assert false - in aux ctxt vals - -let insert_after_hyp (ctxt,vals) id d check = - let rec aux ctxt vals = - match ctxt, vals with - | decl::ctxt', v::vals' -> - if Id.equal (get_id decl) id then begin - check ctxt; - push_named_context_val d (ctxt,vals) - end else - let ctxt,vals = aux ctxt vals in - d::ctxt, v::vals - | [],[] -> raise Hyp_not_found - | _, _ -> assert false - in aux ctxt vals - + | None -> raise Hyp_not_found + in aux ctxt (* To be used in Logic.clear_hyps *) -let remove_hyps ids check_context check_value (ctxt, vals) = - let rec remove_hyps ctxt vals = match ctxt, vals with - | [], [] -> ([], []), false - | d :: rctxt, (nid, v) :: rvals -> - let (ans, seen) = remove_hyps rctxt rvals in +let remove_hyps ids check_context check_value ctxt = + let rec remove_hyps ctxt = match match_named_context_val ctxt with + | None -> empty_named_context_val, false + | Some (d, v, rctxt) -> + let (ans, seen) = remove_hyps rctxt in if Id.Set.mem (get_id d) ids then (ans, true) - else if not seen then (ctxt, vals), false + else if not seen then ctxt, false else - let (rctxt', rvals') = ans in + let rctxt' = ans in let d' = check_context d in let v' = check_value v in - if d == d' && v == v' && rctxt == rctxt' && rvals == rvals' then - (ctxt, vals), true - else (d' :: rctxt', (nid, v') :: rvals'), true - | _ -> assert false + if d == d' && v == v' && rctxt == rctxt' then + ctxt, true + else push_named_context_val_val d' v' rctxt', true in - fst (remove_hyps ctxt vals) + fst (remove_hyps ctxt) (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module diff --git a/kernel/environ.mli b/kernel/environ.mli index 77451d8ea..e23333c06 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -78,7 +78,6 @@ val fold_rel_context : (** {5 Context of variables (section variables and goal assumptions) } *) val named_context_of_val : named_context_val -> Context.Named.t -val named_vals_of_val : named_context_val -> Pre_env.named_vals val val_of_named_context : Context.Named.t -> named_context_val val empty_named_context_val : named_context_val @@ -273,10 +272,6 @@ val apply_to_hyp_and_dependent_on : named_context_val -> variable -> (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) -> named_context_val -val insert_after_hyp : named_context_val -> variable -> - Context.Named.Declaration.t -> - (Context.Named.t -> unit) -> named_context_val - val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 7d76ecf3a..33bd7d8dd 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1860,7 +1860,7 @@ and compile_rel env sigma univ auxdefs n = and compile_named env sigma univ auxdefs id = let open Context.Named.Declaration in - match Context.Named.lookup id env.env_named_context with + match lookup_named id env with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index fefc3222d..72de2f1a6 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -62,12 +62,14 @@ let force_lazy_val vk = match !vk with let dummy_lazy_val () = ref VKnone let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) -type named_vals = (Id.t * lazy_val) list +type named_context_val = { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} type env = { env_globals : globals; - env_named_context : Context.Named.t; - env_named_vals : named_vals; + env_named_context : named_context_val; env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; @@ -78,9 +80,10 @@ type env = { indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = Context.Named.t * named_vals - -let empty_named_context_val = [],[] +let empty_named_context_val = { + env_named_ctx = []; + env_named_map = Id.Map.empty; +} let empty_env = { env_globals = { @@ -88,8 +91,7 @@ let empty_env = { env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; - env_named_context = Context.Named.empty; - env_named_vals = []; + env_named_context = empty_named_context_val; env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0; @@ -126,17 +128,42 @@ let env_of_rel n env = (* Named context *) -let push_named_context_val d (ctxt,vals) = - let rval = ref VKnone in - Context.Named.add d ctxt, (NamedDecl.get_id d,rval)::vals +let push_named_context_val_val d rval ctxt = +(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) + { + env_named_ctx = Context.Named.add d ctxt.env_named_ctx; + env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; + } + +let push_named_context_val d ctxt = + push_named_context_val_val d (ref VKnone) ctxt + +let match_named_context_val c = match c.env_named_ctx with +| [] -> None +| decl :: ctx -> + let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in + let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in + let cval = { env_named_ctx = ctx; env_named_map = map } in + Some (decl, v, cval) + +let map_named_val f ctxt = + let open Context.Named.Declaration in + let fold accu d = + let d' = map_constr f d in + let accu = + if d == d' then accu + else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu + in + (accu, d') + in + let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in + { env_named_ctx = ctx; env_named_map = map } let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); assert (env.env_rel_context = []); *) - let rval = ref VKnone in { env_globals = env.env_globals; - env_named_context = Context.Named.add d env.env_named_context; - env_named_vals = (NamedDecl.get_id d, rval) :: env.env_named_vals; + env_named_context = push_named_context_val d env.env_named_context; env_rel_context = env.env_rel_context; env_rel_val = env.env_rel_val; env_nb_rel = env.env_nb_rel; @@ -147,8 +174,11 @@ let push_named d env = indirect_pterms = env.indirect_pterms; } +let lookup_named id env = + fst (Id.Map.find id env.env_named_context.env_named_map) + let lookup_named_val id env = - snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals) + snd(Id.Map.find id env.env_named_context.env_named_map) (* Warning all the names should be different *) let env_of_named id env = env diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index e551d22c8..866790367 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -40,12 +40,14 @@ val force_lazy_val : lazy_val -> (values * Id.Set.t) option val dummy_lazy_val : unit -> lazy_val val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit -type named_vals = (Id.t * lazy_val) list +type named_context_val = private { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} type env = { env_globals : globals; - env_named_context : Context.Named.t; - env_named_vals : named_vals; + env_named_context : named_context_val; env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; @@ -56,8 +58,6 @@ type env = { indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = Context.Named.t * named_vals - val empty_named_context_val : named_context_val val empty_env : env @@ -73,7 +73,15 @@ val env_of_rel : int -> env -> env val push_named_context_val : Context.Named.Declaration.t -> named_context_val -> named_context_val +val push_named_context_val_val : + Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val +val match_named_context_val : + named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option +val map_named_val : + (constr -> constr) -> named_context_val -> named_context_val + val push_named : Context.Named.Declaration.t -> env -> env +val lookup_named : Id.t -> env -> Context.Named.Declaration.t val lookup_named_val : Id.t -> env -> lazy_val val env_of_named : Id.t -> env -> env diff --git a/library/goptions.ml b/library/goptions.ml index 813bf30a3..8f2f06925 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -208,6 +208,10 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } +type option_locality = OptLocal | OptDefault | OptGlobal + +type option_mod = OptSet | OptAppend + module OptionOrd = struct type t = option_name @@ -238,49 +242,51 @@ let warn_deprecated_option = (fun key -> str "Option" ++ spc () ++ str (nickname key) ++ strbrk " is deprecated") -let declare_option cast uncast +let get_locality = function + | Some true -> OptLocal + | Some false -> OptGlobal + | None -> OptDefault + +let declare_option cast uncast append { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in - (* spiwack: I use two spaces in the nicknames of "local" and "global" objects. - That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are - lists of strings *without* spaces. *) - let (write,lwrite,gwrite) = if sync then - let ldecl_obj = (* "Local": doesn't survive section or modules. *) - declare_object {(default_object ("L "^nickname key)) with - cache_function = (fun (_,v) -> write v); - classify_function = (fun _ -> Dispose)} - in - let decl_obj = (* default locality: survives sections but not modules. *) - declare_object {(default_object (nickname key)) with - cache_function = (fun (_,v) -> write v); - classify_function = (fun _ -> Dispose); - discharge_function = (fun (_,v) -> Some v)} - in - let gdecl_obj = (* "Global": survives section and modules. *) - declare_object {(default_object ("G "^nickname key)) with - cache_function = (fun (_,v) -> write v); - classify_function = (fun v -> Substitute v); - subst_function = (fun (_,v) -> v); - discharge_function = (fun (_,v) -> Some v); - load_function = (fun _ (_,v) -> write v)} - in - let _ = Summary.declare_summary (nickname key) - { Summary.freeze_function = (fun _ -> read ()); - Summary.unfreeze_function = write; - Summary.init_function = (fun () -> write default) } - in - begin fun v -> add_anonymous_leaf (decl_obj v) end , - begin fun v -> add_anonymous_leaf (ldecl_obj v) end , - begin fun v -> add_anonymous_leaf (gdecl_obj v) end - else write,write,write + let change = + if sync then + let _ = Summary.declare_summary (nickname key) + { Summary.freeze_function = (fun _ -> read ()); + Summary.unfreeze_function = write; + Summary.init_function = (fun () -> write default) } in + let cache_options (_,(l,m,v)) = + match m with + | OptSet -> write v + | OptAppend -> write (append (read ()) v) in + let load_options i o = cache_options o in + let subst_options (subst,obj) = obj in + let discharge_options (_,(l,_,_ as o)) = + match l with OptLocal -> None | _ -> Some o in + let classify_options (l,_,_ as o) = + match l with OptGlobal -> Substitute o | _ -> Dispose in + let options : option_locality * option_mod * _ -> obj = + declare_object + { (default_object (nickname key)) with + load_function = load_options; + cache_function = cache_options; + subst_function = subst_options; + discharge_function = discharge_options; + classify_function = classify_options } in + (fun l m v -> Lib.add_anonymous_leaf (options (l, m, v))) + else + (fun _ m v -> + match m with + | OptSet -> write v + | OptAppend -> write (append (read ()) v)) in let warn () = if depr then warn_deprecated_option key in let cread () = cast (read ()) in - let cwrite v = warn (); write (uncast v) in - let clwrite v = warn (); lwrite (uncast v) in - let cgwrite v = warn (); gwrite (uncast v) in - value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab; + let cwrite l v = warn (); change l OptSet (uncast v) in + let cappend l v = warn (); change l OptAppend (uncast v) in + value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,cappend)) !value_tab; write type 'a write_function = 'a -> unit @@ -289,18 +295,22 @@ let declare_int_option = declare_option (fun v -> IntValue v) (function IntValue v -> v | _ -> anomaly (Pp.str "async_option")) + (fun _ _ -> anomaly (Pp.str "async_option")) let declare_bool_option = declare_option (fun v -> BoolValue v) (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option")) + (fun _ _ -> anomaly (Pp.str "async_option")) let declare_string_option = declare_option (fun v -> StringValue v) (function StringValue v -> v | _ -> anomaly (Pp.str "async_option")) + (fun x y -> x^","^y) let declare_stringopt_option = declare_option (fun v -> StringOptValue v) (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option")) + (fun _ _ -> anomaly (Pp.str "async_option")) (* 3- User accessible commands *) @@ -315,13 +325,8 @@ let set_option_value locality check_and_cast key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key - | Some (name, depr, (_,read,write,lwrite,gwrite)) -> - let write = match locality with - | None -> write - | Some true -> lwrite - | Some false -> gwrite - in - write (check_and_cast v (read ())) + | Some (name, depr, (_,read,write,append)) -> + write (get_locality locality) (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option." @@ -357,6 +362,13 @@ let set_string_option_value_gen locality = let unset_option_value_gen locality key = set_option_value locality check_unset_value key () +let set_string_option_append_value_gen locality key v = + let opt = try Some (get_option key) with Not_found -> None in + match opt with + | None -> warn_unknown_option key + | Some (name, depr, (_,read,write,append)) -> + append (get_locality locality) (check_string_value v (read ())) + let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None let set_string_option_value = set_string_option_value_gen None @@ -375,7 +387,7 @@ let msg_option_value (name,v) = (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = - let (name, depr, (_,read,_,_,_)) = get_option key in + let (name, depr, (_,read,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> @@ -385,7 +397,7 @@ let print_option_value key = let get_tables () = let tables = !value_tab in - let fold key (name, depr, (sync,read,_,_,_)) accu = + let fold key (name, depr, (sync,read,_,_)) accu = let state = { opt_sync = sync; opt_name = name; @@ -404,13 +416,13 @@ let print_tables () = in str "Synchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name, depr, (sync,read,_,_,_)) p -> + (fun key (name, depr, (sync,read,_,_)) p -> if sync then p ++ print_option key name (read ()) depr else p) !value_tab (mt ()) ++ str "Asynchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name, depr, (sync,read,_,_,_)) p -> + (fun key (name, depr, (sync,read,_,_)) p -> if sync then p else p ++ print_option key name (read ()) depr) !value_tab (mt ()) ++ diff --git a/library/goptions.mli b/library/goptions.mli index 26864503b..ca2df0710 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -154,6 +154,7 @@ val get_ref_table : val set_int_option_value_gen : bool option -> option_name -> int option -> unit val set_bool_option_value_gen : bool option -> option_name -> bool -> unit val set_string_option_value_gen : bool option -> option_name -> string -> unit +val set_string_option_append_value_gen : bool option -> option_name -> string -> unit val unset_option_value_gen : bool option -> option_name -> unit val set_int_option_value : option_name -> int option -> unit diff --git a/library/lib.ml b/library/lib.ml index 9401bc55b..4fd29a94d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -234,11 +234,16 @@ let add_leaves id objs = List.iter add_obj objs; oname -let add_anonymous_leaf obj = +let add_anonymous_leaf ?(cache_first = true) obj = let id = anonymous_id () in let oname = make_oname id in - cache_object (oname,obj); - add_entry oname (Leaf obj) + if cache_first then begin + cache_object (oname,obj); + add_entry oname (Leaf obj) + end else begin + add_entry oname (Leaf obj); + cache_object (oname,obj) + end let add_frozen_state () = add_anonymous_entry diff --git a/library/lib.mli b/library/lib.mli index 845727059..9f9d8c7e5 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -54,7 +54,7 @@ val segment_of_objects : current list of operations (most recent ones coming first). *) val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name -val add_anonymous_leaf : Libobject.obj -> unit +val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 542f8f067..f19759470 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -479,6 +479,14 @@ let find_keyword loc id s = | None -> raise Not_found | Some c -> KEYWORD c +let process_sequence loc bp c cs = + let rec aux n cs = + match Stream.peek cs with + | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs + | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs) + in + aux 1 cs + (* Must be a special token *) let process_chars loc bp c cs = let t = progress_from_byte loc None (-1) !token_tree cs c in @@ -544,6 +552,12 @@ let rec next_token loc = parser bp | _ -> () in (t, set_loc_pos loc bp ep) + | [< ' ('-'|'+'|'*' as c); s >] -> + let t,new_between_com = + if !between_com then process_sequence loc bp c s, true + else process_chars loc bp c s,false + in + comment_stop bp; between_com := new_between_com; t | [< ''?'; s >] ep -> let t = parse_after_qmark loc bp s in comment_stop bp; (t, set_loc_pos loc ep bp) diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index a3d0e7133..389c34fa5 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -259,6 +259,7 @@ IFDEF CAMLP5 THEN | Tok.INT s -> "INT", s | Tok.STRING s -> "STRING", s | Tok.LEFTQMARK -> "LEFTQMARK", "" + | Tok.BULLET s -> "BULLET", s | Tok.EOI -> "EOI", "" in Gramext.Stoken pattern diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0b9d4622a..ad6ad9340 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -33,6 +33,8 @@ let _ = List.iter CLexer.add_keyword vernac_kw let query_command = Gram.entry_create "vernac:query_command" +let subprf = Gram.entry_create "vernac:subprf" + let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" let thm_token = Gram.entry_create "vernac:thm_token" let def_body = Gram.entry_create "vernac:def_body" @@ -43,25 +45,13 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" -let subprf = Gram.Entry.of_parser "vernac:subprf" (fun strm -> - match get_tok (Stream.peek strm) with - | Some (KEYWORD "{") -> Stream.junk strm; VernacSubproof None - | Some (KEYWORD "}") -> Stream.junk strm; VernacEndSubproof - | Some (KEYWORD k) -> - (match k.[0] with - | ('-'|'+'|'*') as c -> - let n = String.length k in - for i = 1 to n - 1 do - if k.[i] != c then raise Stream.Failure - done; - Stream.junk strm; - VernacBullet (match c with - | '-' -> Dash n - | '+' -> Plus n - | '*' -> Star n - | _ -> assert false) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) +let make_bullet s = + let n = String.length s in + match s.[0] with + | '-' -> Dash n + | '+' -> Plus n + | '*' -> Star n + | _ -> assert false GEXTEND Gram GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; @@ -112,6 +102,13 @@ GEXTEND Gram [ [ c = subgoal_command -> c None] ] ; + subprf: + [ [ s = BULLET -> VernacBullet (make_bullet s) + | "{" -> VernacSubproof None + | "}" -> VernacEndSubproof + ] ] + ; + subgoal_command: [ [ c = query_command; "." -> begin function @@ -854,6 +851,8 @@ GEXTEND Gram (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> VernacSetOption (table,v) + | "Set"; table = option_table; "Append"; v = STRING -> + VernacSetAppendOption (table,v) | "Set"; table = option_table -> VernacSetOption (table,BoolValue true) | IDENT "Unset"; table = option_table -> diff --git a/parsing/tok.ml b/parsing/tok.ml index 99d5c972c..f4b60aeec 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -18,6 +18,7 @@ type t = | INT of string | STRING of string | LEFTQMARK + | BULLET of string | EOI let equal t1 t2 = match t1, t2 with @@ -29,6 +30,7 @@ let equal t1 t2 = match t1, t2 with | INT s1, INT s2 -> string_equal s1 s2 | STRING s1, STRING s2 -> string_equal s1 s2 | LEFTQMARK, LEFTQMARK -> true +| BULLET s1, BULLET s2 -> string_equal s1 s2 | EOI, EOI -> true | _ -> false @@ -40,6 +42,7 @@ let extract_string = function | FIELD s -> s | INT s -> s | LEFTQMARK -> "?" + | BULLET s -> s | EOI -> "" let to_string = function @@ -50,6 +53,7 @@ let to_string = function | INT s -> Format.sprintf "INT %s" s | STRING s -> Format.sprintf "STRING %S" s | LEFTQMARK -> "LEFTQMARK" + | BULLET s -> Format.sprintf "BULLET %S" s | EOI -> "EOI" let match_keyword kwd = function @@ -71,6 +75,7 @@ let of_pattern = function | "INT", s -> INT s | "STRING", s -> STRING s | "LEFTQMARK", _ -> LEFTQMARK + | "BULLET", s -> BULLET s | "EOI", _ -> EOI | _ -> failwith "Tok.of_pattern: not a constructor" @@ -82,6 +87,7 @@ let to_pattern = function | INT s -> "INT", s | STRING s -> "STRING", s | LEFTQMARK -> "LEFTQMARK", "" + | BULLET s -> "BULLET", s | EOI -> "EOI", "" let match_pattern = @@ -94,6 +100,7 @@ let match_pattern = | "INT", "" -> (function INT s -> s | _ -> err ()) | "STRING", "" -> (function STRING s -> s | _ -> err ()) | "LEFTQMARK", "" -> (function LEFTQMARK -> "" | _ -> err ()) + | "BULLET", "" -> (function BULLET s -> s | _ -> err ()) | "EOI", "" -> (function EOI -> "" | _ -> err ()) | pat -> let tok = of_pattern pat in diff --git a/parsing/tok.mli b/parsing/tok.mli index b1e79dc90..b9286c53e 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -16,6 +16,7 @@ type t = | INT of string | STRING of string | LEFTQMARK + | BULLET of string | EOI val equal : t -> t -> bool diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 72baa3493..0d30b3e4c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2577,6 +2577,9 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e typing_function = typing_fun } in let j = compile pb in + + (* We coerce to the tycon (if an elim predicate was provided) *) + let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in evdref := !myevdref; j in @@ -2587,6 +2590,4 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; - (* We coerce to the tycon (if an elim predicate was provided) *) - inh_conv_coerce_to_tycon loc env evdref j tycon - + j diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5653b5675..5d6c41103 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1588,7 +1588,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let x = id_of_name_using_hdchar (Global.env()) t name in let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else - if mem_named_context x (named_context env) then + if mem_named_context_val x (named_context_val env) then user_err ~hdr:"Unification.make_abstraction_core" (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") else diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index aa0ebbb83..fa5a70899 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -370,13 +370,13 @@ end) = struct let n = begin_of_binders bl in match bl with | [LocalRawAssum (nal,k,t)] -> - pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) + kw n ++ pr_binder false pr_c (nal,k,t) | (LocalRawAssum _ | LocalPattern _) :: _ as bdl -> - pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl + kw n ++ pr_undelimited_binders sep pr_c bdl | _ -> assert false let pr_binders_gen pr_c sep is_open = - if is_open then pr_delimited_binders mt sep pr_c + if is_open then pr_delimited_binders pr_com_at sep pr_c else pr_undelimited_binders sep pr_c let rec extract_prod_binders = function @@ -525,9 +525,9 @@ end) = struct prlist_with_sep pr_semicolon (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l - let pr_forall () = keyword "forall" ++ spc () + let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc () - let pr_fun () = keyword "fun" ++ spc () + let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc () let pr_fun_sep = spc () ++ str "=>" diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 1cdf55ac6..7c00106e2 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1108,6 +1108,11 @@ module Make return ( hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v) ) + | VernacSetAppendOption (na,v) -> + return ( + hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ + spc() ++ keyword "Append" ++ spc() ++ str v) + ) | VernacAddOption (na,l) -> return ( hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l)) diff --git a/proofs/logic.ml b/proofs/logic.ml index d23a4ad61..44c629484 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -541,7 +541,7 @@ let prim_refiner r sigma goal = nexthyp, t,cl,sigma else - (if !check && mem_named_context id (named_context_of_val sign) then + (if !check && mem_named_context_val id sign then user_err ~hdr:"Logic.prim_refiner" (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 904e22681..e41fb94cc 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -189,9 +189,9 @@ module New = struct next_ident_away id ids let pf_get_hyp id gl = - let hyps = Proofview.Goal.hyps gl in + let hyps = Proofview.Goal.env gl in let sign = - try Context.Named.lookup id hyps + try Environ.lookup_named id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index fa7acd00a..dc5be08a3 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -181,7 +181,7 @@ let rec classify_vernac e = | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ + | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _ | VernacAddOption _ | VernacRemoveOption _ | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index f9f8e8715..96767e7f6 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -45,7 +45,11 @@ let typeclasses_modulo_eta = ref false let set_typeclasses_modulo_eta d = (:=) typeclasses_modulo_eta d let get_typeclasses_modulo_eta () = !typeclasses_modulo_eta -let typeclasses_limit_intros = ref false +(** When this flag is enabled, the resolution of type classes tries to avoid + useless introductions. This is no longer useful since we have eta, but is + here for compatibility purposes. Another compatibility issues is that the + cost (in terms of search depth) can differ. *) +let typeclasses_limit_intros = ref true let set_typeclasses_limit_intros d = (:=) typeclasses_limit_intros d let get_typeclasses_limit_intros () = !typeclasses_limit_intros @@ -57,31 +61,22 @@ let typeclasses_iterative_deepening = ref false let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening -let get_compat_version d = - match d with - | "8.5" -> Flags.V8_5 - | _ -> Flags.Current - -let typeclasses_unif_compat = ref Flags.V8_5 -let set_typeclasses_unif_compat d = - if d == Flags.Current then set_typeclasses_limit_intros false - else set_typeclasses_limit_intros true; - (:=) typeclasses_unif_compat d - -let get_typeclasses_unif_compat () = !typeclasses_unif_compat -let set_typeclasses_unif_compat_string d = - set_typeclasses_unif_compat (get_compat_version d) -let get_typeclasses_unif_compat_string () = - Flags.pr_version (get_typeclasses_unif_compat ()) - -let typeclasses_compat = ref Flags.Current -let set_typeclasses_compat d = (:=) typeclasses_compat d -let get_typeclasses_compat () = !typeclasses_compat -let set_typeclasses_compat_string d = - set_typeclasses_compat (get_compat_version d) - -let get_typeclasses_compat_string () = - Flags.pr_version (get_typeclasses_compat ()) +(** [typeclasses_filtered_unif] governs the unification algorithm used by type + classes. If enabled, a new algorithm based on pattern filtering and refine + will be used. When disabled, the previous algorithm based on apply will be + used. *) +let typeclasses_filtered_unification = ref false +let set_typeclasses_filtered_unification d = + (:=) typeclasses_filtered_unification d +let get_typeclasses_filtered_unification () = + !typeclasses_filtered_unification + +(** [typeclasses_legacy_resolution] falls back to the 8.5 resolution algorithm, + instead of the 8.6 one which uses the native backtracking facilities of the + proof engine. *) +let typeclasses_legacy_resolution = ref false +let set_typeclasses_legacy_resolution d = (:=) typeclasses_legacy_resolution d +let get_typeclasses_legacy_resolution () = !typeclasses_legacy_resolution let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0) let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false @@ -135,22 +130,22 @@ let _ = optwrite = set_typeclasses_iterative_deepening; } let _ = - declare_string_option + declare_bool_option { optsync = true; optdepr = false; optname = "compat"; - optkey = ["Typeclasses";"Compatibility"]; - optread = get_typeclasses_compat_string; - optwrite = set_typeclasses_compat_string; } + optkey = ["Typeclasses";"Legacy";"Resolution"]; + optread = get_typeclasses_legacy_resolution; + optwrite = set_typeclasses_legacy_resolution; } let _ = - declare_string_option + declare_bool_option { optsync = true; optdepr = false; optname = "compat"; - optkey = ["Typeclasses";"Unification";"Compatibility"]; - optread = get_typeclasses_unif_compat_string; - optwrite = set_typeclasses_unif_compat_string; } + optkey = ["Typeclasses";"Filtered";"Unification"]; + optread = get_typeclasses_filtered_unification; + optwrite = set_typeclasses_filtered_unification; } let set_typeclasses_debug = declare_bool_option @@ -402,7 +397,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) -> let tac = function | Res_pf (term,cl) -> - if get_typeclasses_unif_compat () = Flags.Current then + if get_typeclasses_filtered_unification () then let tac = with_prods nprods poly (term,cl) ({ enter = fun gl clenv -> @@ -412,13 +407,13 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = else let tac = with_prods nprods poly (term,cl) (unify_resolve poly flags) in - if get_typeclasses_compat () = Flags.V8_5 then + if get_typeclasses_legacy_resolution () then Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) | ERes_pf (term,cl) -> - if get_typeclasses_unif_compat () = Flags.Current then + if get_typeclasses_filtered_unification () then let tac = (with_prods nprods poly (term,cl) ({ enter = fun gl clenv -> (matches_pattern concl p) <*> @@ -427,7 +422,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = else let tac = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in - if get_typeclasses_compat () = Flags.V8_5 then + if get_typeclasses_legacy_resolution () then Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else Proofview.tclBIND (Proofview.with_shelf tac) @@ -447,7 +442,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in let pp = match p with - | Some pat when get_typeclasses_unif_compat () = Flags.Current -> + | Some pat when get_typeclasses_filtered_unification () -> str " with pattern " ++ Printer.pr_constr_pattern pat | _ -> mt () in @@ -1293,7 +1288,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) in let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in - if get_typeclasses_compat () = Flags.V8_5 then + if get_typeclasses_legacy_resolution () then Proofview.V82.tactic (fun gl -> try V85.eauto85 depth ~only_classes ~st dbs gl @@ -1419,10 +1414,10 @@ let resolve_all_evars debug depth unique env p oevd do_split fail = let p = select_and_update_evars p oevd (in_comp comp) in try let evd' = - if get_typeclasses_compat () = Flags.Current then - Search.typeclasses_resolve debug depth unique p evd - else + if get_typeclasses_legacy_resolution () then V85.resolve_all_evars_once debug depth unique p evd + else + Search.typeclasses_resolve debug depth unique p evd in if has_undefined p oevd evd' then raise Unresolved; docomp evd' comps @@ -1467,12 +1462,13 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = let st = Hint_db.transparent_state hints in let depth = get_typeclasses_depth () in let gls' = - if get_typeclasses_compat () = Flags.Current then + if get_typeclasses_legacy_resolution () then + V85.eauto85 depth ~st [hints] gls + else try Proofview.V82.of_tactic (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls with Refiner.FailError _ -> raise Not_found - else V85.eauto85 depth ~st [hints] gls in let evd = sig_sig gls' in let t' = let (ev, inst) = destEvar t in diff --git a/tactics/equality.ml b/tactics/equality.ml index 444fac170..7c819edad 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -702,16 +702,16 @@ let replace_in_clause_maybe_by c1 c2 cl tac_opt = exception DiscrFound of (constructor * int) list * constructor * constructor -let injection_on_proofs = ref false +let keep_proof_equalities_for_injection = ref false let _ = declare_bool_option { optsync = true; optdepr = false; optname = "injection on prop arguments"; - optkey = ["Injection";"On";"Proofs"]; - optread = (fun () -> !injection_on_proofs) ; - optwrite = (fun b -> injection_on_proofs := b) } + optkey = ["Keep";"Proof";"Equalities"]; + optread = (fun () -> !keep_proof_equalities_for_injection) ; + optwrite = (fun b -> keep_proof_equalities_for_injection := b) } let find_positions env sigma t1 t2 = @@ -756,7 +756,7 @@ let find_positions env sigma t1 t2 = project env sorts posn t1_0 t2_0 in try - let sorts = if !injection_on_proofs then [InSet;InType;InProp] + let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp] else [InSet;InType] in Inr (findrec sorts [] t1 t2) @@ -1390,7 +1390,10 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = | Inl _ -> tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.") | Inr [] -> - let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in + let suggestion = + if !keep_proof_equalities_for_injection then + "" else + " You can try to use option Set Keep Proof Equalities." in tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)) | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 -> tclZEROMSG (str"Nothing to inject.") diff --git a/tactics/leminv.ml b/tactics/leminv.ml index d80e86241..10fc5076c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -204,11 +204,11 @@ let inversion_scheme env sigma t sort dep_option inv_op = tclTHEN intro (onLastHypId inv_op)) pf) in let pfterm = List.hd (Proof.partial_proof pf) in - let global_named_context = Global.named_context () in + let global_named_context = Global.named_context_val () in let ownSign = ref begin fold_named_context (fun env d sign -> - if mem_named_context (NamedDecl.get_id d) global_named_context then sign + if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bd92e9794..8e7f4613c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -181,10 +181,10 @@ let introduction ?(check=true) id = let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in - let hyps = Proofview.Goal.hyps gl in + let hyps = named_context_val (Proofview.Goal.env gl) in let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in - let () = if check && mem_named_context id hyps then + let () = if check && mem_named_context_val id hyps then user_err ~hdr:"Tactics.introduction" (str "Variable " ++ pr_id id ++ str " is already declared.") in @@ -520,7 +520,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl -> let (sp', u') = check_mutind env sigma n ar in if not (eq_mind sp sp') then error "Fixpoints should be on the same mutual inductive declaration."; - if mem_named_context f (named_context_of_val sign) then + if mem_named_context_val f sign then user_err ~hdr:"Logic.prim_refiner" (str "Name " ++ pr_id f ++ str " already used in the environment"); mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth @@ -573,7 +573,7 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl -> | [] -> sign | (f, ar) :: oth -> let open Context.Named.Declaration in - if mem_named_context f (named_context_of_val sign) then + if mem_named_context_val f sign then error "Name already used in the environment."; mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth in @@ -2791,7 +2791,7 @@ let old_generalize_dep ?(with_let=false) c gl = let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in let tothin' = match kind_of_term c with - | Var id when mem_named_context id sign && not (Id.List.mem id init_ids) + | Var id when mem_named_context_val id (val_of_named_context sign) && not (Id.List.mem id init_ids) -> id::tothin | _ -> tothin in @@ -2945,8 +2945,8 @@ let unfold_body x = let open Context.Named.Declaration in Proofview.Goal.enter { enter = begin fun gl -> (** We normalize the given hypothesis immediately. *) - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let xval = match Context.Named.lookup x hyps with + let env = Proofview.Goal.env (Proofview.Goal.assume gl) in + let xval = match Environ.lookup_named x env with | LocalAssum _ -> user_err ~hdr:"unfold_body" (pr_id x ++ str" is not a defined hypothesis.") | LocalDef (_,xval,_) -> xval @@ -4364,7 +4364,7 @@ let induction_gen clear_flag isrec with_evars elim let cls = Option.default allHypsAndConcl cls in let t = typ_of env sigma c in let is_arg_pure_hyp = - isVar c && not (mem_named_context (destVar c) (Global.named_context())) + isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ())) && lbind == NoBindings && not with_evars && Option.is_empty eqname && clear_flag == None && has_generic_occurrences_but_goal cls (destVar c) env ccl in @@ -4411,7 +4411,7 @@ let induction_gen_l isrec with_evars elim names lc = | [] -> Proofview.tclUNIT () | c::l' -> match kind_of_term c with - | Var id when not (mem_named_context id (Global.named_context())) + | Var id when not (mem_named_context_val id (Global.named_context_val ())) && not with_evars -> let _ = newlc:= id::!newlc in atomize_list l' @@ -4831,7 +4831,7 @@ let abstract_subproof id gk tac = let open Proofview.Notations in Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let current_sign = Global.named_context() + let current_sign = Global.named_context_val () and global_sign = Proofview.Goal.hyps gl in let sigma = Sigma.to_evar_map sigma in let evdref = ref sigma in @@ -4839,8 +4839,8 @@ let abstract_subproof id gk tac = List.fold_right (fun d (s1,s2) -> let id = NamedDecl.get_id d in - if mem_named_context id current_sign && - interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d + if mem_named_context_val id current_sign && + interpretable_as_section_decl evdref (lookup_named_val id current_sign) d then (s1,push_named_context_val d s2) else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, empty_named_context_val) in diff --git a/test-suite/bugs/closed/4970.v b/test-suite/bugs/closed/4970.v new file mode 100644 index 000000000..7a896582f --- /dev/null +++ b/test-suite/bugs/closed/4970.v @@ -0,0 +1,3 @@ +(* Check "{{" is not confused with "{" in notations *) +Reserved Notation "x {{ y }}" (at level 40). +Notation "x {{ y }}" := (x y) (only parsing). diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 8745cf2fb..da2183841 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -135,6 +135,21 @@ intros * [= H]. exact H. Abort. +(* Test the Keep Proof Equalities option. *) +Set Keep Proof Equalities. +Unset Structural Injection. + +Inductive pbool : Prop := Pbool1 | Pbool2. + +Inductive pbool_shell : Set := Pbsc : pbool -> pbool_shell. + +Goal Pbsc Pbool1 = Pbsc Pbool2 -> True. +injection 1. +match goal with + |- Pbool1 = Pbool2 -> True => idtac | |- True => fail +end. +Abort. + (* Injection does not project at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index c9c7c611c..4db547f4e 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -117,7 +117,7 @@ Lemma simpl_plus_l_rr1 : Undo. Set Typeclasses Debug. Set Typeclasses Iterative Deepening. - Time typeclasses eauto 2 with nocore. Show Proof. + Time typeclasses eauto 6 with nocore. Show Proof. Undo. Time eauto. (* does EApply H *) Qed. diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v index 8336f6a80..25ee81b58 100644 --- a/test-suite/success/subst.v +++ b/test-suite/success/subst.v @@ -23,3 +23,20 @@ subst. change (y = S (S y)) in H0. change (S y = y). Abort. + +(* A bug revealed by OCaml 4.03 warnings *) +(* fixes in 4e3d464 and 89ec88f for v8.5, 4e3d4646 and 89ec88f1e for v8.6 *) +Goal forall y, let x:=0 in y=x -> y=y. +intros * H; +(* This worked as expected *) +subst. +Fail clear H. +Abort. + +Goal forall y, let x:=0 in x=y -> y=y. +intros * H; +(* Before the fix, this unfolded x instead of + substituting y and erasing H *) +subst. +Fail clear H. +Abort. diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 54aeeaa11..74b416aae 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -23,6 +23,11 @@ Global Unset Shrink Abstract. Global Unset Shrink Obligations. Global Set Refolding Reduction. +(** The resolution algorithm for type classes has changed. *) +Global Set Typeclasses Legacy Resolution. +Global Set Typeclasses Limit Intros. +Global Unset Typeclasses Filtered Unification. + (** In Coq 8.5, [] meant Vector, and [ ] meant list. Restore this behavior, to allow user-defined [] to not override vector notations. See https://coq.inria.fr/bugs/show_bug.cgi?id=4785. *) diff --git a/theories/Logic/PropExtensionalityFacts.v b/theories/Logic/PropExtensionalityFacts.v new file mode 100644 index 000000000..6438fcd40 --- /dev/null +++ b/theories/Logic/PropExtensionalityFacts.v @@ -0,0 +1,88 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Some facts and definitions about propositional and predicate extensionality + +We investigate the relations between the following extensionality principles + +- Provable-proposition extensionality +- Predicate extensionality +- Propositional functional extensionality + +Table of contents + +1. Definitions + +2.1 Predicate extensionality <-> Proposition extensionality + Propositional functional extensionality + +2.2 Propositional extensionality -> Provable propositional extensionality +*) + +Set Implicit Arguments. + +(**********************************************************************) +(** * Definitions *) + +(** Propositional extensionality *) + +Local Notation PropositionalExtensionality := + (forall A B : Prop, (A <-> B) -> A = B). + +(** Provable-proposition extensionality *) + +Local Notation ProvablePropositionExtensionality := + (forall A:Prop, A -> A = True). + +(** Predicate extensionality *) + +Local Notation PredicateExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q). + +(** Propositional functional extensionality *) + +Local Notation PropositionalFunctionalExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x = Q x) -> P = Q). + +(**********************************************************************) +(** * Propositional and predicate extensionality *) + +(**********************************************************************) +(** ** Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality *) + +Lemma PredExt_imp_PropExt : PredicateExtensionality -> PropositionalExtensionality. +Proof. + intros Ext A B Equiv. + change A with ((fun _ => A) I). + now rewrite Ext with (P := fun _ : True =>A) (Q := fun _ => B). +Qed. + +Lemma PredExt_imp_PropFunExt : PredicateExtensionality -> PropositionalFunctionalExtensionality. +Proof. + intros Ext A P Q Eq. apply Ext. intros x. now rewrite (Eq x). +Qed. + +Lemma PropExt_and_PropFunExt_imp_PredExt : + PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality. +Proof. + intros Ext FunExt A P Q Equiv. + apply FunExt. intros x. now apply Ext. +Qed. + +Theorem PropExt_and_PropFunExt_iff_PredExt : + PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality. +Proof. + firstorder using PredExt_imp_PropExt, PredExt_imp_PropFunExt, PropExt_and_PropFunExt_imp_PredExt. +Qed. + +(**********************************************************************) +(** ** Propositional extensionality + Provable proposition extensionality *) + +Lemma PropExt_imp_ProvPropExt : PropositionalExtensionality -> ProvablePropositionExtensionality. +Proof. + intros Ext A Ha; apply Ext; split; trivial. +Qed. diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index ec45c7ed8..f28ef3f65 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -899,12 +899,12 @@ let warn_non_reversible_notation = (fun () -> strbrk "This notation will not be used for printing as it is not reversible.") -let is_not_printable onlyparse noninjective = function +let is_not_printable onlyparse nonreversible = function | NVar _ -> if not onlyparse then warn_notation_bound_to_variable (); true | _ -> - if not onlyparse && noninjective then + if not onlyparse && nonreversible then (warn_non_reversible_notation (); true) else onlyparse @@ -1102,7 +1102,10 @@ let contract_notation ntn = let rec aux ntn i = if i <= String.length ntn - 5 then let ntn' = - if String.is_sub "{ _ }" ntn i then + if String.is_sub "{ _ }" ntn i && + (i = 0 || ntn.[i-1] = ' ') && + (i = String.length ntn - 5 || ntn.[i+5] = ' ') + then String.sub ntn 0 i ^ "_" ^ String.sub ntn (i+5) (String.length ntn -i-5) else ntn in @@ -1191,12 +1194,11 @@ let add_notation_in_scope local df c mods scope = let nenv = { ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map recvars; - ninterp_only_parse = false; } in - let (acvars, ac) = interp_notation_constr nenv c in + let (acvars, ac, reversible) = interp_notation_constr nenv c in let interp = make_interpretation_vars recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in + let onlyparse = is_not_printable onlyparse (not reversible) ac in let notation = { notobj_local = local; notobj_scope = scope; @@ -1231,12 +1233,11 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let nenv = { ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map recvars; - ninterp_only_parse = false; } in - let (acvars, ac) = interp_notation_constr ~impls nenv c in + let (acvars, ac, reversible) = interp_notation_constr ~impls nenv c in let interp = make_interpretation_vars recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in + let onlyparse = is_not_printable onlyparse (not reversible) ac in let notation = { notobj_local = local; notobj_scope = scope; @@ -1373,10 +1374,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse = let nenv = { ninterp_var_type = i_vars; ninterp_rec_vars = Id.Map.empty; - ninterp_only_parse = false; } in - let nvars, pat = interp_notation_constr nenv c in - let () = nonprintable := nenv.ninterp_only_parse in + let nvars, pat, reversible = interp_notation_constr nenv c in + let () = nonprintable := not reversible in let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in List.map map vars, pat in diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 6b62f7aeb..2396cf04a 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -411,7 +411,7 @@ let inMLModule : ml_module_object -> obj = let declare_ml_modules local l = let l = List.map mod_of_name l in - Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l}) + Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l}) let print_ml_path () = let l = !coq_mlpath_copy in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3b14f597c..9415ade28 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1154,7 +1154,6 @@ let vernac_declare_arguments locality r l nargs flags = let default_env () = { Notation_term.ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; - ninterp_only_parse = false; } let vernac_reserve bl = @@ -1163,7 +1162,7 @@ let vernac_reserve bl = let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in - let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in + let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl @@ -1457,6 +1456,9 @@ let vernac_set_option locality key = function | IntValue n -> set_int_option_value_gen locality key n | BoolValue b -> set_bool_option_value_gen locality key b +let vernac_set_append_option locality key s = + set_string_option_append_value_gen locality key s + let vernac_unset_option locality key = unset_option_value_gen locality key @@ -1926,6 +1928,7 @@ let interp ?proof ~loc locality poly c = | VernacSetOpacity qidl -> vernac_set_opacity locality qidl | VernacSetStrategy l -> vernac_set_strategy locality l | VernacSetOption (key,v) -> vernac_set_option locality key v + | VernacSetAppendOption (key,v) -> vernac_set_append_option locality key v | VernacUnsetOption key -> vernac_unset_option locality key | VernacRemoveOption (key,v) -> vernac_remove_option key v | VernacAddOption (key,v) -> vernac_add_option key v @@ -1998,7 +2001,7 @@ let check_vernac_supports_locality c l = | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacSetOption _ | VernacUnsetOption _ + | VernacSetOption _ | VernacSetAppendOption _ | VernacUnsetOption _ | VernacDeclareReduction _ | VernacExtend _ | VernacInductive _) -> () |