diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 884 |
1 files changed, 666 insertions, 218 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index a8e0133e..531eadb3 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 10067 2007-08-09 17:13:16Z msozeau $ *) +(* $Id: command.ml 11169 2008-06-24 14:37:18Z notin $ *) open Pp open Util -open Options +open Flags open Term open Termops open Declarations @@ -42,22 +42,26 @@ open Pretyping open Evarutil open Evarconv open Notation +open Goptions +open Mod_subst +open Evd +open Decls -let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) -let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) +let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b)) +let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b)) let rec abstract_constr_expr c = function | [] -> c | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl + | LocalRawAssum (idl,k,t)::bl -> + List.fold_right (fun x b -> mkLambdaC([x],k,t,b)) idl (abstract_constr_expr c bl) let rec generalize_constr_expr c = function | [] -> c | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkProdC([x],t,b)) idl + | LocalRawAssum (idl,k,t)::bl -> + List.fold_right (fun x b -> mkProdC([x],k,t,b)) idl (generalize_constr_expr c bl) let rec under_binders env f n c = @@ -80,7 +84,7 @@ let rec destSubCast c = match kind_of_term c with let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) - | CHole loc -> + | CHole (loc, k) -> let (has_no_args,name,params) = a in if not has_no_args then user_err_loc (loc,"", @@ -98,13 +102,13 @@ let definition_message id = if_verbose message ((string_of_id id) ^ " is defined") let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = - let sigma = Evd.empty in let env = Global.env() in - match comtypopt with + match comtypopt with None -> let b = abstract_constr_expr com bl in - let j = interp_constr_judgment sigma env b in - { const_entry_body = j.uj_val; + let b, imps = interp_constr_evars_impls env b in + imps, + { const_entry_body = b; const_entry_type = None; const_entry_opaque = opacity; const_entry_boxed = boxed } @@ -112,7 +116,9 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = (* We use a cast to avoid troubles with evars in comtyp *) (* that can only be resolved knowing com *) let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in - let (body,typ) = destSubCast (interp_constr sigma env b) in + let b, imps = interp_constr_evars_impls env b in + let (body,typ) = destSubCast b in + imps, { const_entry_body = body; const_entry_type = Some typ; const_entry_opaque = opacity; @@ -127,16 +133,23 @@ let red_constant_entry bl ce = function (local_binders_length bl) body } -let declare_global_definition ident ce local = +let declare_global_definition ident ce local imps = let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in - if local = Local && Options.is_verbose() then - msg_warning (pr_id ident ++ str" is declared as a global definition"); - definition_message ident; - ConstRef kn + let gr = ConstRef kn in + maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + if local = Local && Flags.is_verbose() then + msg_warning (pr_id ident ++ str" is declared as a global definition"); + definition_message ident; + gr + +let declare_definition_hook = ref ignore +let set_declare_definition_hook = (:=) declare_definition_hook +let get_declare_definition_hook () = !declare_definition_hook let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = - let ce = constant_entry_of_com (bl,c,typopt,false,boxed) in + let imps, ce = constant_entry_of_com (bl,c,typopt,false,boxed) in let ce' = red_constant_entry bl ce red_option in + !declare_definition_hook ce'; let r = match local with | Local when Lib.sections_are_opened () -> let c = @@ -144,28 +157,29 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in definition_message ident; if Pfedit.refining () then - msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ - str" is not visible from current goals"); + Flags.if_verbose msg_warning + (str"Local definition " ++ pr_id ident ++ + str" is not visible from current goals"); VarRef ident | (Global|Local) -> - declare_global_definition ident ce' local in + declare_global_definition ident ce' local imps in hook local r -let syntax_definition ident c local onlyparse = - let c = snd (interp_aconstr [] [] c) in - Syntax_def.declare_syntactic_definition local ident onlyparse c +let syntax_definition ident (vars,c) local onlyparse = + let pat = interp_aconstr [] vars c in + Syntax_def.declare_syntactic_definition local ident onlyparse pat (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) let assumption_message id = if_verbose message ((string_of_id id) ^ " is assumed") -let declare_one_assumption is_coe (local,kind) c (_,ident) = +let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = declare_variable ident - (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in + (Lib.cwd(), SectionLocalAssum (c,impl,keep), IsAssumption kind) in assumption_message ident; if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ @@ -173,19 +187,26 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) = VarRef ident | (Global|Local) -> let kn = - declare_constant ident (ParameterEntry c, IsAssumption kind) in + declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in + let gr = ConstRef kn in + maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; assumption_message ident; - if local=Local & Options.is_verbose () then + if local=Local & Flags.is_verbose () then msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); - ConstRef kn in + gr in if is_coe then Class.try_add_new_coercion r local -let declare_assumption idl is_coe k bl c = +let declare_assumption_hook = ref ignore +let set_declare_assumption_hook = (:=) declare_assumption_hook + +let declare_assumption idl is_coe k bl c impl keep nl = if not (Pfedit.refining ()) then let c = generalize_constr_expr c bl in - let c = interp_type Evd.empty (Global.env()) c in - List.iter (declare_one_assumption is_coe k c) idl + let env = Global.env () in + let c', imps = interp_type_evars_impls env c in + !declare_assumption_hook c'; + List.iter (declare_one_assumption is_coe k c' imps impl keep nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") @@ -193,6 +214,8 @@ let declare_assumption idl is_coe k bl c = (* 3a| Elimination schemes for mutual inductive definitions *) open Indrec +open Inductiveops + let non_type_eliminations = [ (InProp,elimination_suffix InProp); @@ -208,7 +231,7 @@ let declare_one_elimination ind = { const_entry_body = c; const_entry_type = t; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() }, + const_entry_boxed = Flags.boxed_definitions() }, Decl_kinds.IsDefinition Definition) in definition_message id; kn @@ -248,27 +271,189 @@ let declare_one_elimination ind = let _ = declare (mindstr^suff) elim None in ()) non_type_eliminations +(* bool eq declaration flag && eq dec declaration flag *) +let eq_flag = ref false +let _ = + declare_bool_option + { optsync = true; + optname = "automatic declaration of boolean equality"; + optkey = (SecondaryTable ("Equality","Scheme")); + optread = (fun () -> !eq_flag) ; + optwrite = (fun b -> eq_flag := b) } + +(* boolean equality *) +let (inScheme,outScheme) = + declare_object {(default_object "EQSCHEME") with + cache_function = Ind_tables.cache_scheme; + load_function = (fun _ -> Ind_tables.cache_scheme); + subst_function = Auto_ind_decl.subst_in_constr; + export_function = Ind_tables.export_scheme } + +let declare_eq_scheme sp = + let mib = Global.lookup_mind sp in + let nb_ind = Array.length mib.mind_packets in + let eq_array = Auto_ind_decl.make_eq_scheme sp in + try + for i=0 to (nb_ind-1) do + let cpack = Array.get mib.mind_packets i in + let nam = id_of_string ((string_of_id cpack.mind_typename)^"_beq") + in + let cst_entry = {const_entry_body = eq_array.(i); + const_entry_type = None; + const_entry_opaque = false; + const_entry_boxed = Flags.boxed_definitions() } + in + let cst_decl = (DefinitionEntry cst_entry),(IsDefinition Definition) + in + let cst = Declare.declare_constant nam cst_decl in + Lib.add_anonymous_leaf (inScheme ((sp,i),mkConst cst)); + definition_message nam + done + with Not_found -> + error "Your type contains Parameters without a boolean equality" + +(* decidability of eq *) + + +let (inBoolLeib,outBoolLeib) = + declare_object {(default_object "BOOLLIEB") with + cache_function = Ind_tables.cache_bl; + load_function = (fun _ -> Ind_tables.cache_bl); + subst_function = Auto_ind_decl.subst_in_constr; + export_function = Ind_tables.export_bool_leib } + +let (inLeibBool,outLeibBool) = + declare_object {(default_object "LIEBBOOL") with + cache_function = Ind_tables.cache_lb; + load_function = (fun _ -> Ind_tables.cache_lb); + subst_function = Auto_ind_decl.subst_in_constr; + export_function = Ind_tables.export_leib_bool } + +let (inDec,outDec) = + declare_object {(default_object "EQDEC") with + cache_function = Ind_tables.cache_dec; + load_function = (fun _ -> Ind_tables.cache_dec); + subst_function = Auto_ind_decl.subst_in_constr; + export_function = Ind_tables.export_dec_proof } + +let start_hook = ref ignore +let set_start_hook = (:=) start_hook + +let start_proof id kind c ?init_tac hook = + let sign = Global.named_context () in + let sign = clear_proofs sign in + !start_hook c; + Pfedit.start_proof id kind sign c ?init_tac:init_tac hook + +let save id const (locality,kind) hook = + let {const_entry_body = pft; + const_entry_type = tpo; + const_entry_opaque = opacity } = const in + let k = logical_kind_of_goal_kind kind in + let l,r = match locality with + | Local when Lib.sections_are_opened () -> + let c = SectionLocalDef (pft, tpo, opacity) in + let _ = declare_variable id (Lib.cwd(), c, k) in + (Local, VarRef id) + | Local | Global -> + let kn = declare_constant id (DefinitionEntry const, k) in + (Global, ConstRef kn) in + Pfedit.delete_current_proof (); + definition_message id; + hook l r + +let save_hook = ref ignore +let set_save_hook f = save_hook := f + +let save_named opacity = + let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in + let const = { const with const_entry_opaque = opacity } in + save id const persistence hook + +let make_eq_decidability ind = + (* fetching data *) + let mib = Global.lookup_mind (fst ind) in + let nparams = mib.mind_nparams in + let nparrec = mib.mind_nparams_rec in + let lnonparrec,lnamesparrec = + context_chop (nparams-nparrec) mib.mind_params_ctxt in + let proof_name = (string_of_id( + Array.get mib.mind_packets (snd ind)).mind_typename)^"_eq_dec" in + let bl_name =(string_of_id( + Array.get mib.mind_packets (snd ind)).mind_typename)^"_dec_bl" in + let lb_name =(string_of_id( + Array.get mib.mind_packets (snd ind)).mind_typename)^"_dec_lb" in + (* main calls*) + if Ind_tables.check_bl_proof ind + then (message (bl_name^" is already declared.")) + else ( + start_proof (id_of_string bl_name) + (Global,Proof Theorem) + (Auto_ind_decl.compute_bl_goal ind lnamesparrec nparrec) + (fun _ _ -> ()); + Auto_ind_decl.compute_bl_tact ind lnamesparrec nparrec; + save_named true; + Lib.add_anonymous_leaf + (inBoolLeib (ind,mkConst (Lib.make_con (id_of_string bl_name)))) +(* definition_message (id_of_string bl_name) *) + ); + if Ind_tables.check_lb_proof ind + then (message (lb_name^" is already declared.")) + else ( + start_proof (id_of_string lb_name) + (Global,Proof Theorem) + (Auto_ind_decl.compute_lb_goal ind lnamesparrec nparrec) + ( fun _ _ -> ()); + Auto_ind_decl.compute_lb_tact ind lnamesparrec nparrec; + save_named true; + Lib.add_anonymous_leaf + (inLeibBool (ind,mkConst (Lib.make_con (id_of_string lb_name)))) +(* definition_message (id_of_string lb_name) *) + ); + if Ind_tables.check_dec_proof ind + then (message (proof_name^" is already declared.")) + else ( + start_proof (id_of_string proof_name) + (Global,Proof Theorem) + (Auto_ind_decl.compute_dec_goal ind lnamesparrec nparrec) + ( fun _ _ -> ()); + Auto_ind_decl.compute_dec_tact ind lnamesparrec nparrec; + save_named true; + Lib.add_anonymous_leaf + (inDec (ind,mkConst (Lib.make_con (id_of_string proof_name)))) +(* definition_message (id_of_string proof_name) *) + ) + +(* end of automated definition on ind*) + let declare_eliminations sp = let mib = Global.lookup_mind sp in - if mib.mind_finite then + if mib.mind_finite then begin + if (!eq_flag) then (declare_eq_scheme sp); for i = 0 to Array.length mib.mind_packets - 1 do - declare_one_elimination (sp,i) - done + declare_one_elimination (sp,i); + try + if (!eq_flag) then (make_eq_decidability (sp,i)) + with _ -> + Pfedit.delete_current_proof(); + message "Error while computing decidability scheme. Please report." + done; + end (* 3b| Mutual inductive definitions *) -let compute_interning_datas env l nal typl = - let mk_interning_data na typ = +let compute_interning_datas env l nal typl impll = + let mk_interning_data na typ impls = let idl, impl = - if is_implicit_args() then - let impl = compute_implicits env typ in - let sub_impl,_ = list_chop (List.length l) impl in - let sub_impl' = List.filter is_status_implicit sub_impl in + let impl = + compute_implicits_with_manual env typ (is_implicit_args ()) impls + in + let sub_impl,_ = list_chop (List.length l) impl in + let sub_impl' = List.filter is_status_implicit sub_impl in (List.map name_of_implicit sub_impl', impl) - else - ([],[]) in - (na, (idl, impl, compute_arguments_scope typ)) in - (l, List.map2 mk_interning_data nal typl) + in + (na, (idl, impl, compute_arguments_scope typ)) in + (l, list_map3 mk_interning_data nal typl impll) let declare_interning_data (_,impls) (df,c,scope) = silently (Metasyntax.add_notation_interpretation df impls c) scope @@ -294,34 +479,39 @@ let minductive_message = function spc () ++ str "are defined") let check_all_names_different indl = - let get_names ind = ind.ind_name::List.map fst ind.ind_lc in - if not (list_distinct (List.flatten (List.map get_names indl))) then - error "Two inductive objects have the same name" - -let mk_mltype_data isevars env assums arity indname = - let is_ml_type = is_sort env (Evd.evars_of !isevars) arity in + let ind_names = List.map (fun ind -> ind.ind_name) indl in + let cstr_names = list_map_append (fun ind -> List.map fst ind.ind_lc) indl in + let l = list_duplicates ind_names in + if l <> [] then raise (InductiveError (SameNamesTypes (List.hd l))); + let l = list_duplicates cstr_names in + if l <> [] then raise (InductiveError (SameNamesConstructors (List.hd l))); + let l = list_intersect ind_names cstr_names in + if l <> [] then raise (InductiveError (SameNamesOverlap l)) + +let mk_mltype_data evdref env assums arity indname = + let is_ml_type = is_sort env (evars_of !evdref) arity in (is_ml_type,indname,assums) let prepare_param = function | (na,None,t) -> out_name na, LocalAssum t | (na,Some b,_) -> out_name na, LocalDef b -let interp_ind_arity isevars env ind = - interp_type_evars isevars env ind.ind_arity +let interp_ind_arity evdref env ind = + interp_type_evars evdref env ind.ind_arity -let interp_cstrs isevars env impls mldata arity ind = +let interp_cstrs evdref env impls mldata arity ind = let cnames,ctyps = List.split ind.ind_lc in (* Complete conclusions of constructor types if given in ML-style syntax *) let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in (* Interpret the constructor types *) - let ctyps'' = List.map (interp_type_evars isevars env ~impls) ctyps' in - (cnames, ctyps'') + let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls ~evdref env ~impls) ctyps') in + (cnames, ctyps'', cimpls) let interp_mutual paramsl indl notations finite = check_all_names_different indl; let env0 = Global.env() in - let isevars = ref (Evd.create_evar_defs Evd.empty) in - let env_params, ctx_params = interp_context_evars isevars env0 paramsl in + let evdref = ref (Evd.create_evar_defs Evd.empty) in + let (env_params, ctx_params), userimpls = interp_context_evars evdref env0 paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in (* Names of parameters as arguments of the inductive type (defs removed) *) @@ -329,37 +519,38 @@ let interp_mutual paramsl indl notations finite = let params = List.map (fun (na,_,_) -> out_name na) assums in (* Interpret the arities *) - let arities = List.map (interp_ind_arity isevars env_params) indl in + let arities = List.map (interp_ind_arity evdref env_params) indl in let fullarities = List.map (fun c -> it_mkProd_or_LetIn c ctx_params) arities in let env_ar = push_types env0 indnames fullarities in let env_ar_params = push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) - let impls = compute_interning_datas env0 params indnames fullarities in - let mldatas = List.map2 (mk_mltype_data isevars env_params params) arities indnames in + let indimpls = List.map (fun _ -> userimpls) fullarities in + let impls = compute_interning_datas env0 params indnames fullarities indimpls in + let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = States.with_heavy_rollback (fun () -> (* Temporary declaration of notations and scopes *) List.iter (declare_interning_data impls) notations; (* Interpret the constructor types *) - list_map3 (interp_cstrs isevars env_ar_params impls) mldatas arities indl) + list_map3 (interp_cstrs evdref env_ar_params impls) mldatas arities indl) () in (* Instantiate evars and check all are resolved *) - let isevars,_ = consider_remaining_unif_problems env_params !isevars in - let sigma = Evd.evars_of isevars in - let constructors = List.map (fun (idl,cl) -> (idl,List.map (nf_evar sigma) cl)) constructors in + let evd,_ = consider_remaining_unif_problems env_params !evdref in + let sigma = evars_of evd in + let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in let arities = List.map (nf_evar sigma) arities in - List.iter (check_evars env_params Evd.empty isevars) arities; - Sign.iter_rel_context (check_evars env0 Evd.empty isevars) ctx_params; - List.iter (fun (_,ctyps) -> - List.iter (check_evars env_ar_params Evd.empty isevars) ctyps) + List.iter (check_evars env_params Evd.empty evd) arities; + Sign.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; + List.iter (fun (_,ctyps,_) -> + List.iter (check_evars env_ar_params Evd.empty evd) ctyps) constructors; (* Build the inductive entries *) - let entries = list_map3 (fun ind arity (cnames,ctypes) -> { + let entries = list_map3 (fun ind arity (cnames,ctypes,cimpls) -> { mind_entry_typename = ind.ind_name; mind_entry_arity = arity; mind_entry_consnames = cnames; @@ -370,15 +561,15 @@ let interp_mutual paramsl indl notations finite = { mind_entry_params = List.map prepare_param ctx_params; mind_entry_record = false; mind_entry_finite = finite; - mind_entry_inds = entries } + mind_entry_inds = entries }, (List.map (fun (_,_,impls) -> userimpls, impls) constructors) let eq_constr_expr c1 c2 = try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false (* Very syntactical equality *) let eq_local_binder d1 d2 = match d1,d2 with - | LocalRawAssum (nal1,c1), LocalRawAssum (nal2,c2) -> - List.length nal1 = List.length nal2 && + | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) -> + List.length nal1 = List.length nal2 && k1 = k2 && List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 && eq_constr_expr c1 c2 | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) -> @@ -410,23 +601,49 @@ let prepare_inductive ntnl indl = ind_arity = ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl in - List.fold_right option_cons ntnl [], indl + List.fold_right Option.List.cons ntnl [], indl + + +let elim_flag = ref true +let _ = + declare_bool_option + { optsync = true; + optname = "automatic declaration of eliminations"; + optkey = (SecondaryTable ("Elimination","Schemes")); + optread = (fun () -> !elim_flag) ; + optwrite = (fun b -> elim_flag := b) } + + +let lift_implicits n = + List.map (fun x -> + match fst x with + ExplByPos (k, id) -> ExplByPos (k + n, id), snd x + | _ -> x) -let declare_mutual_with_eliminations isrecord mie = +let declare_mutual_with_eliminations isrecord mie impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_,kn) = declare_mind isrecord mie in - if_verbose ppnl (minductive_message names); - declare_eliminations kn; - kn + let params = List.length mie.mind_entry_params in + let (_,kn) = declare_mind isrecord mie in + list_iter_i (fun i (indimpls, constrimpls) -> + let ind = (kn,i) in + list_iter_i + (fun j impls -> + maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) + (is_implicit_args()) (indimpls @ (lift_implicits params impls))) + constrimpls) + impls; + if_verbose ppnl (minductive_message names); + if !elim_flag then declare_eliminations kn; + kn let build_mutual l finite = let indl,ntnl = List.split l in let paramsl = extract_params indl in let coes = extract_coercions indl in let notations,indl = prepare_inductive ntnl indl in - let mie = interp_mutual paramsl indl notations finite in + let mie,impls = interp_mutual paramsl indl notations finite in (* Declare the mutual inductive block with its eliminations *) - ignore (declare_mutual_with_eliminations false mie); + ignore (declare_mutual_with_eliminations false mie impls); (* Declare the possible notations of inductive types *) List.iter (declare_interning_data ([],[])) notations; (* Declare the coercions *) @@ -434,13 +651,27 @@ let build_mutual l finite = (* 3c| Fixpoints and co-fixpoints *) -let recursive_message = function +let pr_rank = function + | 0 -> str "1st" + | 1 -> str "2nd" + | 2 -> str "3rd" + | n -> str ((string_of_int (n+1))^"th") + +let recursive_message indexes = function | [] -> anomaly "no recursive definition" - | [id] -> pr_id id ++ str " is recursively defined" + | [id] -> pr_id id ++ str " is recursively defined" ++ + (match indexes with + | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | _ -> mt ()) | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ - spc () ++ str "are recursively defined") - -let corecursive_message = function + spc () ++ str "are recursively defined" ++ + match indexes with + | Some a -> spc () ++ str "(decreasing respectively on " ++ + prlist_with_sep pr_coma pr_rank (Array.to_list a) ++ + str " arguments)" + | None -> mt ()) + +let corecursive_message _ = function | [] -> error "no corecursive definition" | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ @@ -521,7 +752,7 @@ let check_mutuality env kind fixl = | _ -> () type fixpoint_kind = - | IsFixpoint of (int option * recursion_order_expr) list + | IsFixpoint of (identifier located option * recursion_order_expr) list | IsCoFixpoint type fixpoint_expr = { @@ -531,15 +762,20 @@ type fixpoint_expr = { fix_type : constr_expr } -let interp_fix_type isevars env fix = - interp_type_evars isevars env - (generalize_constr_expr fix.fix_type fix.fix_binders) +let interp_fix_context evdref env fix = + interp_context_evars evdref env fix.fix_binders -let interp_fix_body isevars env impls fix fixtype = - interp_casted_constr_evars isevars env ~impls - (abstract_constr_expr fix.fix_body fix.fix_binders) fixtype +let interp_fix_ccl evdref (env,_) fix = + interp_type_evars evdref env fix.fix_type -let declare_fix boxed kind f def t = +let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = + let env = push_rel_context ctx env_rec in + let body = interp_casted_constr_evars evdref env ~impls fix.fix_body ccl in + it_mkLambda_or_LetIn body ctx + +let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx + +let declare_fix boxed kind f def t imps = let ce = { const_entry_body = def; const_entry_type = Some t; @@ -547,26 +783,37 @@ let declare_fix boxed kind f def t = const_entry_boxed = boxed } in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in - ConstRef kn - + let gr = ConstRef kn in + maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + gr + let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in let names = List.map (fun id -> Name id) fixnames in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) -let compute_guardness_evidence (n,_) fixl fixtype = +(* Jump over let-bindings. *) + +let rel_index n ctx = + list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx)) + +let rec unfold f b = + match f b with + | Some (x, b') -> x :: unfold f b' + | None -> [] + +let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = match n with - | Some n -> n + | Some (loc, n) -> [rel_index n fixctx] | None -> - (* Recursive argument was not given by the user : - We check that there is only one inductive argument *) - let m = local_binders_length fixl.fix_binders in - let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in - let isIndApp t = isInd (fst (decompose_app (strip_head_cast t))) in - (* This could be more precise (e.g. do some delta) *) - let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in - try (list_unique_index true lb) - 1 - with Not_found -> error "the recursive argument needs to be specified" + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let len = List.length fixctx in + unfold (function x when x = len -> None + | n -> Some (n, succ n)) 0 let interp_recursive fixkind l boxed = let env = Global.env() in @@ -575,70 +822,124 @@ let interp_recursive fixkind l boxed = let fixnames = List.map (fun fix -> fix.fix_name) fixl in (* Interp arities allowing for unresolved types *) - let isevars = ref (Evd.create_evar_defs Evd.empty) in - let fixtypes = List.map (interp_fix_type isevars env) fixl in + let evdref = ref (Evd.create_evar_defs Evd.empty) in + let fixctxs, fiximps = + List.split (List.map (interp_fix_context evdref env) fixl) in + let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in + let fixtypes = List.map2 build_fix_type fixctxs fixccls in let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_interning_datas env [] fixnames fixtypes in - let notations = List.fold_right option_cons ntnl [] in + let impls = compute_interning_datas env [] fixnames fixtypes fiximps in + let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = States.with_heavy_rollback (fun () -> List.iter (declare_interning_data impls) notations; - List.map2 (interp_fix_body isevars env_rec impls) fixl fixtypes) + list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) () in (* Instantiate evars and check all are resolved *) - let isevars,_ = consider_remaining_unif_problems env_rec !isevars in - let fixdefs = List.map (nf_evar (Evd.evars_of isevars)) fixdefs in - let fixtypes = List.map (nf_evar (Evd.evars_of isevars)) fixtypes in - List.iter (check_evars env_rec Evd.empty isevars) fixdefs; - List.iter (check_evars env Evd.empty isevars) fixtypes; + let evd,_ = consider_remaining_unif_problems env_rec !evdref in + let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in + let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in + List.iter (check_evars env_rec Evd.empty evd) fixdefs; + List.iter (check_evars env Evd.empty evd) fixtypes; check_mutuality env kind (List.combine fixnames fixdefs); (* Build the fix declaration block *) let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in - let fixdecls = + let indexes, fixdecls = match fixkind with | IsFixpoint wfl -> - let fixwf = list_map3 compute_guardness_evidence wfl fixl fixtypes in - list_map_i (fun i _ -> mkFix ((Array.of_list fixwf,i),fixdecls)) 0 l + let possible_indexes = + list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in + let indexes = search_guard dummy_loc env possible_indexes fixdecls in + Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l | IsCoFixpoint -> - list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l + None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l in (* Declare the recursive definitions *) - ignore (list_map3 (declare_fix boxed kind) fixnames fixdecls fixtypes); - if_verbose ppnl (recursive_message kind fixnames); + ignore (list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps); + if_verbose ppnl (recursive_message kind indexes fixnames); (* Declare notations *) List.iter (declare_interning_data ([],[])) notations let build_recursive l b = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in - let fixl = List.map (fun ((id,_,bl,typ,def),ntn) -> + let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn)) l in interp_recursive (IsFixpoint g) fixl b let build_corecursive l b = - let fixl = List.map (fun ((id,bl,typ,def),ntn) -> + let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn)) l in interp_recursive IsCoFixpoint fixl b (* 3d| Schemes *) - -let build_scheme lnamedepindsort = +let rec split_scheme l = + let env = Global.env() in + match l with + | [] -> [],[] + | (Some id,t)::q -> let l1,l2 = split_scheme q in + ( match t with + | InductionScheme (x,y,z) -> ((id,x,y,z)::l1),l2 + | EqualityScheme x -> l1,(x::l2) + ) +(* + if no name has been provided, we build one from the types of the ind +requested +*) + | (None,t)::q -> + let l1,l2 = split_scheme q in + ( match t with + | InductionScheme (x,y,z) -> + let ind = mkInd (Nametab.inductive_of_reference y) in + let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind) +in + let z' = family_of_sort (interp_sort z) in + let suffix = ( + match sort_of_ind with + | InProp -> + if x then (match z' with + | InProp -> "_ind_nodep" + | InSet -> "_rec_nodep" + | InType -> "_rect_nodep") + else ( match z' with + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" ) + | _ -> + if x then (match z' with + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" ) + else (match z' with + | InProp -> "_ind_nodep" + | InSet -> "_rec_nodep" + | InType -> "_rect_nodep") + ) in + let newid = (string_of_id (Pcoq.coerce_global_to_id y))^suffix in + let newref = (dummy_loc,id_of_string newid) in + ((newref,x,y,z)::l1),l2 + | EqualityScheme x -> l1,(x::l2) + ) + + +let build_induction_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort and sigma = Evd.empty and env0 = Global.env() in let lrecspec = List.map (fun (_,dep,indid,sort) -> - let ind = Nametab.global_inductive indid in + let ind = Nametab.inductive_of_reference indid in let (mib,mip) = Global.lookup_inductive ind in (ind,mib,mip,dep,interp_elimination_sort sort)) lnamedepindsort @@ -650,114 +951,259 @@ let build_scheme lnamedepindsort = let ce = { const_entry_body = decl; const_entry_type = Some decltype; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() } in + const_entry_boxed = Flags.boxed_definitions() } in let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in ConstRef kn :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in - if_verbose ppnl (recursive_message Fixpoint lrecnames) - -let rec get_concl n t = - if n = 0 then t - else - match kind_of_term t with - Prod (_,_,t) -> get_concl (pred n) t - | _ -> raise (Invalid_argument "get_concl") - -let cut_last l = - let rec aux acc = function - hd :: [] -> List.rev acc, hd - | hd :: tl -> aux (hd :: acc) tl - | [] -> raise (Invalid_argument "cut_last") - in aux [] l + if_verbose ppnl (recursive_message Fixpoint None lrecnames) + +let build_scheme l = + let ischeme,escheme = split_scheme l in +(* we want 1 kind of scheme at a time so we check if the user +tried to declare different schemes at once *) + if (ischeme <> []) && (escheme <> []) + then + error "Do not declare equality and induction scheme at the same time." + else ( + if ischeme <> [] then build_induction_scheme ischeme; + List.iter ( fun indname -> + let ind = Nametab.inductive_of_reference indname + in declare_eq_scheme (fst ind); + try + make_eq_decidability ind + with _ -> + Pfedit.delete_current_proof(); + message "Error while computing decidability scheme. Please report." + ) escheme + ) +let list_split_rev_at index l = + let rec aux i acc = function + hd :: tl when i = index -> acc, tl + | hd :: tl -> aux (succ i) (hd :: acc) tl + | [] -> failwith "list_split_at: Invalid argument" + in aux 0 [] l + +let fold_left' f = function + [] -> raise (Invalid_argument "fold_right'") + | hd :: tl -> List.fold_left f hd tl + let build_combined_scheme name schemes = let env = Global.env () in - let defs = +(* let nschemes = List.length schemes in *) + let find_inductive ty = + let (ctx, arity) = decompose_prod ty in + let (_, last) = List.hd ctx in + match kind_of_term last with + | App (ind, args) -> ctx, destInd ind, Array.length args + | _ -> ctx, destInd last, 0 + in + let defs = List.map (fun x -> let refe = Ident x in let qualid = qualid_of_reference refe in - let cst = Nametab.locate_constant (snd qualid) in - qualid, cst, Typeops.type_of_constant env cst) + let cst = try + Nametab.locate_constant (snd qualid) + with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared") + in + let ty = Typeops.type_of_constant env cst in + qualid, cst, ty) schemes in let (qid, c, t) = List.hd defs in - let nargs = - let (_, arity, _) = destProd t in - nb_prod arity - in - let prods = nb_prod t - nargs in - let defs, (qid, c, t) = cut_last defs in - let (args, concl) = decompose_prod_n prods t in - let concls = List.map (fun (_, cst, t) -> cst, get_concl prods t) defs in + let ctx, ind, nargs = find_inductive t in + (* Number of clauses, including the predicates quantification *) + let prods = nb_prod t - (nargs + 1) in let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in let relargs = rel_vect 0 prods in - let concl_typ, concl_bod = - List.fold_right - (fun (cst, x) (acct, accb) -> - mkApp (coqand, [| x; acct |]), - mkApp (coqconj, [| x; acct; mkApp(mkConst cst, relargs); accb |])) - concls (concl, mkApp (mkConst c, relargs)) + let concls = List.rev_map + (fun (_, cst, t) -> + mkApp(mkConst cst, relargs), + snd (decompose_prod_n prods t)) defs in + let concl_bod, concl_typ = + fold_left' + (fun (accb, acct) (cst, x) -> + mkApp (coqconj, [| x; acct; cst; accb |]), + mkApp (coqand, [| x; acct |])) concls in - let ctx = List.map (fun (x, y) -> x, None, y) args in + let ctx, _ = + list_split_rev_at prods + (List.rev_map (fun (x, y) -> x, None, y) ctx) in let typ = it_mkProd_wo_LetIn concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in let ce = { const_entry_body = body; const_entry_type = Some typ; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() } in + const_entry_boxed = Flags.boxed_definitions() } in let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in - if_verbose ppnl (recursive_message Fixpoint [snd name]) - + if_verbose ppnl (recursive_message Fixpoint None [snd name]) (* 4| Goal declaration *) -let start_proof id kind c hook = - let sign = Global.named_context () in - let sign = clear_proofs sign in - Pfedit.start_proof id kind sign c hook - -let start_proof_com sopt kind (bl,t) hook = - let id = match sopt with - | Some id -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - errorlabstrm "start_proof" (pr_id id ++ str " already exists"); - id - | None -> - next_global_ident_away false (id_of_string "Unnamed_thm") - (Pfedit.get_all_proof_names ()) - in - let env = Global.env () in - let c = interp_type Evd.empty env (generalize_constr_expr t bl) in - let _ = Typeops.infer_type env c in - start_proof id kind c hook - -let save id const (locality,kind) hook = - let {const_entry_body = pft; - const_entry_type = tpo; - const_entry_opaque = opacity } = const in - let l,r = match locality with - | Local when Lib.sections_are_opened () -> - let k = logical_kind_of_goal_kind kind in - let c = SectionLocalDef (pft, tpo, opacity) in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Local -> - let k = logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) - | Global -> - let k = logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) in - Pfedit.delete_current_proof (); - definition_message id; - hook l r - -let save_named opacity = - let id,(const,persistence,hook) = Pfedit.cook_proof () in - let const = { const with const_entry_opaque = opacity } in - save id const persistence hook +(* 4.1| Support for mutually proved theorems *) + +let retrieve_first_recthm = function + | VarRef id -> + (pi2 (Global.lookup_named id),variable_opacity id) + | ConstRef cst -> + let {const_body=body;const_opaque=opaq} = + Global.lookup_constant cst in + (Option.map Declarations.force body,opaq) + | _ -> assert false + +let compute_proof_name = function + | Some (loc,id) -> + (* We check existence here: it's a bit late at Qed time *) + if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then + user_err_loc (loc,"",pr_id id ++ str " already exists"); + id + | None -> + next_global_ident_away false (id_of_string "Unnamed_thm") + (Pfedit.get_all_proof_names ()) + +let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) = + match body with + | None -> + (match local with + | Local -> + let impl=false and keep=false in (* copy values from Vernacentries *) + let k = IsAssumption Conjectural in + let c = SectionLocalAssum (t_i,impl,keep) in + let _ = declare_variable id (Lib.cwd(),c,k) in + (Local,VarRef id,imps) + | Global -> + let k = IsAssumption Conjectural in + let kn = declare_constant id (ParameterEntry (t_i,false), k) in + (Global,ConstRef kn,imps)) + | Some body -> + let k = logical_kind_of_goal_kind kind in + let body_i = match kind_of_term body with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | _ -> anomaly "Not a proof by induction" in + match local with + | Local -> + let c = SectionLocalDef (body_i, Some t_i, opaq) in + let _ = declare_variable id (Lib.cwd(), c, k) in + (Local,VarRef id,imps) + | Global -> + let const = + { const_entry_body = body_i; + const_entry_type = Some t_i; + const_entry_opaque = opaq; + const_entry_boxed = false (* copy of what cook_proof does *)} in + let kn = declare_constant id (DefinitionEntry const, k) in + (Global,ConstRef kn,imps) + +let look_for_mutual_statements thms = + if List.tl thms <> [] then + (* More than one statement: we look for a common inductive hyp or a *) + (* common coinductive conclusion *) + let n = List.length thms in + let inds = List.map (fun (id,(t,_) as x) -> + let (hyps,ccl) = splay_prod_assum (Global.env()) Evd.empty t in + let whnf_hyp_hds = map_rel_context_with_binders + (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c))) + hyps in + let ind_hyps = + List.filter ((<>) None) (list_map_i (fun i (_,b,t) -> + match kind_of_term t with + | Ind (kn,_ as ind) when + let mind = Global.lookup_mind kn in + mind.mind_ntypes = n & mind.mind_finite & b = None -> + Some (ind,x,i) + | _ -> + None) 1 whnf_hyp_hds) in + let ind_ccl = + let cclenv = push_rel_context hyps (Global.env()) in + let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in + match kind_of_term whnf_ccl with + | Ind (kn,_ as ind) when + let mind = Global.lookup_mind kn in + mind.mind_ntypes = n & not mind.mind_finite -> + Some (ind,x,0) + | _ -> + None in + ind_hyps,ind_ccl) thms in + let inds_hyps,ind_ccls = List.split inds in + let is_same_ind kn = function Some ((kn',_),_,_) -> kn = kn' | _ -> false in + let compare_kn ((kn,i),_,_) ((kn,i'),_,_) = i - i' in + (* Check if all conclusions are coinductive in the same type *) + let same_indccl = + match ind_ccls with + | (Some ((kn,_),_,_ as x))::rest when List.for_all (is_same_ind kn) rest + -> Some (x :: List.map Option.get rest) + | _ -> None in + (* Check if some hypotheses are inductive in the same type *) + let common_same_indhyp = + let rec find_same_ind inds = + match inds with + | []::_ -> + [] + | (Some ((kn,_),_,_) as x :: hyps_thms1)::other_thms -> + let others' = List.map (List.filter (is_same_ind kn)) other_thms in + (x,others')::find_same_ind (hyps_thms1::other_thms) + | (None::hyps_thm1)::other_thms -> + find_same_ind (hyps_thm1::other_thms) + | [] -> + assert false in + find_same_ind inds_hyps in + let common_inds,finite = + match same_indccl, common_same_indhyp with + | None, [(x,rest)] when List.for_all (fun l -> List.length l = 1) rest -> + (* One occurrence of common inductive hyps and no common coind ccls *) + Option.get x::List.map (fun x -> Option.get (List.hd x)) rest, + false + | Some indccl, [] -> + (* One occurrence of common coind ccls and no common inductive hyps *) + indccl, true + | _ -> + error + ("Cannot find a common mutual inductive premise or coinductive" ^ + " conclusion in the statements") in + let ordered_inds = List.sort compare_kn common_inds in + list_iter_i (fun i' ((kn,i),_,_) -> + if i <> i' then + error + ("Cannot find distinct (co)inductive types of the same family" ^ + "of mutual (co)inductive types")) + ordered_inds; + let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in + let rec_tac = + if finite then + match List.map (fun (id,(t,_)) -> (id,t)) thms with + | (id,_)::l -> Hiddentac.h_mutual_cofix true id l + | _ -> assert false + else + match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with + | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l + | _ -> assert false in + Some rec_tac,thms + else + None, thms + +(* 4.2| General support for goals *) + +let start_proof_com kind thms hook = + let thms = List.map (fun (sopt,(bl,t)) -> + (compute_proof_name sopt, + interp_type_evars_impls (Global.env()) (generalize_constr_expr t bl))) + thms in + let rec_tac,thms = look_for_mutual_statements thms in + match thms with + | [] -> anomaly "No proof to start" + | (id,(t,imps))::other_thms -> + let hook strength ref = + let other_thms_data = + if other_thms = [] then [] else + (* there are several theorems defined mutually *) + let body,opaq = retrieve_first_recthm ref in + list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in + let thms_data = (strength,ref,imps)::other_thms_data in + List.iter (fun (strength,ref,imps) -> + maybe_declare_manual_implicits false ref (is_implicit_args ()) imps; + hook strength ref) thms_data in + start_proof id kind t ?init_tac:rec_tac hook let check_anonymity id save_ident = if atompart_of_id id <> "Unnamed_thm" then @@ -767,13 +1213,13 @@ let check_anonymity id save_ident = *) let save_anonymous opacity save_ident = - let id,(const,persistence,hook) = Pfedit.cook_proof () in + let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; save save_ident const persistence hook let save_anonymous_with_strength kind opacity save_ident = - let id,(const,_,hook) = Pfedit.cook_proof () in + let id,(const,_,hook) = Pfedit.cook_proof !save_hook in let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) @@ -786,7 +1232,7 @@ let admit () = error "Only statements declared as conjecture can be admitted"; *) let kn = - declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in + declare_constant id (ParameterEntry (typ,false), IsAssumption Conjectural) in Pfedit.delete_current_proof (); assumption_message id; hook Global (ConstRef kn) @@ -795,3 +1241,5 @@ let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) + + |