diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-24 13:14:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-24 13:14:17 +0000 |
| commit | c789e243ff599db876e94a5ab2a13ff98baa0d6c (patch) | |
| tree | 6dffe51299d60f2fb9ad8fa0a90c5b8a2cd119d9 | |
| parent | 61222d6bfb2fddd8608bea4056af2e9541819510 (diff) | |
Some dead code removal, thanks to Oug analyzer
In particular, the unused lib/tlm.ml and lib/gset.ml are removed
In addition, to simplify code, Libobject.record_object returning only the
('a->obj) function, which is enough almost all the time.
Use Libobject.record_object_full if you really need also the (obj->'a).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
115 files changed, 81 insertions, 1615 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 0e5eb0c23..70f16158e 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -135,16 +135,6 @@ let delta_of_mp resolve mp = | _ -> anomaly "mod_subst: bad association in delta_resolver" with Not_found -> mp - -let delta_of_kn resolve kn = - try - match Deltamap.find (KN kn) resolve with - | Equiv kn1 -> kn1 - | Inline _ -> kn - | _ -> anomaly - "mod_subst: bad association in delta_resolver" - with - Not_found -> kn let remove_mp_delta_resolver resolver mp = Deltamap.remove (MP mp) resolver diff --git a/dev/printers.mllib b/dev/printers.mllib index 3f489a95b..a244b7979 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -13,11 +13,9 @@ Dyn System Envars Store -Gset Gmap Fset Fmap -Tlm Gmapl Profile Explore diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 2cbef98e8..18f1d13ea 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -202,75 +202,6 @@ and check_same_fix_binder bl1 bl2 = let same c d = try check_same_type c d; true with _ -> false -(* Idem for rawconstr *) - -let array_iter2 f v1 v2 = - List.iter2 f (Array.to_list v1) (Array.to_list v2) - -let rec same_patt p1 p2 = - match p1, p2 with - PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar" - | PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) -> - if c1<>c2 || al1 <> al2 then failwith "PatCstr"; - List.iter2 same_patt pl1 pl2 - | _ -> failwith "same_patt" - -let rec same_raw c d = - match c,d with - | RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef" - | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar" - | REvar(_,e1,a1), REvar(_,e2,a2) -> - if e1 <> e2 then failwith "REvar"; - Option.iter2(List.iter2 same_raw) a1 a2 - | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar" - | RApp(_,f1,a1), RApp(_,f2,a2) -> - List.iter2 same_raw (f1::a1) (f2::a2) - | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) -> - if na1 <> na2 then failwith "RLambda"; - same_raw t1 t2; same_raw m1 m2 - | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) -> - if na1 <> na2 then failwith "RProd"; - same_raw t1 t2; same_raw m1 m2 - | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) -> - if na1 <> na2 then failwith "RLetIn"; - same_raw t1 t2; same_raw m1 m2 - | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) -> - List.iter2 - (fun (t1,(al1,oind1)) (t2,(al2,oind2)) -> - same_raw t1 t2; - if al1 <> al2 then failwith "RCases"; - Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) -> - if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2; - List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) -> - List.iter2 same_patt pl1 pl2; - same_raw b1 b2) b1 b2 - | RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) -> - if nl1<>nl2 then failwith "RLetTuple"; - same_raw b1 b2; - same_raw c1 c2 - | RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) -> - same_raw b1 b2; same_raw t1 t2; same_raw e1 e2 - | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) -> - if fk1 <> fk2 || na1 <> na2 then failwith "RRec"; - array_iter2 - (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) -> - if na1<>na2 then failwith "RRec"; - Option.iter2 same_raw bd1 bd2; - same_raw ty1 ty2)) bl1 bl2; - array_iter2 same_raw ty1 ty2; - array_iter2 same_raw def1 def2 - | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort" - | RHole _, _ -> () - | _, RHole _ -> () - | RCast(_,c1,_),r2 -> same_raw c1 r2 - | r1, RCast(_,c2,_) -> same_raw r1 c2 - | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic" - | _ -> failwith "same_raw" - -let same_rawconstr c d = - try same_raw c d; true - with Failure _ | Invalid_argument _ -> false - (**********************************************************************) (* mapping patterns to cases_pattern_expr *) @@ -555,11 +486,6 @@ let rec flatten_application = function | RApp (loc,RApp(_,a,l'),l) -> flatten_application (RApp (loc,a,l'@l)) | a -> a -let rec rename_rawconstr_var id0 id1 = function - RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1) - | RVar(loc,id) when id=id0 -> RVar(loc,id1) - | c -> map_rawconstr (rename_rawconstr_var id0 id1) c - (**********************************************************************) (* mapping rawterms to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) @@ -964,32 +890,6 @@ let rec raw_of_pat env = function | PCoFix c -> Detyping.detype false [] env (mkCoFix c) | PSort s -> RSort (loc,s) -and raw_of_eqn env constr construct_nargs branch = - let make_pat x env b ids = - let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in - let id = next_name_away_with_default "x" x avoid in - PatVar (dummy_loc,Name id),(Name id)::env,id::ids - in - let rec buildrec ids patlist env n b = - if n=0 then - (dummy_loc, ids, - [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], - raw_of_pat env b) - else - match b with - | PLambda (x,_,b) -> - let pat,new_env,new_ids = make_pat x env b ids in - buildrec new_ids (pat::patlist) new_env (n-1) b - - | PLetIn (x,_,b) -> - let pat,new_env,new_ids = make_pat x env b ids in - buildrec new_ids (pat::patlist) new_env (n-1) b - - | _ -> - error "Unsupported branch in case-analysis while printing pattern." - in - buildrec [] [] env construct_nargs branch - let extern_constr_pattern env pat = extern true (None,[]) Idset.empty (raw_of_pat env pat) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 3d618b0bc..bb555148f 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -106,11 +106,6 @@ let init_modules = [ init_dir@["Wf"] ] -let coq_id = id_of_string "Coq" -let init_id = id_of_string "Init" -let arith_id = id_of_string "Arith" -let datatypes_id = id_of_string "Datatypes" - let logic_module_name = ["Coq";"Init";"Logic"] let logic_module = make_dir logic_module_name @@ -225,8 +220,6 @@ let lazy_logic_constant dir id = lazy (logic_constant dir id) let coq_eq_eq = lazy_init_constant ["Logic"] "eq" let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl" let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind" -let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec" -let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect" let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal" let coq_eq_sym = lazy_init_constant ["Logic"] "eq_sym" let coq_eq_trans = lazy_init_constant ["Logic"] "eq_trans" @@ -248,8 +241,6 @@ let build_coq_eq_refl () = Lazy.force coq_eq_refl let build_coq_eq_sym () = Lazy.force coq_eq_sym let build_coq_f_equal2 () = Lazy.force coq_f_equal2 -let build_coq_sym_eq = build_coq_eq_sym (* compatibility *) - let build_coq_inversion_eq_data () = let _ = check_required_library logic_module_name in { inv_eq = Lazy.force coq_eq_eq; @@ -261,8 +252,6 @@ let build_coq_inversion_eq_data () = let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq" let coq_jmeq_refl = lazy_logic_constant ["JMeq"] "JMeq_refl" let coq_jmeq_ind = lazy_logic_constant ["JMeq"] "JMeq_ind" -let coq_jmeq_rec = lazy_logic_constant ["JMeq"] "JMeq_rec" -let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect" let coq_jmeq_sym = lazy_logic_constant ["JMeq"] "JMeq_sym" let coq_jmeq_congr = lazy_logic_constant ["JMeq"] "JMeq_congr" let coq_jmeq_trans = lazy_logic_constant ["JMeq"] "JMeq_trans" @@ -298,8 +287,6 @@ let build_coq_sumbool () = Lazy.force coq_sumbool let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity" let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity" let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind" -let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec" -let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect" let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr" let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym" let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans" diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 113b12f23..e7394d70c 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -154,11 +154,6 @@ let dump_constraint ((loc, n), _, _) sec ty = | Names.Name id -> dump_definition (loc, id) sec ty | Names.Anonymous -> () -let dump_name (loc, n) sec ty = - match n with - | Names.Name id -> dump_definition (loc, id) sec ty - | Names.Anonymous -> () - let dump_modref loc mp ty = if dump () then let (dp, l) = Lib.split_modpath mp in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 0776e63c6..1e97c5178 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -57,7 +57,7 @@ let cache_generalizable_type (_,(local,cmd)) = let load_generalizable_type _ (_,(local,cmd)) = generalizable_table := add_generalizable cmd !generalizable_table -let (in_generalizable, _) = +let in_generalizable = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; @@ -203,8 +203,6 @@ let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) let rec make_fresh ids env x = if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_subscript x) -let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id - let next_name_away_from na avoid = match na with | Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon") diff --git a/interp/notation.ml b/interp/notation.ml index 0395e9bc3..d5e27841a 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -111,13 +111,10 @@ let subst_scope (subst,sc) = sc open Libobject -let discharge_scope (local,_,_ as o) = - if local then None else Some o - let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let (inScope,outScope) = +let inScope = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -499,7 +496,7 @@ let rebuild_arguments_scope (req,r,l) = let l1,_ = list_chop (List.length l' - List.length l) l' in (req,r,l1@l) -let (inArgumentsScope,outArgumentsScope) = +let inArgumentsScope = declare_object {(default_object "ARGUMENTS-SCOPE") with cache_function = cache_arguments_scope; load_function = load_arguments_scope; @@ -622,9 +619,6 @@ let factorize_entries = function (ntn,[c],[]) l in (ntn,l_of_ntn)::rest -let is_ident s = (* Poor analysis *) - String.length s <> 0 & is_letter s.[0] - let browse_notation strict ntn map = let find = if String.contains ntn ' ' then (=) ntn diff --git a/interp/reserve.ml b/interp/reserve.ml index ec58e47fa..3bcd6b1e7 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -21,7 +21,7 @@ let reserve_table = ref Idmap.empty let cache_reserved_type (_,(id,t)) = reserve_table := Idmap.add id t !reserve_table -let (in_reserved, _) = +let in_reserved = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 954485f77..8056ab426 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -62,7 +62,7 @@ let subst_syntax_constant (subst,(local,pat,onlyparse)) = let classify_syntax_constant (local,_,_ as o) = if local then Dispose else Substitute o -let (in_syntax_constant, out_syntax_constant) = +let in_syntax_constant = declare_object {(default_object "SYNTAXCONSTANT") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; diff --git a/interp/topconstr.ml b/interp/topconstr.ml index dc35c47db..cbdb41ea3 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -508,8 +508,6 @@ let subst_interpretation subst (metas,pat) = let bound = List.map fst metas in (metas,subst_aconstr subst bound pat) -let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l) - (* Pattern-matching rawconstr and aconstr *) let abstract_return_type_context pi mklam tml rtno = @@ -528,11 +526,6 @@ let abstract_return_type_context_aconstr = abstract_return_type_context pi3 (fun na c -> ALambda(na,AHole Evd.InternalHole,c)) -let rec adjust_scopes = function - | _,[] -> [] - | [],a::args -> (None,a) :: adjust_scopes ([],args) - | sc::scopes,a::args -> (sc,a) :: adjust_scopes (scopes,args) - exception No_match let rec alpha_var id1 id2 = function @@ -586,10 +579,6 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 = (match_names metas acc na1 na2) patl1 patl2 | _ -> raise No_match -let adjust_application_n n loc f l = - let l1,l2 = list_chop (List.length l - n) l in - if l1 = [] then f,l else RApp (loc,f,l1), l2 - let glue_letin_with_decls = true let rec match_iterated_binders islambda decls = function @@ -947,10 +936,6 @@ let local_binders_loc bll = if bll = [] then dummy_loc else join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll)) -let occur_var_constr_ref id = function - | Ident (loc,id') -> id = id' - | Qualid _ -> false - let ids_of_cases_indtype = let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in let rec vars_of = function diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 913421087..00f5eb3b0 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -50,12 +50,6 @@ value coq_static_alloc(value size) /* ML */ return (value) coq_stat_alloc((asize_t) Long_val(size)); } -value coq_static_free(value blk) /* ML */ -{ - coq_stat_free((void *) blk); - return Val_unit; -} - value accumulate_code(value unit) /* ML */ { return (value) accumulate; diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index c0093a49e..79e4d0fea 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -49,7 +49,6 @@ extern code_t accumulate; /* functions over global environment */ value coq_static_alloc(value size); /* ML */ -value coq_static_free(value string); /* ML */ value init_coq_vm(value unit); /* ML */ value re_init_coq_vm(value unit); /* ML */ diff --git a/kernel/closure.ml b/kernel/closure.ml index d70ce83a8..6434e1415 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -81,7 +81,6 @@ module type RedFlagsSig = sig val red_add_transparent : reds -> transparent_state -> reds val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool - val red_get_const : reds -> bool * evaluable_global_reference list end module RedFlags = (struct @@ -156,16 +155,6 @@ module RedFlags = (struct | DELTA -> (* Used for Rel/Var defined in context *) incr_cnt red.r_delta delta - let red_get_const red = - let p1,p2 = red.r_const in - let (b1,l1) = Idpred.elements p1 in - let (b2,l2) = Cpred.elements p2 in - if b1=b2 then - let l1' = List.map (fun x -> EvalVarRef x) l1 in - let l2' = List.map (fun x -> EvalConstRef x) l2 in - (b1, l1' @ l2') - else error "unrepresentable pair of predicate" - end : RedFlagsSig) open RedFlags @@ -690,16 +679,6 @@ let fapp_stack (m,stk) = zip m stk (strip_update_shift, through get_arg). *) (* optimised for the case where there are no shifts... *) -let strip_update_shift head stk = - assert (head.norm <> Red); - let rec strip_rec h depth = function - | Zshift(k)::s -> strip_rec (lift_fconstr k h) (depth+k) s - | Zupdate(m)::s -> - strip_rec (update m (h.norm,h.term)) depth s - | stk -> (depth,stk) in - strip_rec head 0 stk - -(* optimised for the case where there are no shifts... *) let strip_update_shift_app head stk = assert (head.norm <> Red); let rec strip_rec rstk h depth = function diff --git a/kernel/closure.mli b/kernel/closure.mli index 4e8b6d2bd..74c91650a 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -60,8 +60,6 @@ module type RedFlagsSig = sig (** Tests if a reduction kind is set *) val red_set : reds -> red_kind -> bool - (** Gives the constant list *) - val red_get_const : reds -> bool * evaluable_global_reference list end module RedFlags : RedFlagsSig diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 77a322905..983c1f26d 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -23,7 +23,6 @@ open Cbytegen external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" -external free_tcode : tcode -> unit = "coq_static_free" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" (*******************) diff --git a/kernel/entries.ml b/kernel/entries.ml index c31c6f75d..714da0319 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -69,14 +69,7 @@ type constant_entry = (*s Modules *) - -type specification_entry = - SPEconst of constant_entry - | SPEmind of mutual_inductive_entry - | SPEmodule of module_entry - | SPEmodtype of module_struct_entry - -and module_struct_entry = +type module_struct_entry = MSEident of module_path | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry | MSEwith of module_struct_entry * with_declaration diff --git a/kernel/entries.mli b/kernel/entries.mli index 224680dff..2ba306455 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -64,14 +64,7 @@ type constant_entry = (** {6 Modules } *) - -type specification_entry = - SPEconst of constant_entry - | SPEmind of mutual_inductive_entry - | SPEmodule of module_entry - | SPEmodtype of module_struct_entry - -and module_struct_entry = +type module_struct_entry = MSEident of module_path | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry | MSEwith of module_struct_entry * with_declaration diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 63a7b83ee..e4bf055c9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -85,15 +85,6 @@ let mind_check_names mie = vue since inductive and constructors are not referred to by their name, but only by the name of the inductive packet and an index. *) -let mind_check_arities env mie = - let check_arity id c = - if not (is_arity env c) then - raise (InductiveError (NotAnArity id)) - in - List.iter - (fun {mind_entry_typename=id; mind_entry_arity=ar} -> check_arity id ar) - mie.mind_entry_inds - (************************************************************************) (************************************************************************) @@ -549,16 +540,6 @@ let check_positivity kn env_ar params inds = (************************************************************************) (* Build the inductive packet *) -(* Elimination sorts *) -let is_recursive = Rtree.is_infinite -(* let rec one_is_rec rvec = - List.exists (function Mrec(i) -> List.mem i listind - | Imbr(_,lvec) -> array_exists one_is_rec lvec - | Norec -> false) rvec - in - array_exists one_is_rec -*) - (* Allowed eliminations *) let all_sorts = [InProp;InSet;InType] diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1e2cedee2..289968eb5 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -78,8 +78,6 @@ let instantiate_params full t args sign = if rem_args <> [] then fail(); substl subs ty -let instantiate_partial_params = instantiate_params false - let full_inductive_instantiate mib params sign = let dummy = prop_sort in let t = mkArity (sign,dummy) in @@ -95,10 +93,6 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) = (* Functions to build standard types related to inductive *) - -let number_of_inductives mib = Array.length mib.mind_packets -let number_of_constructors mip = Array.length mip.mind_consnames - (* Computing the actual sort of an applied or partially applied inductive type: diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 8b11aa185..452c2e69a 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -54,11 +54,6 @@ type substitution = (module_path * delta_resolver) Umap.t let empty_subst = Umap.empty - -let string_of_subst_domain = function - | MBI mbid -> debug_string_of_mbid mbid - | MPI mp -> string_of_mp mp - let add_mbid mbid mp resolve = Umap.add (MBI mbid) (mp,resolve) let add_mp mp1 mp2 resolve = @@ -109,16 +104,6 @@ let delta_of_mp resolve mp = | _ -> anomaly "mod_subst: bad association in delta_resolver" with Not_found -> mp - -let delta_of_kn resolve kn = - try - match Deltamap.find (KN kn) resolve with - | Equiv kn1 -> kn1 - | Inline _ -> kn - | _ -> anomaly - "mod_subst: bad association in delta_resolver" - with - Not_found -> kn let remove_mp_delta_resolver resolver mp = Deltamap.remove (MP mp) resolver diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index e8c831f70..e14e7c900 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -34,13 +34,6 @@ let rec list_split_assoc k rev_before = function | (k',b)::after when k=k' -> rev_before,b,after | h::tail -> list_split_assoc k (h::rev_before) tail -let rec list_fold_map2 f e = function - | [] -> (e,[],[]) - | h::t -> - let e',h1',h2' = f e h in - let e'',t1',t2' = list_fold_map2 f e' t in - e'',h1'::t1',h2'::t2' - let discr_resolver env mtb = match mtb.typ_expr with SEBstruct _ -> diff --git a/kernel/term.ml b/kernel/term.ml index 492ebbb0d..88bc4cc4e 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -285,14 +285,6 @@ let kind_of_term2 c = c let kind_of_term = kind_of_term - -(* En vue d'un kind_of_type : constr -> hnftype ??? *) -type hnftype = - | HnfSort of sorts - | HnfProd of name * constr * constr - | HnfAtom of constr - | HnfInd of inductive * constr array - (**********************************************************************) (* Non primitive term destructors *) (**********************************************************************) @@ -346,18 +338,12 @@ let rec is_Type c = match kind_of_term c with | Cast (c,_,_) -> is_Type c | _ -> false -let isType = function - | Type _ -> true - | _ -> false - let is_small = function | Prop _ -> true | _ -> false let iskind c = isprop c or is_Type c -let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2) - (* Tests if an evar *) let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false @@ -424,10 +410,6 @@ let destEvar c = match kind_of_term c with | Evar (kn, a as r) -> r | _ -> invalid_arg "destEvar" -let num_of_evar c = match kind_of_term c with - | Evar (n, _) -> n - | _ -> anomaly "num_of_evar called with bad args" - (* Destructs a (co)inductive type named kn *) let destInd c = match kind_of_term c with | Ind (kn, a as r) -> r @@ -497,18 +479,6 @@ let decompose_app c = | App (f,cl) -> (f, Array.to_list cl) | _ -> (c,[]) -(* strips head casts and flattens head applications *) -let rec strip_head_cast c = match kind_of_term c with - | App (f,cl) -> - let rec collapse_rec f cl2 = match kind_of_term f with - | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | Cast (c,_,_) -> collapse_rec c cl2 - | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) - in - collapse_rec f cl - | Cast (c,_,_) -> strip_head_cast c - | _ -> c - (****************************************************************************) (* Functions to recur through subterms *) (****************************************************************************) @@ -899,12 +869,10 @@ let mkCast = mkCast (* Constructs the product (x:t1)t2 *) let mkProd = mkProd let mkNamedProd id typ c = mkProd (Name id, typ, subst_var id c) -let mkProd_string s t c = mkProd (Name (id_of_string s), t, c) (* Constructs the abstraction [x:t1]t2 *) let mkLambda = mkLambda let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c) -let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c) (* Constructs [x=c_1:t]c_2 *) let mkLetIn = mkLetIn @@ -933,11 +901,6 @@ let mkNamedLambda_or_LetIn (id,body,t) c = | Some b -> mkNamedLetIn id b t c (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *) -let mkProd_wo_LetIn (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> subst1 b c - let mkNamedProd_wo_LetIn (id,body,t) c = match body with | None -> mkNamedProd id t c @@ -951,11 +914,6 @@ let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) function is not itself an applicative term *) let mkApp = mkApp -let mkAppA v = - let l = Array.length v in - if l=0 then anomaly "mkAppA received an empty array" - else mkApp (v.(0), Array.sub v 1 (Array.length v -1)) - (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) let mkConst = mkConst @@ -974,7 +932,6 @@ let mkConstruct = mkConstruct (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) let mkCase = mkCase -let mkCaseL (ci, p, c, ac) = mkCase (ci, p, c, Array.of_list ac) (* If recindxs = [|i1,...in|] funnames = [|f1,...fn|] diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 183a27935..3d2461237 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -18,7 +18,6 @@ open Reduction open Inductive open Type_errors -let conv = default_conv CONV let conv_leq = default_conv CUMUL let conv_leq_vecti env v1 v2 = @@ -45,8 +44,6 @@ let assumption_of_judgment env j = with TypeError _ -> error_assumption env j -let sort_judgment env j = (type_judgment env j).utj_type - (************************************************) (* Incremental typing rules: builds a typing judgement given the *) (* judgements for the subterms. *) @@ -474,8 +471,6 @@ and execute_recdef env (names,lar,vdef) i cu = and execute_array env = array_fold_map' (execute env) -and execute_list env = list_fold_map' (execute env) - (* Derived functions *) let infer env constr = let (j,(cst,_)) = diff --git a/kernel/univ.ml b/kernel/univ.ml index 9854cdc1d..40bd2a20d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -568,16 +568,6 @@ let no_upper_constraints u cst = (* Pretty-printing *) -let num_universes g = - UniverseLMap.fold (fun _ _ -> succ) g 0 - -let num_edges g = - let reln_len = function - | Equiv _ -> 1 - | Canonical {lt=lt;le=le} -> List.length lt + List.length le - in - UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0 - let pr_arc = function | Canonical {univ=u; lt=[]; le=[]} -> mt () diff --git a/kernel/vm.ml b/kernel/vm.ml index 90fb56d86..51528dbf2 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -538,12 +538,6 @@ let branch_of_switch k sw = (* Evaluation *) - -let is_accu v = - let o = Obj.repr v in - Obj.is_block o && Obj.tag o = accu_tag && - fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag - let rec whd_stack v stk = match stk with | [] -> whd_val v diff --git a/lib/gset.ml b/lib/gset.ml deleted file mode 100644 index 984259500..000000000 --- a/lib/gset.ml +++ /dev/null @@ -1,240 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Sets using the generic comparison function of ocaml. Code borrowed from - the ocaml standard library. *) - - type 'a t = Empty | Node of 'a t * 'a * 'a t * int - - (* Sets are represented by balanced binary trees (the heights of the - children differ by at most 2 *) - - let height = function - Empty -> 0 - | Node(_, _, _, h) -> h - - (* Creates a new node with left son l, value x and right son r. - l and r must be balanced and | height l - height r | <= 2. - Inline expansion of height for better speed. *) - - let create l x r = - let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in - let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in - Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1)) - - (* Same as create, but performs one step of rebalancing if necessary. - Assumes l and r balanced. - Inline expansion of create for better speed in the most frequent case - where no rebalancing is required. *) - - let bal l x r = - let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in - let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in - if hl > hr + 2 then begin - match l with - Empty -> invalid_arg "Set.bal" - | Node(ll, lv, lr, _) -> - if height ll >= height lr then - create ll lv (create lr x r) - else begin - match lr with - Empty -> invalid_arg "Set.bal" - | Node(lrl, lrv, lrr, _)-> - create (create ll lv lrl) lrv (create lrr x r) - end - end else if hr > hl + 2 then begin - match r with - Empty -> invalid_arg "Set.bal" - | Node(rl, rv, rr, _) -> - if height rr >= height rl then - create (create l x rl) rv rr - else begin - match rl with - Empty -> invalid_arg "Set.bal" - | Node(rll, rlv, rlr, _) -> - create (create l x rll) rlv (create rlr rv rr) - end - end else - Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1)) - - (* Same as bal, but repeat rebalancing until the final result - is balanced. *) - - let rec join l x r = - match bal l x r with - Empty -> invalid_arg "Set.join" - | Node(l', x', r', _) as t' -> - let d = height l' - height r' in - if d < -2 or d > 2 then join l' x' r' else t' - - (* Merge two trees l and r into one. - All elements of l must precede the elements of r. - Assumes | height l - height r | <= 2. *) - - let rec merge t1 t2 = - match (t1, t2) with - (Empty, t) -> t - | (t, Empty) -> t - | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> - bal l1 v1 (bal (merge r1 l2) v2 r2) - - (* Same as merge, but does not assume anything about l and r. *) - - let rec concat t1 t2 = - match (t1, t2) with - (Empty, t) -> t - | (t, Empty) -> t - | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> - join l1 v1 (join (concat r1 l2) v2 r2) - - (* Splitting *) - - let rec split x = function - Empty -> - (Empty, None, Empty) - | Node(l, v, r, _) -> - let c = Pervasives.compare x v in - if c = 0 then (l, Some v, r) - else if c < 0 then - let (ll, vl, rl) = split x l in (ll, vl, join rl v r) - else - let (lr, vr, rr) = split x r in (join l v lr, vr, rr) - - (* Implementation of the set operations *) - - let empty = Empty - - let is_empty = function Empty -> true | _ -> false - - let rec mem x = function - Empty -> false - | Node(l, v, r, _) -> - let c = Pervasives.compare x v in - c = 0 || mem x (if c < 0 then l else r) - - let rec add x = function - Empty -> Node(Empty, x, Empty, 1) - | Node(l, v, r, _) as t -> - let c = Pervasives.compare x v in - if c = 0 then t else - if c < 0 then bal (add x l) v r else bal l v (add x r) - - let singleton x = Node(Empty, x, Empty, 1) - - let rec remove x = function - Empty -> Empty - | Node(l, v, r, _) -> - let c = Pervasives.compare x v in - if c = 0 then merge l r else - if c < 0 then bal (remove x l) v r else bal l v (remove x r) - - let rec union s1 s2 = - match (s1, s2) with - (Empty, t2) -> t2 - | (t1, Empty) -> t1 - | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> - if h1 >= h2 then - if h2 = 1 then add v2 s1 else begin - let (l2, _, r2) = split v1 s2 in - join (union l1 l2) v1 (union r1 r2) - end - else - if h1 = 1 then add v1 s2 else begin - let (l1, _, r1) = split v2 s1 in - join (union l1 l2) v2 (union r1 r2) - end - - let rec inter s1 s2 = - match (s1, s2) with - (Empty, t2) -> Empty - | (t1, Empty) -> Empty - | (Node(l1, v1, r1, _), t2) -> - match split v1 t2 with - (l2, None, r2) -> - concat (inter l1 l2) (inter r1 r2) - | (l2, Some _, r2) -> - join (inter l1 l2) v1 (inter r1 r2) - - let rec diff s1 s2 = - match (s1, s2) with - (Empty, t2) -> Empty - | (t1, Empty) -> t1 - | (Node(l1, v1, r1, _), t2) -> - match split v1 t2 with - (l2, None, r2) -> - join (diff l1 l2) v1 (diff r1 r2) - | (l2, Some _, r2) -> - concat (diff l1 l2) (diff r1 r2) - - let rec compare_aux l1 l2 = - match (l1, l2) with - ([], []) -> 0 - | ([], _) -> -1 - | (_, []) -> 1 - | (Empty :: t1, Empty :: t2) -> - compare_aux t1 t2 - | (Node(Empty, v1, r1, _) :: t1, Node(Empty, v2, r2, _) :: t2) -> - let c = compare v1 v2 in - if c <> 0 then c else compare_aux (r1::t1) (r2::t2) - | (Node(l1, v1, r1, _) :: t1, t2) -> - compare_aux (l1 :: Node(Empty, v1, r1, 0) :: t1) t2 - | (t1, Node(l2, v2, r2, _) :: t2) -> - compare_aux t1 (l2 :: Node(Empty, v2, r2, 0) :: t2) - - let compare s1 s2 = - compare_aux [s1] [s2] - - let equal s1 s2 = - compare s1 s2 = 0 - - let rec subset s1 s2 = - match (s1, s2) with - Empty, _ -> - true - | _, Empty -> - false - | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) -> - let c = Pervasives.compare v1 v2 in - if c = 0 then - subset l1 l2 && subset r1 r2 - else if c < 0 then - subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2 - else - subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2 - - let rec iter f = function - Empty -> () - | Node(l, v, r, _) -> iter f l; f v; iter f r - - let rec fold f s accu = - match s with - Empty -> accu - | Node(l, v, r, _) -> fold f l (f v (fold f r accu)) - - let rec cardinal = function - Empty -> 0 - | Node(l, v, r, _) -> cardinal l + 1 + cardinal r - - let rec elements_aux accu = function - Empty -> accu - | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l - - let elements s = - elements_aux [] s - - let rec min_elt = function - Empty -> raise Not_found - | Node(Empty, v, r, _) -> v - | Node(l, v, r, _) -> min_elt l - - let rec max_elt = function - Empty -> raise Not_found - | Node(l, v, Empty, _) -> v - | Node(l, v, r, _) -> max_elt r - - let choose = min_elt diff --git a/lib/gset.mli b/lib/gset.mli deleted file mode 100644 index ae5e13e9e..000000000 --- a/lib/gset.mli +++ /dev/null @@ -1,32 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Sets using the generic comparison function of ocaml. Same interface as - the module [Set] from the ocaml standard library. *) - -type 'a t - -val empty : 'a t -val is_empty : 'a t -> bool -val mem : 'a -> 'a t -> bool -val add : 'a -> 'a t -> 'a t -val singleton : 'a -> 'a t -val remove : 'a -> 'a t -> 'a t -val union : 'a t -> 'a t -> 'a t -val inter : 'a t -> 'a t -> 'a t -val diff : 'a t -> 'a t -> 'a t -val compare : 'a t -> 'a t -> int -val equal : 'a t -> 'a t -> bool -val subset : 'a t -> 'a t -> bool -val iter : ('a -> unit) -> 'a t -> unit -val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b -val cardinal : 'a t -> int -val elements : 'a t -> 'a list -val min_elt : 'a t -> 'a -val max_elt : 'a t -> 'a -val choose : 'a t -> 'a diff --git a/lib/lib.mllib b/lib/lib.mllib index c3982a8c9..0607ae50e 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -10,11 +10,9 @@ Hashcons Dyn System Envars -Gset Gmap Fset Fmap -Tlm Tries Gmapl Profile diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 37d63b360..854e4b49c 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -273,11 +273,6 @@ let pp_dirs ft = (* pretty print on stdout and stderr *) -let pp_std_dirs = pp_dirs !std_ft -let pp_err_dirs = pp_dirs !err_ft - -let ppcmds x = Ppdir_ppcmds x - (* Special chars for emacs, to detect warnings inside goal output *) let emacs_warning_start_string = String.make 1 (Char.chr 254) let emacs_warning_end_string = String.make 1 (Char.chr 255) diff --git a/lib/profile.ml b/lib/profile.ml index fe86fac59..53ba0c19b 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -9,7 +9,6 @@ open Gc let word_length = Sys.word_size / 8 -let int_size = Sys.word_size - 1 let float_of_time t = float_of_int t /. 100. let time_of_float f = int_of_float (f *. 100.) @@ -352,7 +351,6 @@ let close_profile print = end | _ -> failwith "Inconsistency" -let append_profile () = close_profile false let print_profile () = close_profile true let declare_profile name = diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml index 2a7f9df0e..9ce348a0b 100644 --- a/lib/segmenttree.ml +++ b/lib/segmenttree.ml @@ -40,7 +40,6 @@ type domain = type 'a t = (domain * 'a option) array (** The root is the first item of the array. *) -let is_root i = (i = 0) (** Standard layout for left child. *) let left_child i = 2 * i + 1 diff --git a/lib/tlm.ml b/lib/tlm.ml deleted file mode 100644 index 4c2287dd2..000000000 --- a/lib/tlm.ml +++ /dev/null @@ -1,61 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t - -let empty = Node (Gset.empty, Gmap.empty) - -let map (Node (_,m)) lbl = Gmap.find lbl m - -let xtract (Node (hereset,_)) = Gset.elements hereset - -let dom (Node (_,m)) = Gmap.dom m - -let in_dom (Node (_,m)) lbl = Gmap.mem lbl m - -let is_empty_node (Node(a,b)) = (Gset.elements a = []) & (Gmap.to_list b = []) - -let assure_arc m lbl = - if Gmap.mem lbl m then - m - else - Gmap.add lbl (Node (Gset.empty,Gmap.empty)) m - -let cleanse_arcs (Node (hereset,m)) = - let l = Gmap.rng m in - Node(hereset, if List.for_all is_empty_node l then Gmap.empty else m) - -let rec at_path f (Node (hereset,m)) = function - | [] -> - cleanse_arcs (Node(f hereset,m)) - | h::t -> - let m = assure_arc m h in - cleanse_arcs (Node(hereset, - Gmap.add h (at_path f (Gmap.find h m) t) m)) - -let add tm (path,v) = - at_path (fun hereset -> Gset.add v hereset) tm path - -let rmv tm (path,v) = - at_path (fun hereset -> Gset.remove v hereset) tm path - -let app f tlm = - let rec apprec pfx (Node(hereset,m)) = - let path = List.rev pfx in - Gset.iter (fun v -> f(path,v)) hereset; - Gmap.iter (fun l tm -> apprec (l::pfx) tm) m - in - apprec [] tlm - -let to_list tlm = - let rec torec pfx (Node(hereset,m)) = - let path = List.rev pfx in - List.flatten((List.map (fun v -> (path,v)) (Gset.elements hereset)):: - (List.map (fun (l,tm) -> torec (l::pfx) tm) (Gmap.to_list m))) - in - torec [] tlm diff --git a/lib/tlm.mli b/lib/tlm.mli deleted file mode 100644 index 73668ff44..000000000 --- a/lib/tlm.mli +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Tries. This module implements a data structure [('a,'b) t] mapping lists - of values of type ['a] to sets (as lists) of values of type ['b]. *) - -type ('a,'b) t - -val empty : ('a,'b) t - -(** Work on labels, not on paths. *) - -val map : ('a,'b) t -> 'a -> ('a,'b) t -val xtract : ('a,'b) t -> 'b list -val dom : ('a,'b) t -> 'a list -val in_dom : ('a,'b) t -> 'a -> bool - -(** Work on paths, not on labels. *) - -val add : ('a,'b) t -> 'a list * 'b -> ('a,'b) t -val rmv : ('a,'b) t -> ('a list * 'b) -> ('a,'b) t - -val app : (('a list * 'b) -> unit) -> ('a,'b) t -> unit -val to_list : ('a,'b) t -> ('a list * 'b) list - diff --git a/library/declare.ml b/library/declare.ml index 0764af4b0..a9c463020 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -78,7 +78,7 @@ let discharge_variable (_,o) = match o with | Inr (id,_) -> Some (Inl (variable_constraints id)) | Inl _ -> Some o -let (inVariable,_) = +let inVariable = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; discharge_function = discharge_variable; @@ -145,7 +145,7 @@ let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk let classify_constant cst = Substitute (dummy_constant cst) -let (inConstant,_) = +let inConstant = declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; @@ -259,7 +259,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = true; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) -let (inInductive,_) = +let inInductive = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; diff --git a/library/declaremods.ml b/library/declaremods.ml index 30fa3db65..58b0d6a46 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -262,7 +262,7 @@ let classify_module (_,substobjs) = Substitute (None,substobjs) let (in_module,out_module) = - declare_object {(default_object "MODULE") with + declare_object_full {(default_object "MODULE") with cache_function = cache_module; load_function = load_module; open_function = open_module; @@ -289,7 +289,7 @@ let open_keep i ((sp,kn),seg) = let dirpath,mp = dir_of_sp sp, mp_of_kn kn in open_objects i (dirpath,(mp,empty_dirpath)) seg -let (in_modkeep,_) = +let in_modkeep = declare_object {(default_object "MODULE KEEP OBJECTS") with cache_function = cache_keep; load_function = load_keep; @@ -376,7 +376,7 @@ let classify_modtype (_,substobjs,_) = Substitute (None,substobjs,[]) -let (in_modtype,_) = +let in_modtype = declare_object {(default_object "MODULE TYPE") with cache_function = cache_modtype; open_function = open_modtype; @@ -649,7 +649,7 @@ let subst_import (subst,(export,mp as obj)) = if mp'==mp then obj else (export,mp') -let (in_import,_) = +let in_import = declare_object {(default_object "IMPORT MODULE") with cache_function = cache_import; open_function = (fun i o -> if i=1 then cache_import o); @@ -840,7 +840,7 @@ let classify_include ((me,is_mod),substobjs) = Substitute ((me,is_mod),substobjs) let (in_include,out_include) = - declare_object {(default_object "INCLUDE") with + declare_object_full {(default_object "INCLUDE") with cache_function = cache_include; load_function = load_include; open_function = open_include; diff --git a/library/goptions.ml b/library/goptions.ml index 85d9fd77b..e047ab9a0 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -94,7 +94,7 @@ module MakeTable = if p' == p then obj else (f,p') in - let (inGo,outGo) = + let inGo = Libobject.declare_object {(Libobject.default_object nick) with Libobject.load_function = load_options; Libobject.open_function = load_options; @@ -235,18 +235,18 @@ let declare_option cast uncast 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. *) + 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. *) + 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. *) + 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); diff --git a/library/heads.ml b/library/heads.ml index 313050bbc..363443bbb 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -165,7 +165,7 @@ let discharge_head (_,(ref,k)) = let rebuild_head (ref,k) = (ref, compute_head ref) -let (inHead, _) = +let inHead = declare_object {(default_object "HEAD") with cache_function = cache_head; load_function = load_head; diff --git a/library/impargs.ml b/library/impargs.ml index daf264f6a..84097c840 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -300,8 +300,6 @@ let compute_manual_implicits env flags t enriching l = in merge 1 l autoimps -let const v _ = v - let compute_implicits_auto env f manual t = match manual with | [] -> @@ -523,7 +521,7 @@ let rebuild_implicits (req,l) = let classify_implicits (req,_ as obj) = if req = ImplLocal then Dispose else Substitute obj -let (inImplicits, _) = +let inImplicits = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; load_function = load_implicits; diff --git a/library/lib.ml b/library/lib.ml index 8c9153cd7..f0eea4355 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -252,12 +252,6 @@ let add_frozen_state () = (* Modules. *) - -let is_opened id = function - oname,(OpenedSection _ | OpenedModule _ | OpenedModtype _) when - basename (fst oname) = id -> true - | _ -> false - let is_opening_node = function _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true | _ -> false @@ -356,13 +350,6 @@ let contents_after = function (* Modules. *) -let check_for_comp_unit () = - let is_decl = function (_,FrozenState _) -> false | _ -> true in - try - let _ = find_entry_p is_decl in - error "a module cannot be started after some declarations" - with Not_found -> () - (* TODO: use check_for_module ? *) let start_compilation s mp = if !comp_name <> None then @@ -499,8 +486,6 @@ let add_section_constant kn = let replacement_context () = pi2 (List.hd !sectab) -let variables_context () = pi1 (List.hd !sectab) - let section_segment_of_constant con = Names.Cmap.find con (fst (pi3 (List.hd !sectab))) @@ -595,7 +580,7 @@ let close_section () = (* Backtracking. *) let (inLabel,outLabel) = - declare_object {(default_object "DOT") with + declare_object_full {(default_object "DOT") with classify_function = (fun _ -> Dispose)} let recache_decl = function diff --git a/library/libnames.ml b/library/libnames.ml index bb45369f2..e47ce86ca 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -195,8 +195,6 @@ module SpOrdered = let compare = sp_ord end -module Spset = Set.Make(SpOrdered) -module Sppred = Predicate.Make(SpOrdered) module Spmap = Map.Make(SpOrdered) let dirpath sp = let (p,_) = repr_path sp in p diff --git a/library/libnames.mli b/library/libnames.mli index f881f4b38..1f49b6a4f 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -107,7 +107,6 @@ val path_of_string : string -> full_path val string_of_path : full_path -> string val pr_path : full_path -> std_ppcmds -module Sppred : Predicate.S with type elt = full_path module Spmap : Map.S with type key = full_path val restrict_path : int -> full_path -> full_path diff --git a/library/libobject.ml b/library/libobject.ml index b44418b13..d9ffe1cd5 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -79,7 +79,7 @@ let object_tag lobj = Dyn.tag lobj let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) -let declare_object odecl = +let declare_object_full odecl = let na = odecl.object_name in let (infun,outfun) = Dyn.create na in let cacher (oname,lobj) = @@ -122,6 +122,8 @@ let declare_object odecl = dyn_rebuild_function = rebuild }; (infun,outfun) +let declare_object odecl = fst (declare_object_full odecl) + let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) (* this function describes how the cache, load, open, and export functions diff --git a/library/libobject.mli b/library/libobject.mli index 32cf9354f..ad4468fb8 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -85,15 +85,18 @@ val default_object : string -> 'a object_declaration val ident_subst_function : substitution * 'a -> 'a (** {6 ... } *) -(** Given an object declaration, the function [declare_object] +(** Given an object declaration, the function [declare_object_full] will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects. *) type obj -val declare_object : +val declare_object_full : 'a object_declaration -> ('a -> obj) * (obj -> 'a) +val declare_object : + 'a object_declaration -> ('a -> obj) + val object_tag : obj -> string val cache_object : object_name * obj -> unit diff --git a/library/library.ml b/library/library.ml index c1673925c..45d5c8f58 100644 --- a/library/library.ml +++ b/library/library.ml @@ -66,8 +66,6 @@ let add_load_path isroot (phys_path,coq_path) = load_paths := (phys_path,coq_path,isroot) :: !load_paths; | _ -> anomaly ("Two logical paths are associated to "^phys_path) -let physical_paths (dp,lp) = dp - let extend_path_with_dirpath p dir = List.fold_left Filename.concat p (List.map string_of_id (List.rev (repr_dirpath dir))) @@ -213,9 +211,6 @@ let library_is_loaded dir = let library_is_opened dir = List.exists (fun m -> m.library_name = dir) !libraries_imports_list -let library_is_exported dir = - List.exists (fun m -> m.library_name = dir) !libraries_exports_list - let loaded_libraries () = List.map (fun m -> m.library_name) !libraries_loaded_list @@ -305,7 +300,7 @@ let subst_import (_,o) = o let classify_import (_,export as obj) = if export then Substitute obj else Dispose -let (in_import, out_import) = +let in_import = declare_object {(default_object "IMPORT LIBRARY") with cache_function = cache_import; open_function = open_import; @@ -517,7 +512,7 @@ let discharge_require (_,o) = Some o (* open_function is never called from here because an Anticipate object *) -let (in_require, out_require) = +let in_require = declare_object {(default_object "REQUIRE") with cache_function = cache_require; load_function = load_require; diff --git a/library/nameops.ml b/library/nameops.ml index e8c5b3d05..799b8ebe1 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -110,8 +110,6 @@ let add_prefix s id = id_of_string (s ^ string_of_id id) let atompart_of_id id = fst (repr_ident id) -let lift_ident = lift_subscript - (* Names *) let out_name = function diff --git a/library/nametab.ml b/library/nametab.ml index 7ee4b3920..e43ae650c 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -378,7 +378,6 @@ let locate_modtype qid = SpTab.locate qid !the_modtypetab let full_name_modtype qid = SpTab.user_name qid !the_modtypetab let locate_tactic qid = SpTab.locate qid !the_tactictab -let full_name_tactic qid = SpTab.user_name qid !the_tactictab let locate_dir qid = DirTab.locate qid !the_dirtab @@ -411,11 +410,6 @@ let locate_constant qid = | TrueGlobal (ConstRef kn) -> kn | _ -> raise Not_found -let locate_mind qid = - match locate_extended qid with - | TrueGlobal (IndRef (kn,0)) -> kn - | _ -> raise Not_found - let global_of_path sp = match SpTab.find sp !the_ccitab with | TrueGlobal ref -> ref @@ -423,9 +417,6 @@ let global_of_path sp = let extended_global_of_path sp = SpTab.find sp !the_ccitab -let locate_in_absolute_module dir id = - global_of_path (make_path dir id) - let global r = let (loc,qid) = qualid_of_reference r in try match locate_extended qid with @@ -449,8 +440,6 @@ let exists_module = exists_dir let exists_modtype sp = SpTab.exists sp !the_modtypetab -let exists_tactic sp = SpTab.exists sp !the_tactictab - (* Reverse locate functions ***********************************************) let path_of_global ref = diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 8931d67f3..12cffc492 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -107,18 +107,6 @@ let ident_colon = | _ -> err ()) | _ -> err ()) -let ident_with = - Gram.Entry.of_parser "ident_with" - (fun strm -> - match get_tok (stream_nth 0 strm) with - | IDENT s -> - (match get_tok (stream_nth 1 strm) with - | KEYWORD "with" -> - stream_njunk 2 strm; - Names.id_of_string s - | _ -> err ()) - | _ -> err ()) - let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None GEXTEND Gram diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index f9e146730..9b476d996 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -93,24 +93,6 @@ let check_for_coloneq = | KEYWORD "(" -> skip_binders 2 | _ -> err ()) -let guess_lpar_ipat s strm = - match get_tok (stream_nth 0 strm) with - | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with - | KEYWORD ("("|"[") -> () - | IDENT _ -> - (match get_tok (stream_nth 2 strm) with - | KEYWORD s' when s = s' -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err () - -let guess_lpar_coloneq = - Gram.Entry.of_parser "guess_lpar_coloneq" (guess_lpar_ipat ":=") - -let guess_lpar_colon = - Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":") - let lookup_at_as_coma = Gram.Entry.of_parser "lookup_at_as_coma" (fun strm -> diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index d1168ad19..15cdc6077 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -250,8 +250,6 @@ let rec number len = parser | [< ' ('0'..'9' as c); s >] -> number (store len c) s | [< >] -> len -let escape len c = store len c - let rec string in_comments bp len = parser | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> if esc then string in_comments bp (store len '"') s else len diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 95948d2ac..034c46e58 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -264,13 +264,6 @@ let get_univ s = let get_entry (u, utab) s = Hashtbl.find utab s -let get_entry_type (u, utab) s = - try - type_of_typed_entry (get_entry (u, utab) s) - with Not_found -> - errorlabstrm "Pcoq.get_entry" - (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".") - let new_entry etyp (u, utab) s = if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr); let ename = u ^ ":" ^ s in @@ -340,7 +333,6 @@ module Prim = module Constr = struct let gec_constr = make_gen_entry uconstr rawwit_constr - let gec_constr_list = make_gen_entry uconstr (wit_list0 rawwit_constr) (* Entries that can be refered via the string -> Gram.entry table *) let constr = gec_constr "constr" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index c7edd9b92..7db89a5ff 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -147,11 +147,6 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe -(* -val get_entry : gram_universe -> string -> typed_entry -val get_entry_type : gram_universe -> string -> entry_type -*) - val create_entry : gram_universe -> string -> entry_type -> typed_entry val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> 'a Gram.entry diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 6276a23c3..9bfa32285 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -22,14 +22,10 @@ open Constrextern open Termops (*i*) -let sep_p = fun _ -> str"." let sep_v = fun _ -> str"," ++ spc() -let sep_pp = fun _ -> str":" -let sep_bar = fun _ -> spc() ++ str"| " let pr_tight_coma () = str "," ++ cut () let latom = 0 -let lannot = 100 let lprod = 200 let llambda = 200 let lif = 200 @@ -108,10 +104,6 @@ let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) -let pr_optc pr = function - | None -> mt () - | Some x -> pr_sep_com spc pr x - let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" let pr_universe = Univ.pr_uni @@ -355,21 +347,6 @@ let pr_recursive pr_decl id = function (pr_decl true) dl ++ fnl() ++ str "for " ++ pr_id id -let is_var id = function - | CRef (Ident (_,id')) when id=id' -> true - | _ -> false - -let tm_clash = function - | (CRef (Ident (_,id)), Some (CApp (_,_,nal))) - when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false) - nal - -> Some id - | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal))) - when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false) - nal - -> Some id - | _ -> None - let pr_asin pr (na,indnalopt) = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) | Some na -> spc () ++ str "as " ++ pr_lname na @@ -387,8 +364,6 @@ let pr_case_type pr po = | Some p -> spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p) -let pr_return_type pr po = pr_case_type pr po - let pr_simple_return_type pr na po = (match na with | Some (_,Name id) -> @@ -561,38 +536,6 @@ let pr pr sep inherited a = pr_with_comments loc (sep() ++ if prec_less prec inherited then strm else surround strm) - -let rec strip_context n iscast t = - if n = 0 then - [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t - else match t with - | CLambdaN (loc,(nal,bk,t)::bll,c) -> - let n' = List.length nal in - if n' > n then - let nal1,nal2 = list_chop n nal in - [LocalRawAssum (nal1,bk,t)], CLambdaN (loc,(nal2,bk,t)::bll,c) - else - let bl', c = strip_context (n-n') iscast - (if bll=[] then c else CLambdaN (loc,bll,c)) in - LocalRawAssum (nal,bk,t) :: bl', c - | CProdN (loc,(nal,bk,t)::bll,c) -> - let n' = List.length nal in - if n' > n then - let nal1,nal2 = list_chop n nal in - [LocalRawAssum (nal1,bk,t)], CProdN (loc,(nal2,bk,t)::bll,c) - else - let bl', c = strip_context (n-n') iscast - (if bll=[] then c else CProdN (loc,bll,c)) in - LocalRawAssum (nal,bk,t) :: bl', c - | CArrow (loc,t,c) -> - let bl', c = strip_context (n-1) iscast c in - LocalRawAssum ([loc,Anonymous],default_binder_kind,t) :: bl', c - | CCast (_,c,_) -> strip_context n false c - | CLetIn (_,na,b,c) -> - let bl', c = strip_context (n-1) iscast c in - LocalRawDef (na,b) :: bl', c - | _ -> anomaly "strip_context" - type term_pr = { pr_constr_expr : constr_expr -> std_ppcmds; pr_lconstr_expr : constr_expr -> std_ppcmds; diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 864b5b227..64b8b7bc9 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -90,8 +90,6 @@ let pr_quantified_hypothesis = function | AnonHyp n -> int n | NamedHyp id -> pr_id id -let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h - let pr_binding prc = function | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) @@ -130,11 +128,6 @@ let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s) let with_evars ev s = if ev then "e" ^ s else s -let out_bindings = function - | ImplicitBindings l -> ImplicitBindings (List.map snd l) - | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l) - | NoBindings -> NoBindings - let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = @@ -294,8 +287,6 @@ let pr_extend prc prlc prtac prpat = (**********************************************************************) (* The tactic printer *) -let sep_v = fun _ -> str"," ++ spc() - let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = match ty with @@ -316,8 +307,6 @@ let pr_ltac_or_var pr = function | ArgArg x -> pr x | ArgVar (loc,id) -> pr_with_comments loc (pr_id id) -let pr_arg pr x = spc () ++ pr x - let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp) @@ -326,12 +315,6 @@ let pr_evaluable_reference_env env = function | EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp) -let pr_quantified_hypothesis = function - | AnonHyp n -> int n - | NamedHyp id -> pr_id id - -let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h - let pr_esubst prc l = let pr_qhyp = function (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" @@ -356,10 +339,6 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc let pr_with_bindings prlc prc (c,bl) = hov 1 (prc c ++ pr_bindings prlc prc bl) -let pr_with_constr prc = function - | None -> mt () - | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) - let pr_with_induction_names = function | None, None -> mt () | eqpat, ipat -> @@ -441,15 +420,6 @@ let pr_clauses default_is_concl pr_id = function (if occs = no_occurrences_expr then mt () else pr_with_occurrences (fun () -> str" |- *") (occs,()))) -let pr_clause_pattern pr_id = function - | (None, []) -> mt () - | (glopt,l) -> - str " in" ++ - prlist - (fun (id,nl) -> prlist (pr_arg int) nl - ++ spc () ++ pr_id id) l ++ - pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt - let pr_orient b = if b then mt () else str " <-" let pr_multi = function @@ -546,20 +516,6 @@ let pr_auto_using prc = function | l -> spc () ++ hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l) -let pr_autoarg_adding = function - | [] -> mt () - | l -> - spc () ++ str "adding [" ++ - hv 0 (prlist_with_sep spc pr_reference l) ++ str "]" - -let pr_autoarg_destructing = function - | true -> spc () ++ str "destructing" - | false -> mt () - -let pr_autoarg_usingTDB = function - | true -> spc () ++ str "using tdb" - | false -> mt () - let pr_then () = str ";" let ltop = (5,E) @@ -1037,9 +993,6 @@ let rec raw_printers = and pr_raw_tactic_level env n (t:raw_tactic_expr) = fst (make_pr_tac raw_printers env) n t -and pr_raw_match_rule env t = - snd (make_pr_tac raw_printers env) t - let pr_and_constr_expr pr (c,_) = pr c let pr_pat_and_constr_expr b (c,_) = @@ -1061,9 +1014,6 @@ let rec glob_printers = and pr_glob_tactic_level env n (t:glob_tactic_expr) = fst (make_pr_tac glob_printers env) n t -and pr_glob_match_rule env t = - snd (make_pr_tac glob_printers env) t - let pr_constr_or_lconstr_pattern b = if b then pr_lconstr_pattern else pr_constr_pattern diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index b0ae6d139..ba3371ee3 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -84,27 +84,12 @@ let rec match_vernac_rule tys = function else match_vernac_rule tys rls let sep = fun _ -> spc() -let sep_p = fun _ -> str"." -let sep_v = fun _ -> str"," let sep_v2 = fun _ -> str"," ++ spc() -let sep_pp = fun _ -> str":" let pr_ne_sep sep pr = function [] -> mt() | l -> sep() ++ pr l -let pr_entry_prec = function - | Some LeftA -> str"LEFTA " - | Some RightA -> str"RIGHTA " - | Some NonA -> str"NONA " - | None -> mt() - -let pr_prec = function - | Some LeftA -> str", left associativity" - | Some RightA -> str", right associativity" - | Some NonA -> str", no associativity" - | None -> mt() - let pr_set_entry_type = function | ETName -> str"ident" | ETReference -> str"global" @@ -168,11 +153,6 @@ let pr_explanation (e,b,f) = let a = if f then str"!" ++ a else a in if b then str "[" ++ a ++ str "]" else a -let pr_class_rawexpr = function - | FunClass -> str"Funclass" - | SortClass -> str"Sortclass" - | RefClass qid -> pr_smart_global qid - let pr_option_ref_value = function | QualidRefValue id -> pr_reference id | StringRefValue s -> qs s @@ -290,9 +270,6 @@ let pr_decl_notation prc ((loc,ntn),c,scopt) = fnl () ++ str "where " ++ qs ntn ++ str " := " ++ prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt -let pr_vbinders l = - hv 0 (pr_binders l) - let pr_binders_arg = pr_ne_sep spc pr_binders @@ -421,21 +398,6 @@ let pr_grammar_tactic_rule n (_,pil,t) = hov 0 (prlist_with_sep sep pr_production_item pil ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) -let pr_box b = let pr_boxkind = function - | PpHB n -> str"h" ++ spc() ++ int n - | PpVB n -> str"v" ++ spc() ++ int n - | PpHVB n -> str"hv" ++ spc() ++ int n - | PpHOVB n -> str"hov" ++ spc() ++ int n - | PpTB -> str"t" -in str"<" ++ pr_boxkind b ++ str">" - -let pr_paren_reln_or_extern = function - | None,L -> str"L" - | None,E -> str"E" - | Some pprim,Any -> qs pprim - | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p - | _ -> mt() - let pr_statement head (id,(bl,c,guard)) = assert (id<>None); hov 0 diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 62dd94893..c4e378826 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -39,7 +39,6 @@ type object_pr = { print_module : bool -> Names.module_path -> std_ppcmds; print_modtype : module_path -> std_ppcmds; print_named_decl : identifier * constr option * types -> std_ppcmds; - print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; @@ -457,11 +456,6 @@ let gallina_print_library_entry with_values ent = | (_,Lib.FrozenState _) -> None -let gallina_print_leaf_entry with_values c = - match gallina_print_leaf_entry with_values c with - | None -> mt () - | Some pp -> pp ++ fnl() - let gallina_print_context with_values = let rec prec n = function | h::rest when n = None or Option.get n > 0 -> @@ -487,7 +481,6 @@ let default_object_pr = { print_module = gallina_print_module; print_modtype = gallina_print_modtype; print_named_decl = gallina_print_named_decl; - print_leaf_entry = gallina_print_leaf_entry; print_library_entry = gallina_print_library_entry; print_context = gallina_print_context; print_typed_value_in_env = gallina_print_typed_value_in_env; @@ -504,7 +497,6 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x let print_module x = !object_pr.print_module x let print_modtype x = !object_pr.print_modtype x let print_named_decl x = !object_pr.print_named_decl x -let print_leaf_entry x = !object_pr.print_leaf_entry x let print_library_entry x = !object_pr.print_library_entry x let print_context x = !object_pr.print_context x let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x @@ -583,16 +575,6 @@ let print_full_pure_context () = assume that the declaration of constructors and eliminations follows the definition of the inductive type *) -let list_filter_vec f vec = - let rec frec n lf = - if n < 0 then lf - else if f vec.(n) then - frec (n-1) (vec.(n)::lf) - else - frec (n-1) lf - in - frec (Array.length vec -1) [] - (* This is designed to print the contents of an opened section *) let read_sec_context r = let loc,qid = qualid_of_reference r in @@ -692,15 +674,6 @@ let print_impargs ref = (if has_impl then print_impl_args impl else (str "No implicit arguments" ++ fnl ())) -let unfold_head_fconst = - let rec unfrec k = match kind_of_term k with - | Const cst -> constant_value (Global.env ()) cst - | Lambda (na,t,b) -> mkLambda (na,t,unfrec b) - | App (f,v) -> appvect (unfrec f,v) - | _ -> k - in - unfrec - (* for debug *) let inspect depth = print_context false (Some depth) (Lib.contents_after None) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index a7820e034..842fc4e89 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -74,7 +74,6 @@ type object_pr = { print_module : bool -> Names.module_path -> std_ppcmds; print_modtype : module_path -> std_ppcmds; print_named_decl : identifier * constr option * types -> std_ppcmds; - print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; diff --git a/parsing/printer.ml b/parsing/printer.ml index 5d6837e13..34637b1e8 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -242,18 +242,6 @@ let pr_context_of env = match Flags.print_hyps_limit () with (* display goal parts (Proof mode) *) -let pr_restricted_named_context among env = - hv 0 (fold_named_context - (fun env ((id,_,_) as d) pps -> - if true || Idset.mem id among then - pps ++ - fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ - pr_var_decl env d - else - pps) - env ~init:(mt ())) - - let pr_predicate pr_elt (b, elts) = let pr_elts = prlist_with_sep spc pr_elt elts in if b then @@ -269,13 +257,6 @@ let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) -let pr_subgoal_metas metas env= - let pr_one (meta,typ) = - str "?" ++ int meta ++ str " : " ++ - hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253)) "") in - hv 0 (prlist_with_sep mt pr_one metas) - (* display complete goal *) let default_pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index 34b32c0a7..b800170de 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -37,7 +37,7 @@ let set_trace b = trace := b let timeout = ref 10 let set_timeout n = timeout := n -let (dp_timeout_obj,_) = +let dp_timeout_obj = declare_object {(default_object "Dp_timeout") with cache_function = (fun (_,x) -> set_timeout x); @@ -45,7 +45,7 @@ let (dp_timeout_obj,_) = let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x) -let (dp_debug_obj,_) = +let dp_debug_obj = declare_object {(default_object "Dp_debug") with cache_function = (fun (_,x) -> set_debug x); @@ -53,7 +53,7 @@ let (dp_debug_obj,_) = let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x) -let (dp_trace_obj,_) = +let dp_trace_obj = declare_object {(default_object "Dp_trace") with cache_function = (fun (_,x) -> set_trace x); @@ -826,7 +826,7 @@ let prelude_files = ref ([] : string list) let set_prelude l = prelude_files := l -let (dp_prelude_obj,_) = +let dp_prelude_obj = declare_object {(default_object "Dp_prelude") with cache_function = (fun (_,x) -> set_prelude x); @@ -1088,7 +1088,7 @@ let dp_hint l = in List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l) -let (dp_hint_obj,_) = +let dp_hint_obj = declare_object {(default_object "Dp_hint") with cache_function = (fun (_,l) -> dp_hint l); @@ -1114,7 +1114,7 @@ let dp_predefined qid s = with NotFO -> msg_warning (str " ignored (not a first order declaration)") -let (dp_predefined_obj,_) = +let dp_predefined_obj = declare_object {(default_object "Dp_predefined") with cache_function = (fun (_,(id,s)) -> dp_predefined id s); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 5457d2e8c..a292dec2f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -459,7 +459,7 @@ let lang_ref = ref Ocaml let lang () = !lang_ref -let (extr_lang,_) = +let extr_lang = declare_object {(default_object "Extraction Lang") with cache_function = (fun (_,l) -> lang_ref := l); @@ -491,7 +491,7 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) -let (inline_extraction,_) = +let inline_extraction = declare_object {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); @@ -534,7 +534,7 @@ let print_extraction_inline () = (* Reset part *) -let (reset_inline,_) = +let reset_inline = declare_object {(default_object "Reset Extraction Inline") with cache_function = (fun (_,_)-> inline_table := empty_inline_table); @@ -573,7 +573,7 @@ let add_implicits r l = (* Registration of operations for rollback. *) -let (implicit_extraction,_) = +let implicit_extraction = declare_object {(default_object "Extraction Implicit") with cache_function = (fun (_,(r,l)) -> add_implicits r l); @@ -633,7 +633,7 @@ let add_blacklist_entries l = (* Registration of operations for rollback. *) -let (blacklist_extraction,_) = +let blacklist_extraction = declare_object {(default_object "Extraction Blacklist") with cache_function = (fun (_,l) -> add_blacklist_entries l); @@ -661,7 +661,7 @@ let print_extraction_blacklist () = (* Reset part *) -let (reset_blacklist,_) = +let reset_blacklist = declare_object {(default_object "Reset Extraction Blacklist") with cache_function = (fun (_,_)-> blacklist_table := Idset.empty); @@ -707,7 +707,7 @@ let find_custom_match pv = (* Registration of operations for rollback. *) -let (in_customs,_) = +let in_customs = declare_object {(default_object "ML extractions") with cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); @@ -722,7 +722,7 @@ let _ = declare_summary "ML extractions" unfreeze_function = ((:=) customs); init_function = (fun () -> customs := Refmap'.empty) } -let (in_custom_matchs,_) = +let in_custom_matchs = declare_object {(default_object "ML extractions custom matchs") with cache_function = (fun (_,(r,s)) -> add_custom_match r s); diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index d4ced4139..1cba563ea 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -65,7 +65,7 @@ let subst_addfield (subst,(typ,th as obj)) = (typ',th') (* Declaration of the Add Field library object *) -let (in_addfield,out_addfield)= +let in_addfield = Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with Libobject.open_function = (fun i o -> if i=1 then cache_addfield o); Libobject.cache_function = cache_addfield; diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index ff7089613..002fb7098 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -362,7 +362,7 @@ let pr_table tb = let l = Cmap.fold (fun k v acc -> v::acc) tb [] in Util.prlist_with_sep fnl pr_info l -let in_Function,out_Function = +let in_Function = Libobject.declare_object {(Libobject.default_object "FUNCTIONS_DB") with Libobject.cache_function = cache_Function; diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 8b977e5dc..7588e6a2f 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -262,7 +262,7 @@ let subst_th (subst,(c,th as obj)) = (c',th') -let (theory_to_obj, obj_to_theory) = +let theory_to_obj = let cache_th (_,(c, th)) = theories_map_add (c,th) in declare_object {(default_object "tactic-ring-theory") with open_function = (fun i o -> if i=1 then cache_th o); diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index fa0e76841..052406867 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -440,7 +440,7 @@ let subst_th (subst,th) = ring_post_tac = posttac' } -let (theory_to_obj, obj_to_theory) = +let theory_to_obj = let cache_th (name,th) = add_entry name th in declare_object {(default_object "tactic-new-ring-theory") with @@ -1016,7 +1016,7 @@ let subst_th (subst,th) = field_pre_tac = pretac'; field_post_tac = posttac' } -let (ftheory_to_obj, obj_to_ftheory) = +let ftheory_to_obj = let cache_th (name,th) = add_field_entry name th in declare_object {(default_object "tactic-new-field-theory") with diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 591e01c04..22cc745f6 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -153,7 +153,7 @@ let _ = let progmap_union = ProgMap.fold ProgMap.add -let (input,output) = +let input = declare_object { (default_object "Program state") with classify_function = (fun () -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b8c13a2f7..cc9aa0060 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -749,16 +749,6 @@ let insert_aliases env sigma alias eqns = (**********************************************************************) (* Functions to deal with elimination predicate *) -exception Occur -let noccur_between_without_evar n m term = - let rec occur_rec n c = match kind_of_term c with - | Rel p -> if n<=p && p<n+m then raise Occur - | Evar (_,cl) -> () - | _ -> iter_constr_with_binders succ occur_rec n c - in - (m = 0) or (try occur_rec n term; true with Occur -> false) - - (* Infering the predicate *) (* The problem to solve is the following: diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 66263aee3..85112c288 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -92,13 +92,6 @@ let rec shift_value n = function let shift_value n v = if n = 0 then v else shift_value n v -let rec shift_stack n = function - TOP -> TOP - | APP(v,stk) -> APP(Array.map (shift_value n) v, shift_stack n stk) - | CASE(c,b,i,s,stk) -> CASE(c,b,i,subs_shft(n,s), shift_stack n stk) -let shift_stack n stk = - if n = 0 then stk else shift_stack n stk - (* Contracts a fixpoint: given a fixpoint and a bindings, * returns the corresponding fixpoint body, and the bindings in which * it should be evaluated: its first variables are the fixpoint bodies diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 73ce8134f..2d2677ee0 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -398,7 +398,7 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) = let classify_coercion (coe,stre,isid,cls,clt,ps as obj) = if stre = Local then Dispose else Substitute obj -let (inCoercion,_) = +let inCoercion = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0dcaf1444..04dc13290 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -166,8 +166,6 @@ let computable p k = && noccur_between 1 (k+1) ccl -let avoid_flag isgoal = if isgoal then Some true else None - let lookup_name_as_displayed env t s = let rec lookup avoid n c = match kind_of_term c with | Prod (name,_,c') -> diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 3f899a8ec..4ad823e06 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1394,33 +1394,8 @@ let check_evars env initial_sigma sigma c = | _ -> iter_constr proc_rec c in proc_rec c -(* Substitutes undefined evars by evars of same context up to renaming *) - -let subst_evar_evar subst c = - let rec aux c = match kind_of_term c with - | Evar (evk,args) -> - let evk' = try ExistentialMap.find evk subst with Not_found -> evk in - mkEvar (evk',Array.map aux args) - | _ -> map_constr aux c - in aux c - -let subst_undefined_evar_info_evar subst evi = - { evi with - evar_hyps = map_named_val (subst_evar_evar subst) evi.evar_hyps; - evar_concl = subst_evar_evar subst evi.evar_concl } - open Rawterm -let subst_evar_evar_in_constr_with_bindings subst (c,bl) = - (subst_evar_evar subst c, - match bl with - | ImplicitBindings largs -> - ImplicitBindings (List.map (subst_evar_evar subst) largs) - | ExplicitBindings lbind -> - ExplicitBindings (List.map (on_pi3 (subst_evar_evar subst)) lbind) - | NoBindings -> - NoBindings) - (* Operations on value/type constraints *) type type_constraint_type = (int * int) option * constr diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 22f0c256d..c70c13d9e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -96,8 +96,6 @@ module EvarInfoMap = struct type t = evar_info ExistentialMap.t * evar_info ExistentialMap.t let empty = ExistentialMap.empty, ExistentialMap.empty - let is_empty (def,undef) = - (ExistentialMap.is_empty def, ExistentialMap.is_empty undef) let to_list (def,undef) = (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 8a0966ae3..5bd8b44f9 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -146,9 +146,6 @@ let make_case_info env ind style = ci_cstr_ndecls = mip.mind_consnrealdecls; ci_pp_info = print_info } -let make_default_case_info env style ind = - make_case_info env ind style - (*s Useful functions *) type constructor_summary = { @@ -200,12 +197,6 @@ let get_constructors env (ind,params) = Array.init (Array.length mip.mind_consnames) (fun j -> get_constructor (ind,mib,mip,params) (j+1)) -let rec instantiate args c = match kind_of_term c, args with - | Prod (_,_,c), a::args -> instantiate args (subst1 a c) - | LetIn (_,b,_,c), args -> instantiate args (subst1 b c) - | _, [] -> c - | _ -> anomaly "too short arity" - (* substitution in a signature *) let substnl_rel_context subst n sign = diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 3f117786c..b971db135 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -85,13 +85,6 @@ let build_lambda toabstract stk (m : constr) = in buildrec m 1 stk -let memb_metavars m n = - match (m,n) with - | (None, _) -> true - | (Some mvs, n) -> List.mem n mvs - -let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 - let same_case_structure (_,cs1,ind,_) ci2 br1 br2 = match ind with | Some ind -> ind = ci2.ci_ind diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index c703d5be7..15bc06e02 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -59,12 +59,6 @@ let rec occur_meta_pattern = function | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false -type constr_label = - | ConstNode of constant - | IndNode of inductive - | CstrNode of constructor - | VarNode of identifier - exception BoundPattern;; let rec head_pattern_bound t = @@ -155,8 +149,6 @@ let map_pattern_with_binders g f l = function (* Bound to terms *) | PFix _ | PCoFix _ as x) -> x -let map_pattern f = map_pattern_with_binders (fun _ () -> ()) (fun () -> f) () - let error_instantiate_pattern id l = let is = if List.length l = 1 then "is" else "are" in errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f75f4990a..d477ec34a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -76,7 +76,7 @@ let discharge_structure (_,(ind,id,kl,projs)) = Some (Lib.discharge_inductive ind, discharge_constructor id, kl, List.map (Option.map Lib.discharge_con) projs) -let (inStruc,outStruc) = +let inStruc = declare_object {(default_object "STRUCTURE") with cache_function = cache_structure; load_function = load_structure; @@ -135,7 +135,7 @@ open Libobject let load_method (_,(ty,id)) = meth_dnet := MethodsDnet.add ty id !meth_dnet -let (in_method,out_method) = +let in_method = declare_object { (default_object "RECMETHODS") with load_function = (fun _ -> load_method); @@ -290,7 +290,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) = let discharge_canonical_structure (_,(cst,ind)) = Some (Lib.discharge_con cst,Lib.discharge_inductive ind) -let (inCanonStruc,outCanonStruct) = +let inCanonStruc = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; @@ -328,8 +328,6 @@ let check_and_decompose_canonical_structure ref = let declare_canonical_structure ref = add_canonical_structure (check_and_decompose_canonical_structure ref) -let outCanonicalStructure x = fst (outCanonStruct x) - let lookup_canonical_conversion (proj,pat) = List.assoc pat (Refmap.find proj !object_table) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 78a5341b1..689e544b8 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -42,13 +42,6 @@ let append_stack_list l s = | (l1, s) -> Zapp l1 :: s let append_stack v s = append_stack_list (Array.to_list v) s -(* Collapse the shifts in the stack *) -let zshift n s = - match (n,s) with - (0,_) -> s - | (_,Zshift(k)::s) -> Zshift(n+k)::s - | _ -> Zshift(n)::s - let rec stack_args_size = function | Zapp l::s -> List.length l + stack_args_size s | Zshift(_)::s -> stack_args_size s @@ -61,10 +54,6 @@ let rec decomp_stack = function | Zapp(v::l)::s -> Some (v, (Zapp l :: s)) | Zapp [] :: s -> decomp_stack s | _ -> None -let rec decomp_stackn = function - | Zapp [] :: s -> decomp_stackn s - | Zapp l :: s -> (Array.of_list l, s) - | _ -> assert false let array_of_stack s = let rec stackrec = function | [] -> [] @@ -153,10 +142,6 @@ let whd_stack sigma x = appterm_of_stack (whd_app_state sigma (x, empty_stack)) let whd_castapp_stack = whd_stack -let stack_reduction_of_reduction red_fun env sigma s = - let t = red_fun env sigma (app_stack s) in - whd_stack t - let strong whdfun env sigma t = let rec strongrec env t = map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in @@ -584,14 +569,6 @@ let rec whd_betaiota_preserving_vm_cast env sigma t = let nf_betaiota_preserving_vm_cast = strong whd_betaiota_preserving_vm_cast -(* lazy weak head reduction functions *) -let whd_flags flgs env sigma t = - try - whd_val - (create_clos_infos ~evars:(safe_evar_value sigma) flgs env) - (inject t) - with Anomaly _ -> error "Tried to normalized ill-typed term" - (********************************************************************) (* Conversion *) (********************************************************************) @@ -924,17 +901,6 @@ let nf_meta sigma c = meta_instance sigma (mk_freelisted c) (* Instantiate metas that create beta/iota redexes *) -let meta_value evd mv = - let rec valrec mv = - match meta_opt_fvalue evd mv with - | Some (b,_) -> - instance evd - (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) - b.rebus - | None -> mkMeta mv - in - valrec mv - let meta_reducible_instance evd b = let fm = Metaset.elements b.freemetas in let metas = List.fold_left (fun l mv -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index a7a5d84c1..e99baa291 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -299,17 +299,6 @@ let reference_eval sigma env = function end) | ref -> compute_consteval sigma env ref -let rev_firstn_liftn fn ln = - let rec rfprec p res l = - if p = 0 then - res - else - match l with - | [] -> invalid_arg "Reduction.rev_firstn_liftn" - | a::rest -> rfprec (p-1) ((lift ln a)::res) rest - in - rfprec fn [] - (* If f is bound to EliminationFix (n',infos), then n' is the minimal number of args for starting the reduction and infos is (nbfix,[(yi1,Ti1);...;(yip,Tip)],n) indicating that f converts diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 93418c6e6..17e052223 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -32,7 +32,6 @@ let pr_name = function | Name id -> pr_id id | Anonymous -> str "_" -let pr_path sp = str(string_of_kn sp) let pr_con sp = str(string_of_con sp) let rec pr_constr c = match kind_of_term c with diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index b381f295c..b1cbed4af 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -32,10 +32,6 @@ let register_set_typeclass_transparency = (:=) set_typeclass_transparency_ref let set_typeclass_transparency gr c = !set_typeclass_transparency_ref gr c -let mismatched_params env n m = mismatched_ctx_inst env Parameters n m -(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *) -let mismatched_props env n m = mismatched_ctx_inst env Properties n m - type rels = constr list (* This module defines type-classes *) @@ -197,7 +193,7 @@ let discharge_class (_,cl) = let rebuild_class cl = cl -let (class_input,class_output) = +let class_input = declare_object { (default_object "type classes state") with cache_function = cache_class; @@ -246,7 +242,7 @@ let classify_instance inst = if inst.is_global = -1 then Dispose else Substitute inst -let (instance_input,instance_output) = +let instance_input = declare_object { (default_object "type classes instances state") with cache_function = cache_instance; @@ -304,13 +300,6 @@ let instance_constructor cl args = let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes [] -let cmapl_add x y m = - try - let l = Gmap.find x m in - Gmap.add x (Gmap.add y.is_impl y l) m - with Not_found -> - Gmap.add x (Gmap.add y.is_impl y Gmap.empty) m - let cmap_elements c = Gmap.fold (fun k v acc -> v :: acc) c [] let instances_of c = diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 8340af0fc..c39be8b68 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -190,8 +190,6 @@ and execute_recdef env evdref (names,lar,vdef) = and execute_array env evdref = Array.map (execute env evdref) -and execute_list env evdref = List.map (execute env evdref) - let check env evd c t = let evdref = ref evd in let j = execute env evdref c in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 12b734e56..70f2f6b64 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -30,9 +30,7 @@ open Coercion.Default (* Abbreviations *) let pf_env = Refiner.pf_env -let pf_hyps = Refiner.pf_hyps let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c -let pf_concl gls = Goal.V82.concl (Refiner.project gls) (sig_it gls) (******************************************************************) (* Clausal environments *) @@ -144,9 +142,6 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_rename_from_n gls n (c,t) = - mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t) - let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) (******************************************************************) diff --git a/proofs/logic.ml b/proofs/logic.ml index 6438f5855..593ef0b32 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -694,27 +694,6 @@ type variable_proof_status = ProofVar | SectionVar of identifier type proof_variable = name * variable_proof_status -let subst_proof_vars = - let rec aux p vars = - let _,subst = - List.fold_left (fun (n,l) var -> - let t = match var with - | Anonymous,_ -> l - | Name id, ProofVar -> (id,mkRel n)::l - | Name id, SectionVar id' -> (id,mkVar id')::l in - (n+1,t)) (p,[]) vars - in replace_vars (List.rev subst) - in aux 1 - -let rec rebind id1 id2 = function - | [] -> [Name id2,SectionVar id1] - | (na,k as x)::l -> - if na = Name id1 then (Name id2,k)::l else - let l' = rebind id1 id2 l in - if na = Name id2 then (Anonymous,k)::l' else x::l' - -let add_proof_var id vl = (Name id,ProofVar)::vl - let proof_variable_index x = let rec aux n = function | (Name id,ProofVar)::l when x = id -> n diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2f2e2016b..cafe45485 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -37,7 +37,7 @@ let _ = register_proof_mode standard (* Default proof mode, to be set at the beginning of proofs. *) let default_proof_mode = ref standard -let set_default_proof_mode = +let _ = Goptions.declare_string_option {Goptions. optsync = true ; optname = "default proof mode" ; diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6304564b9..d150f2a38 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -85,7 +85,7 @@ let discharge_strategy (_,(local,obj)) = if local then None else map_strategy disch_ref obj -let (inStrategy,outStrategy) = +let inStrategy = declare_object {(default_object "STRATEGY") with cache_function = (fun (_,obj) -> cache_strategy obj); load_function = (fun _ (_,obj) -> cache_strategy obj); @@ -211,7 +211,7 @@ let subst_red_expr subs e = (Pattern.subst_pattern subs) e -let (inReduction,_) = +let inReduction = declare_object {(default_object "REDUCTION") with cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e); diff --git a/proofs/refiner.ml b/proofs/refiner.ml index b094eea6b..eeccbd0e5 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -24,29 +24,11 @@ open Logic let sig_it x = x.it let project x = x.sigma - -let and_status = List.fold_left (+) 0 - (* Getting env *) let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) -(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]] - gives - [ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ; - (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ] - *) - -let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) - (l : proof_tree list) = - match nl with - | [] -> [] - | h::t -> - let m,l = list_chop h l in - (List.hd fl m) :: (mapshape t (List.tl fl) l) - - let abstract_operation syntax semantics = semantics diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 49423d3d7..855d2cea7 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -105,14 +105,6 @@ type 'id gclause = let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr} -let goal_location_of = function -| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr -> - Some scl -| { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr -> - None -| _ -> - error "Not a simple \"in\" clause (one hypothesis or the conclusion)" - type 'constr induction_clause = ('constr with_bindings induction_arg list * 'constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option)) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index e9ae0154f..116526d61 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -204,10 +204,6 @@ open Pp open Tacexpr open Rawterm -let rec pr_list f = function - | [] -> mt () - | a::l1 -> (f a) ++ pr_list f l1 - let db_pr_goal sigma g = let env = Goal.V82.env sigma g in let penv = print_named_context env in diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 3b518f5db..1c2fb2787 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -154,11 +154,6 @@ let db_mc_pattern_success debug = msgnl (str "The goal has been successfully matched!" ++ fnl() ++ str "Let us execute the right-hand side part..." ++ fnl()) -let pp_match_pattern env = function - | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c) - | Subterm (b,o,c) -> - Subterm (b,o,(extern_constr_pattern (names_of_rel_context env) c)) - (* Prints a failure message for an hypothesis pattern *) let db_hyp_pattern_failure debug env (na,hyp) = if debug <> DebugOff & !skip = 0 then diff --git a/tactics/auto.ml b/tactics/auto.ml index fbdf8683e..17a2ea174 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -487,17 +487,7 @@ let subst_autohint (subst,(local,name,hintlist as obj)) = let classify_autohint ((local,name,hintlist) as obj) = if local or hintlist = (AddTactic []) then Dispose else Substitute obj -let discharge_autohint (_,(local,name,hintlist as obj)) = - if local then None else - match hintlist with - | CreateDB _ -> - (* We assume that the transparent state is either empty or full *) - Some obj - | AddTransparency _ | AddTactic _ -> - (* Needs the adequate code here to support Global Hints in sections *) - None - -let (inAutoHint,_) = +let inAutoHint = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; load_function = (fun _ -> cache_autohint); @@ -953,8 +943,6 @@ let gen_trivial lems = function | None -> full_trivial lems | Some l -> trivial lems l -let inj_open c = (Evd.empty,c) - let h_trivial lems l = Refiner.abstract_tactic (TacTrivial (lems,l)) (gen_trivial lems l) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c49787356..fb5b2f527 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -223,7 +223,7 @@ let classify_hintrewrite x = Libobject.Substitute x (* Declaration of the Hint Rewrite library object *) -let (inHintRewrite,_)= +let inHintRewrite = Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with Libobject.cache_function = cache_hintrewrite; Libobject.load_function = (fun _ -> cache_hintrewrite); diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index cb52ec5b9..36fa43ff2 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -45,18 +45,6 @@ let _ = Auto.auto_init := (fun () -> exception Found of evar_map -let is_dependent ev evm = - Evd.fold (fun ev' evi dep -> - if ev = ev' then dep - else dep || occur_evar ev evi.evar_concl) - evm false - -let evar_filter evi = - let hyps' = evar_filtered_context evi in - { evi with - evar_hyps = Environ.val_of_named_context hyps'; - evar_filter = List.map (fun _ -> true) hyps' } - let evars_to_goals p evm = let goals, evm' = Evd.fold @@ -86,8 +74,6 @@ let e_give_exact flags c gl = let t1 = (pf_type_of gl c) in tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl -let assumption flags id = e_give_exact flags (mkVar id) - open Unification let auto_unif_flags = { @@ -210,9 +196,6 @@ let rec catchable = function | Loc.Exc_located (_, e) -> catchable e | e -> Logic.catchable_exception e -let is_ground gl = - Evarutil.is_ground_term (project gl) (pf_concl gl) - let nb_empty_evars s = Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0 @@ -296,10 +279,6 @@ let normevars_tac : atac = (* in {it = gls'; sigma = s}) *) -let id_tac : atac = - { skft = fun sk fk {it = gl; sigma = s} -> - sk {it = [gl]; sigma = s} fk } - (* Ordering of states is lexicographic on the number of remaining goals. *) let compare (pri, _, _, res) (pri', _, _, res') = let nbgoals s = @@ -312,16 +291,6 @@ let compare (pri, _, _, res) (pri', _, _, res') = let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls } -let solve_tac (x : 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> - if gls = [] then sk res fk else fk ()) fk gls } - -let solve_unif_tac : atac = - { skft = fun sk fk {it = gl; sigma = s} -> - try let s' = Evarconv.consider_remaining_unif_problems (Global.env ()) s in - normevars_tac.skft sk fk ({it=gl; sigma=s'}) - with _ -> fk () } - let hints_tac hints = { skft = fun sk fk {it = gl,info; sigma = s} -> let possible_resolve (lgls as res, pri, b, pp) = @@ -387,17 +356,6 @@ let evars_of_term c = | _ -> fold_constr evrec acc c in evrec Intset.empty c -exception Found_evar of int - -let occur_evars evars c = - try - let rec evrec c = - match kind_of_term c with - | Evar (n, _) -> if Intset.mem n evars then raise (Found_evar n) else () - | _ -> iter_constr evrec c - in evrec c; false - with Found_evar _ -> true - let dependent only_classes evd oev concl = let concl_evars = Intset.union (evars_of_term concl) (Option.cata Intset.singleton Intset.empty oev) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index f6f12b91b..d9addd1f0 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -220,7 +220,7 @@ let subst_dd (subst,(local,na,dd)) = d_pri = dd.d_pri; d_code = !forward_subst_tactic subst dd.d_code }) -let (inDD,_) = +let inDD = declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with cache_function = cache_dd; open_function = (fun i o -> if i=1 then cache_dd o); diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index d2e45475e..fab8d2d45 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -410,19 +410,6 @@ let autounfold db cls gl = | OnConcl occs -> tac occs None) cls gl -let autosimpl db cl = - let unfold_of_elts constr (b, elts) = - if not b then - List.map (fun c -> all_occurrences, constr c) elts - else [] - in - let unfolds = List.concat (List.map (fun dbname -> - let db = searchtable_map dbname in - let (ids, csts) = Hint_db.transparent_state db in - unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @ - unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db) - in unfold_option unfolds cl - open Extraargs TACTIC EXTEND autounfold diff --git a/tactics/elim.ml b/tactics/elim.ml index 1a78a509f..1ff8800f1 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -109,12 +109,6 @@ let head_in gls indl t = in List.mem ity indl with Not_found -> false -let inductive_of = function - | IndRef ity -> ity - | r -> - errorlabstrm "Decompose" - (Printer.pr_global r ++ str " is not an inductive type.") - let decompose_these c l gls = let indl = (*List.map inductive_of*) l in general_decompose (fun (_,t) -> head_in gls indl t) c gls @@ -134,8 +128,6 @@ let decompose_or c gls = (fun (_,t) -> is_disjunction t) c gls -let inj_open c = (Evd.empty,c) - let h_decompose l c = Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l) diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index fbf36c1c3..4fbe361e0 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -46,10 +46,6 @@ let optimize_non_type_induction_scheme kind dep sort ind = let build_induction_scheme_in_type dep sort ind = build_induction_scheme (Global.env()) Evd.empty ind dep sort -let rect_scheme_kind_from_type = - declare_individual_scheme_object "_rect_nodep" - (build_induction_scheme_in_type false InType) - let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" (build_induction_scheme_in_type false InType) @@ -58,14 +54,6 @@ let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" (build_induction_scheme_in_type true InType) -let rect_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_rect_dep" - (build_induction_scheme_in_type true InType) - -let ind_scheme_kind_from_type = - declare_individual_scheme_object "_ind_nodep" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp) - let ind_scheme_kind_from_prop = declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp) @@ -74,14 +62,6 @@ let ind_dep_scheme_kind_from_type = declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp) -let ind_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_ind_dep" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InProp) - -let rec_scheme_kind_from_type = - declare_individual_scheme_object "_rec_nodep" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) - let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) @@ -90,10 +70,6 @@ let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) -let rec_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_rec_dep" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InSet) - (* Case analysis *) let build_case_analysis_scheme_in_type dep sort ind = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 3bf6c5824..49ff459c6 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -432,7 +432,7 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) -let (inTransitivity,_) = +let inTransitivity = declare_object {(default_object "TRANSITIVITY-STEPS") with cache_function = cache_transitivity_lemma; open_function = (fun i o -> if i=1 then cache_transitivity_lemma o); diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 23d555f8d..c31980158 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -34,8 +34,6 @@ open Vernacexpr open Safe_typing open Decl_kinds -let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments" - let no_inductive_inconstr env constr = (str "Cannot recognize an inductive predicate in " ++ pr_lconstr_env env constr ++ @@ -86,18 +84,6 @@ let no_inductive_inconstr env constr = *) -let thin_ids env (hyps,vars) = - fst - (List.fold_left - (fun ((ids,globs) as sofar) (id,c,a) -> - if List.mem id globs then - match c with - | None -> (id::ids,(global_vars env a)@globs) - | Some body -> - (id::ids,(global_vars env body)@(global_vars env a)@globs) - else sofar) - ([],vars) hyps) - (* returns the sub_signature of sign corresponding to those identifiers that * are not global. *) (* diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index f79bfa0ff..3bed376ff 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -71,28 +71,20 @@ let try_find_reference dir s = constr_of_global (try_find_global_reference dir s) let gen_constant dir s = Coqlib.gen_constant "rewrite" dir s -let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") -let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq") -let coq_eq_rect = lazy (gen_constant ["Init"; "Logic"] "eq_rect") let coq_f_equal = lazy (gen_constant ["Init"; "Logic"] "f_equal") -let iff = lazy (gen_constant ["Init"; "Logic"] "iff") let coq_all = lazy (gen_constant ["Init"; "Logic"] "all") let impl = lazy (gen_constant ["Program"; "Basics"] "impl") let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow") -let coq_id = lazy (gen_constant ["Init"; "Datatypes"] "id") let reflexive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Reflexive") -let reflexive_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "reflexivity") let reflexive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "reflexivity") let symmetric_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Symmetric") let symmetric_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "symmetry") -let symmetric_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "symmetry") let transitive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Transitive") let transitive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "transitivity") -let transitive_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "transitivity") let coq_inverse = lazy (gen_constant (* ["Classes"; "RelationClasses"] "inverse" *) ["Program"; "Basics"] "flip") @@ -100,18 +92,14 @@ let coq_inverse = lazy (gen_constant (* ["Classes"; "RelationClasses"] "inverse" let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |]) (* let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; new_Type (); rel |]) *) -let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement") let forall_relation = lazy (gen_constant ["Classes"; "Morphisms"] "forall_relation") let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation") -let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep") let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") -let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence") let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation") let subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "subrelation") -let is_subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "is_subrelation") let do_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "do_subrelation") let apply_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "apply_subrelation") @@ -119,25 +107,13 @@ let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "rela let mk_relation a = mkApp (Lazy.force coq_relation, [| a |]) (* let mk_relation a = mkProd (Anonymous, a, mkProd (Anonymous, a, new_Type ())) *) -let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT") - -let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive") - -let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv") -let setoid_proper = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_proper") -let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive") - let rewrite_relation_class = lazy (gen_constant ["Classes"; "RelationClasses"] "RewriteRelation") -let rewrite_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "rewrite_relation") let arrow_morphism a b = if isprop a && isprop b then Lazy.force impl else Lazy.force arrow -let setoid_refl pars x = - applistc (Lazy.force setoid_refl_proj) (pars @ [x]) - let proper_type = lazy (constr_of_global (Lazy.force proper_class).cl_impl) let proper_proxy_type = lazy (constr_of_global (Lazy.force proper_proxy_class).cl_impl) @@ -165,10 +141,6 @@ let split_head = function hd :: tl -> hd, tl | [] -> assert(false) -let new_goal_evar (goal,cstr) env t = - let goal', t = Evarutil.new_evar goal env t in - (goal', cstr), t - let new_cstr_evar (goal,cstr) env t = let cstr', t = Evarutil.new_evar cstr env t in (goal, cstr'), t @@ -311,15 +283,6 @@ let rewrite2_unif_flags = { Unification.modulo_eta = true } -let setoid_rewrite_unif_flags = { - Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; - Unification.use_metas_eagerly = true; - Unification.modulo_delta = conv_transparent_state; - Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; - Unification.modulo_eta = true -} - let convertible env evd x y = Reductionops.is_conv env evd x y @@ -385,11 +348,6 @@ let unfold_impl t = mkProd (Anonymous, a, lift 1 b) | _ -> assert false -let unfold_id t = - match kind_of_term t with - | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_id) *) -> b - | _ -> assert false - let unfold_all t = match kind_of_term t with | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) -> @@ -398,9 +356,6 @@ let unfold_all t = | _ -> assert false) | _ -> assert false -let decomp_prod env evm n c = - snd (Reductionops.splay_prod_n env evm n c) - let rec decomp_pointwise n c = if n = 0 then c else @@ -1099,11 +1054,8 @@ let occurrences_of = function error "Illegal negative occurrence number."; (true,nl) -let pr_gen_strategy pr_id = Pp.mt () -let pr_loc_strategy _ _ _ = Pp.mt () let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" -let intern_strategy ist gl c = c let interp_strategy ist gl c = c let glob_strategy ist l = l let subst_strategy evm l = l @@ -1119,7 +1071,7 @@ let interp_constr_list env sigma = open Pcoq -let (wit_strategy, globwit_strategy, rawwit_strategy) = +let _ = (Genarg.create_arg "strategy" : ((strategy, Genarg.tlevel) Genarg.abstract_argument_type * (strategy, Genarg.glevel) Genarg.abstract_argument_type * @@ -1216,10 +1168,6 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance binders instance fields = new_instance binders instance (CRecord (dummy_loc,None,fields)) ~generalize:false None -let require_library dirpath = - let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in - Library.require_library [qualid] (Some false) - let declare_instance_refl binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance binders instance @@ -1235,8 +1183,6 @@ let declare_instance_trans binders a aeq n lemma = in anew_instance binders instance [(Ident (dummy_loc,id_of_string "transitivity"),lemma)] -let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None))) - let declare_relation ?(binders=[]) a aeq n refl symm trans = init_setoid (); let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" @@ -1281,10 +1227,11 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type -let (wit_binders : Genarg.tlevel binders_argtype), - (globwit_binders : Genarg.glevel binders_argtype), - (rawwit_binders : Genarg.rlevel binders_argtype) = - Genarg.create_arg "binders" +let _, _, rawwit_binders = + (Genarg.create_arg "binders" : + Genarg.tlevel binders_argtype * + Genarg.glevel binders_argtype * + Genarg.rlevel binders_argtype) open Pcoq.Constr @@ -1355,9 +1302,6 @@ VERNAC COMMAND EXTEND AddParametricRelation3 [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] END -let mk_qualid s = - Libnames.Qualid (dummy_loc, Libnames.qualid_of_string s) - let cHole = CHole (dummy_loc, None) open Entries @@ -1599,15 +1543,6 @@ let general_s_rewrite_clause x = let _ = Equality.register_general_rewrite_clause general_s_rewrite_clause -let is_loaded d = - let d' = List.map id_of_string d in - let dir = make_dirpath (List.rev d') in - Library.library_is_loaded dir - -let try_loaded f gl = - if is_loaded ["Coq";"Classes";"RelationClasses"] then f gl - else tclFAIL 0 (str"You need to require Coq.Classes.RelationClasses first") gl - (** [setoid_]{reflexivity,symmetry,transitivity} tactics *) let not_declared env ty rel = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f067141a8..a2caec7c5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -65,11 +65,6 @@ let skip_metaid = function | AI x -> x | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc -type ltac_type = - | LtacFun of ltac_type - | LtacBasic - | LtacTactic - (* Values for interpretation *) type value = | VRTactic of (goal list sigma) (* For Match results *) @@ -160,22 +155,6 @@ let valueOut = function (* To embed constr *) let constrIn t = CDynamic (dummy_loc,constr_in t) -let constrOut = function - | CDynamic (_,d) -> - if (Dyn.tag d) = "constr" then - constr_out d - else - anomalylabstrm "constrOut" (str "Dynamic tag should be constr") - | ast -> - anomalylabstrm "constrOut" (str "Not a Dynamic ast") - -(* Globalizes the identifier *) -let find_reference env qid = - (* We first look for a variable of the current proof *) - match repr_qualid qid with - | (d,id) when repr_dirpath d = [] & List.mem id (ids_of_context env) - -> VarRef id - | _ -> Nametab.locate qid (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) let atomic_mactab = ref Idmap.empty @@ -346,10 +325,6 @@ let intern_name l ist = function | Anonymous -> Anonymous | Name id -> Name (intern_ident l ist id) -let vars_of_ist (lfun,_,_,env) = - List.fold_left (fun s id -> Idset.add id s) - (vars_of_env env) lfun - let strict_check = ref false let adjust_loc loc = if !strict_check then dloc else loc @@ -519,12 +494,6 @@ let intern_bindings ist = function let intern_constr_with_bindings ist (c,bl) = (intern_constr ist c, intern_bindings ist bl) -let intern_clause_pattern ist (l,occl) = - let rec check = function - | (hyp,l) :: rest -> (intern_hyp ist (skip_metaid hyp),l)::(check rest) - | [] -> [] - in (l,check occl) - (* TODO: catch ltac vars *) let intern_induction_arg ist = function | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c) @@ -994,14 +963,6 @@ and intern_genarg ist x = (***************************************************************************) (* Evaluation/interpretation *) -let constr_to_id loc = function - | VConstr ([],c) when isVar c -> destVar c - | _ -> invalid_arg_loc (loc, "Not an identifier") - -let constr_to_qid loc c = - try shortest_qualid_of_global Idset.empty (global_of_constr c) - with _ -> invalid_arg_loc (loc, "Not a global reference") - let is_variable env id = List.mem id (ids_of_named_context (Environ.named_context env)) @@ -1149,16 +1110,6 @@ let interp_hyp_list_as_list ist gl (loc,id as x) = let interp_hyp_list ist gl l = List.flatten (List.map (interp_hyp_list_as_list ist gl) l) -let interp_clause_pattern ist gl (l,occl) = - let rec check acc = function - | (hyp,l) :: rest -> - let hyp = interp_hyp ist gl hyp in - if List.mem hyp acc then - error ("Hypothesis "^(string_of_id hyp)^" occurs twice."); - (hyp,l)::(check (hyp::acc) rest) - | [] -> [] - in (l,check [] occl) - let interp_move_location ist gl = function | MoveAfter id -> MoveAfter (interp_hyp ist gl id) | MoveBefore id -> MoveBefore (interp_hyp ist gl id) @@ -1396,8 +1347,6 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let interp_constr_list ist env sigma c = snd (interp_constr_in_compound_list (fun x -> x) (fun x -> x) (fun ist env sigma c -> (Evd.empty, interp_constr ist env sigma c)) ist env sigma c) -let inj_open c = (Evd.empty,c) - let interp_open_constr_list = interp_constr_in_compound_list (fun x -> x) (fun x -> x) (interp_open_constr None) @@ -2888,11 +2837,6 @@ and subst_genarg subst (x:glob_generic_argument) = (***************************************************************************) (* Tactic registration *) -(* For bad tactic calls *) -let bad_tactic_args s = - anomalylabstrm s - (str "Tactic " ++ str s ++ str " called with bad arguments") - (* Declaration of the TAC-DEFINITION object *) let add (kn,td) = mactab := Gmap.add kn td !mactab let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab) @@ -2937,7 +2881,7 @@ let subst_md (subst,(local,defs)) = let classify_md (local,defs as o) = if local then Dispose else Substitute o -let (inMD,outMD) = +let inMD = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index d0fa46c7a..1310fe7f9 100644 --- a/tactics/tactic_option.ml +++ b/tactics/tactic_option.ml @@ -25,7 +25,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name = let subst (s, (local, tac)) = (local, Tacinterp.subst_tactic s tac) in - let input, _output = + let input = declare_object { (default_object name) with cache_function = cache; diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 1108a7f2d..dc013fda6 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -171,12 +171,9 @@ let fullGoal gl = None :: List.map Option.make (pf_ids_of_hyps gl) let onAllHyps tac gl = tclMAP tac (pf_ids_of_hyps gl) gl let onAllHypsAndConcl tac gl = tclMAP tac (fullGoal gl) gl -let onAllHypsAndConclLR tac gl = tclMAP tac (List.rev (fullGoal gl)) gl let tryAllHyps tac gl = tclFIRST_PROGRESS_ON tac (pf_ids_of_hyps gl) gl let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (fullGoal gl) gl -let tryAllHypsAndConclLR tac gl = - tclFIRST_PROGRESS_ON tac (List.rev (fullGoal gl)) gl let onClause tac cl gls = tclMAP tac (simple_clause_of cl gls) gls let onClauseLR tac cl gls = tclMAP tac (List.rev (simple_clause_of cl gls)) gls diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 98904a59c..b030a09c3 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -117,7 +117,6 @@ val tryAllHypsAndConcl : (identifier option -> tactic) -> tactic val onAllHyps : (identifier -> tactic) -> tactic val onAllHypsAndConcl : (identifier option -> tactic) -> tactic -val onAllHypsAndConclLR : (identifier option -> tactic) -> tactic val onClause : (identifier option -> tactic) -> clause -> tactic val onClauseLR : (identifier option -> tactic) -> clause -> tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4a3001065..3876c6b35 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -75,21 +75,6 @@ let _ = optread = (fun () -> !dependent_propositions_elimination) ; optwrite = (fun b -> dependent_propositions_elimination := b) } -let apply_in_side_conditions_come_first = ref true - -let use_apply_in_side_conditions_come_first () = - !apply_in_side_conditions_come_first - && Flags.version_strictly_greater Flags.V8_2 - -let _ = - declare_bool_option - { optsync = true; - optname = "apply-in side-conditions coming first"; - optkey = ["Side";"Conditions";"First";"For";"apply";"in"]; - optread = (fun () -> !dependent_propositions_elimination) ; - optwrite = (fun b -> dependent_propositions_elimination := b) } - - (*********************************************) (* Tactics *) (*********************************************) @@ -163,7 +148,6 @@ let internal_cut_rev_replace = internal_cut_rev_gen true (* Moving hypotheses *) let move_hyp = Tacmach.move_hyp -let order_hyps = Tacmach.order_hyps (* Renaming hypotheses *) let rename_hyp = Tacmach.rename_hyp @@ -340,16 +324,6 @@ let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname) let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast) let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast) -(* A function which reduces accordingly to a reduction expression, - as the command Eval does. *) - -let checking_fun = function - (* Expansion is not necessarily well-typed: e.g. expansion of t into x is - not well-typed in [H:(P t); x:=t |- G] because x is defined after H *) - | Fold _ -> with_check - | Pattern _ -> with_check - | _ -> (fun x -> x) - (* The main reduction function *) let reduction_clause redexp cl = @@ -455,7 +429,6 @@ let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) no_move false false let intro = intro_gen dloc (IntroAvoid []) no_move false false let introf = intro_gen dloc (IntroAvoid []) no_move true false let intro_avoiding l = intro_gen dloc (IntroAvoid l) no_move false false -let introf_move_name destopt = intro_gen dloc (IntroAvoid []) destopt true false (**** Multiple introduction tactics ****) @@ -2164,23 +2137,6 @@ let make_up_names n ind_opt cname = else avoid in id_of_string base, hyprecname, avoid -let is_indhyp p n t = - let l, c = decompose_prod t in - let c,_ = decompose_app c in - let p = p + List.length l in - match kind_of_term c with - | Rel k when p < k & k <= p + n -> true - | _ -> false - -let chop_context n l = - let rec chop_aux acc = function - | n, (_,Some _,_ as h :: t) -> chop_aux (h::acc) (n, t) - | 0, l2 -> (List.rev acc, l2) - | n, (h::t) -> chop_aux (h::acc) (n-1, t) - | _, [] -> anomaly "chop_context" - in - chop_aux [] (n,l) - let error_ind_scheme s = let s = if s <> "" then s^" " else s in error ("Cannot recognize "^s^"an induction scheme.") @@ -2213,8 +2169,6 @@ let lift_togethern n l = l ([], n) in l' -let lift_together l = lift_togethern 0 l - let lift_list l = List.map (lift 1) l let ids_of_constr ?(all=false) vars c = @@ -2277,17 +2231,6 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls = let appeqs = mkApp (instc, Array.of_list refls) in (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) mkApp (appeqs, abshypt) - -let deps_of_var id env = - Environ.fold_named_context - (fun _ (n,b,t) (acc : Idset.t) -> - if Option.cata (occur_var env id) false b || occur_var env id t then - Idset.add n acc - else acc) - env ~init:Idset.empty - -let idset_of_list = - List.fold_left (fun s x -> Idset.add x s) Idset.empty let hyps_of_vars env sign nogen hyps = if Idset.is_empty hyps then [] @@ -2491,33 +2434,6 @@ let occur_rel n c = let res = not (noccurn n c) in res -let list_filter_firsts f l = - let rec list_filter_firsts_aux f acc l = - match l with - | e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l' - | _ -> acc,l - in - list_filter_firsts_aux f [] l - -let count_rels_from n c = - let rels = free_rels c in - let cpt,rg = ref 0, ref n in - while Intset.mem !rg rels do - cpt:= !cpt+1; rg:= !rg+1; - done; - !cpt - -let count_nonfree_rels_from n c = - let rels = free_rels c in - if Intset.exists (fun x -> x >= n) rels then - let cpt,rg = ref 0, ref n in - while not (Intset.mem !rg rels) do - cpt:= !cpt+1; rg:= !rg+1; - done; - !cpt - else raise Not_found - - (* cuts a list in two parts, first of size n. Size must be greater than n *) let cut_list n l = let rec cut_list_aux acc n l = @@ -3023,14 +2939,6 @@ let induction_without_atomization isrec with_evars elim names lid gl = then error "Not the right number of induction arguments." else induction_from_context_l with_evars elim_info lid names gl -let enforce_eq_name id gl = function - | (b,(loc,IntroAnonymous)) -> - (b,(loc,IntroIdentifier (fresh_id [id] (add_prefix "Heq" id) gl))) - | (b,(loc,IntroFresh heq_base)) -> - (b,(loc,IntroIdentifier (fresh_id [id] heq_base gl))) - | x -> - x - let has_selected_occurrences = function | None -> false | Some cls -> diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index ea9906d8d..b493d989b 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -266,8 +266,6 @@ let t_reduction_not = tacticIn reduction_not let intuition_gen tac = interp (tacticIn (tauto_intuit t_reduction_not tac)) -let simplif_gen = interp (tacticIn simplif) - let tauto_intuitionistic g = try intuition_gen <:tactic<fail>> g with diff --git a/toplevel/classes.ml b/toplevel/classes.ml index c06fbfc68..821fc0fad 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -65,13 +65,6 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m type binder_list = (identifier located * bool * constr_expr) list -(* Calls to interpretation functions. *) - -let interp_type_evars evdref env ?(impls=empty_internalization_env) typ = - let typ' = intern_gen true ~impls !evdref env typ in - let imps = Implicit_quantifiers.implicits_of_rawterm typ' in - imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' - (* Declare everything in the parameters as implicit, and the class instance as well *) open Topconstr @@ -281,14 +274,6 @@ let named_of_rel_context l = l ([], []) in ctx -let push_named_context = List.fold_right push_named - -let rec list_filter_map f = function - | [] -> [] - | hd :: tl -> match f hd with - | None -> list_filter_map f tl - | Some x -> x :: list_filter_map f tl - let context ?(hook=fun _ -> ()) l = let env = Global.env() in let evars = ref Evd.empty in diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index c4b775912..8df17350c 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -173,9 +173,6 @@ let rec attribute_of_vernac_command = function | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand] | VernacExtend _ -> [] -let is_vernac_goal_starting_command com = - List.mem GoalStartingCommand (attribute_of_vernac_command com) - let is_vernac_navigation_command com = List.mem NavigationCommand (attribute_of_vernac_command com) diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 3440f9fe8..daa93a7e6 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -51,7 +51,7 @@ let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> (Lib.discharge_inductive ind,Lib.discharge_con const)) l) -let (inScheme,_) = +let inScheme = declare_object {(default_object "SCHEME") with cache_function = cache_scheme; load_function = (fun _ -> cache_scheme); diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index 41680036c..c182fb385 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -71,7 +71,7 @@ let subst a b = Profile.profile2 subst_key TypeDnet.subst a b let load_key = Profile.declare_profile "load" let load a = Profile.profile1 load_key load a *) -let (input,output) = +let input = declare_object { (default_object "LIBTYPES") with load_function = (fun _ -> load); diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index efaf7707c..f0cfd5fd9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -32,7 +32,7 @@ open Nameops let cache_token (_,s) = add_keyword s -let (inToken, outToken) = +let inToken = declare_object {(default_object "TOKEN") with open_function = (fun i o -> if i=1 then cache_token o); cache_function = cache_token; @@ -70,7 +70,7 @@ let subst_tactic_parule subst (key,n,p,(d,tac)) = let subst_tactic_notation (subst,(pa,pp)) = (subst_tactic_parule subst pa,pp) -let (inTacticGrammar, outTacticGrammar) = +let inTacticGrammar = declare_object {(default_object "TacticGrammar") with open_function = (fun i o -> if i=1 then cache_tactic_notation o); cache_function = cache_tactic_notation; @@ -363,11 +363,6 @@ let error_not_same_scope x y = error ("Variables "^string_of_id x^" and "^string_of_id y^ " must be in the same scope.") -let error_both_bound_and_binding x y = - errorlabstrm "" (strbrk "The recursive variables " ++ pr_id x ++ - strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder \ - for both terms and binders.") - (**********************************************************************) (* Build pretty-printing rules *) @@ -403,12 +398,6 @@ let is_right_bracket s = let l = String.length s in l <> 0 & (s.[l-1] = '}' or s.[l-1] = ']' or s.[l-1] = ')') -let is_left_bracket_on_left s = - let l = String.length s in l <> 0 & s.[l-1] = '>' - -let is_right_bracket_on_right s = - let l = String.length s in l <> 0 & s.[0] = '<' - let is_comma s = let l = String.length s in l <> 0 & (s.[0] = ',' or s.[0] = ';') @@ -726,7 +715,7 @@ let subst_syntax_extension (subst,(local,sy)) = let classify_syntax_definition (local,_ as o) = if local then Dispose else Substitute o -let (inSyntaxExtension, outSyntaxExtension) = +let inSyntaxExtension = declare_object {(default_object "SYNTAX-EXTENSION") with open_function = (fun i o -> if i=1 then cache_syntax_extension o); cache_function = cache_syntax_extension; @@ -976,7 +965,7 @@ let subst_notation (subst,(lc,scope,pat,b,ndf)) = let classify_notation (local,_,_,_,_ as o) = if local then Dispose else Substitute o -let (inNotation, outNotation) = +let inNotation = declare_object {(default_object "NOTATION") with open_function = open_notation; cache_function = cache_notation; @@ -1152,7 +1141,7 @@ let subst_scope_command (subst,(scope,o as x)) = match o with scope, ScopeClasses cl' | _ -> x -let (inScopeCommand,outScopeCommand) = +let inScopeCommand = declare_object {(default_object "DELIMITERS") with cache_function = cache_scope_command; open_function = open_scope_command; diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index ccb6c4774..429d39e20 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -217,8 +217,6 @@ let file_of_name name = coqtop could always load plugins, we prefer to have uniformity between bytecode and native versions. *) -let stdlib_use_plugins = Coq_config.has_natdynlink - (* [known_loaded_module] contains the names of the loaded ML modules * (linked or loaded with load_object). It is used not to load a * module twice. It is NOT the list of ML modules Coq knows. *) @@ -298,7 +296,7 @@ let cache_ml_module_object (_,{mnames=mnames}) = let classify_ml_module_object ({mlocal=mlocal} as o) = if mlocal then Dispose else Substitute o -let (inMLModule,outMLModule) = +let inMLModule = declare_object {(default_object "ML-MODULE") with load_function = (fun _ -> cache_ml_module_object); cache_function = cache_ml_module_object; diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index f624d40a7..c625854ea 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -61,8 +61,6 @@ type ml_module_object = { mlocal: Vernacexpr.locality_flag; mnames: string list; } -val inMLModule : ml_module_object -> Libobject.obj -val outMLModule : Libobject.obj -> ml_module_object val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 0dd18f064..1ef51496b 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -277,9 +277,6 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map pi1 ctx))) -let qualid_of_con c = - Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) - let declare_instance_cst glob con = let instance = Typeops.type_of_constant (Global.env ()) con in let _, r = decompose_prod_assum instance in diff --git a/toplevel/search.ml b/toplevel/search.ml index abb0af108..e01978dc1 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -93,10 +93,6 @@ let rec head c = | LetIn (_,_,_,c) -> head c | _ -> c -let constr_to_full_path c = match kind_of_term c with - | Const sp -> sp - | _ -> raise No_full_path - let xor a b = (a or b) & (not (a & b)) let plain_display ref a c = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index eae675177..b7524eea0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -20,7 +20,6 @@ open Tacmach open Constrintern open Prettyp open Printer -open Tactic_printer open Tacinterp open Command open Goptions @@ -1161,16 +1160,6 @@ let vernac_locate = function (********************) (* Proof management *) -let vernac_goal = function - | None -> () - | Some c -> - if not (refining()) then begin - let unnamed_kind = Lemma (* Arbitrary *) in - start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->()); - print_subgoals () - end else - error "repeated Goal not permitted in refining mode." - let vernac_abort = function | None -> delete_current_proof (); diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index cdf72bb1e..224d9765f 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -372,9 +372,6 @@ let locality_flag = ref None let local_of_bool = function true -> Local | false -> Global -let is_true = function Some (_,b) -> b | _ -> false -let is_false = function Some (_,b) -> not b | _ -> false - let check_locality () = match !locality_flag with | Some (loc,true) -> diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 878b0fdf8..10c5a00f6 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -64,7 +64,3 @@ let call (opn,converted_args) = if !Flags.debug then msgnl (str"Vernac Interpreter " ++ str !loc); raise e - -let bad_vernac_args s = - anomalylabstrm s - (str"Vernac " ++ str s ++ str" called with bad arguments") |