diff options
author | 2009-07-04 13:28:38 +0200 | |
---|---|---|
committer | 2009-07-04 13:28:38 +0200 | |
commit | 3a420f4ad929e8372d32c735fd0fd89dfc0346a1 (patch) | |
tree | 943a01d103c1296dc7c07cb188af994354c4d9a3 /contrib/subtac | |
parent | 1769cbaddea77112dd6f336316d8eb9a0945a1e6 (diff) | |
parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) |
Merge commit 'upstream/8.2.pl1+dfsg'
Diffstat (limited to 'contrib/subtac')
-rw-r--r-- | contrib/subtac/subtac.ml | 14 | ||||
-rw-r--r-- | contrib/subtac/subtac_cases.ml | 192 | ||||
-rw-r--r-- | contrib/subtac/subtac_classes.ml | 4 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.ml | 2 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 27 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.mli | 5 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 13 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping.mli | 3 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.ml | 24 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.mli | 8 |
10 files changed, 94 insertions, 198 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index ba00fce5..c0b64379 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 11800 2009-01-18 18:34:15Z msozeau $ *) +(* $Id: subtac.ml 12194 2009-06-17 16:38:09Z msozeau $ *) open Global open Pp @@ -99,7 +99,7 @@ let declare_assumption env isevars idl is_coe k bl c nl = Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None in let c = solve_tccs_in_type env id isevars evm c typ in - List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl + List.iter (Command.declare_one_assumption is_coe k c imps false [] nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") @@ -127,7 +127,6 @@ let check_fresh (loc,id) = let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; - check_required_library ["Coq";"Program";"Tactics"]; let env = Global.env () in let isevars = ref (create_evar_defs Evd.empty) in try @@ -143,7 +142,7 @@ let subtac (loc, command) = start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> - ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon)) + ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) | VernacFixpoint (l, b) -> List.iter (fun ((lid, _, _, _, _), _) -> check_fresh lid; @@ -237,9 +236,6 @@ let subtac (loc, command) = debug 2 (Himsg.explain_pretype_error env exn); raise e - | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e''); - raise e) + | e'' -> raise e) - | e -> - msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e); - raise e + | e -> raise e diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 1d213db9..bd06407f 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_cases.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: subtac_cases.ml 12194 2009-06-17 16:38:09Z msozeau $ *) open Cases open Util @@ -301,8 +301,8 @@ module Cases_F(Coercion : Coercion.S) : S = struct let inh_coerce_to_ind isevars env ty tyi = let expected_typ = inductive_template isevars env None tyi in - (* devrait être indifférent d'exiger leq ou pas puisque pour - un inductif cela doit être égal *) + (* devrait être indifférent d'exiger leq ou pas puisque pour + un inductif cela doit être égal *) let _ = e_cumul env isevars expected_typ ty in () let unify_tomatch_with_patterns isevars env loc typ pats = @@ -696,9 +696,9 @@ let insert_aliases_eqn sign eqnnames alias_rest eqn = let insert_aliases env sigma alias eqns = - (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *) - (* défaut présent mais inutile, ce qui est le cas général, l'alias *) - (* est introduit même s'il n'est pas utilisé dans les cas réguliers *) + (* Là , y a une faiblesse, si un alias est utilisé dans un cas par *) + (* défaut présent mais inutile, ce qui est le cas général, l'alias *) + (* est introduit même s'il n'est pas utilisé dans les cas réguliers *) let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in (* names2 takes the meet of all needed aliases *) @@ -843,7 +843,7 @@ let infer_predicate loc env isevars typs cstrs indf = (* Non dependent case -> turn it into a (dummy) dependent one *) let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in - (true,pred) (* true = dependent -- par défaut *) + (true,pred) (* true = dependent -- par défaut *) else (* let s = get_sort_of env (evars_of isevars) typs.(0) in @@ -1294,7 +1294,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest = List.fold_left mkSpecialLetInJudge j sign (* pour les alias des initiaux, enrichir les env de ce qu'il faut et -substituer après par les initiaux *) +substituer après par les initiaux *) (**************************************************************************) (* Preparation of the pattern-matching problem *) @@ -1319,99 +1319,6 @@ let matx_of_eqns env eqns = (************************************************************************) (* preparing the elimination predicate if any *) -let build_expected_arity env isevars isdep tomatchl = - let cook n = function - | _,IsInd (_,IndType(indf,_)) -> - let indf' = lift_inductive_family n indf in - Some (build_dependent_inductive env indf', fst (get_arity env indf')) - | _,NotInd _ -> None - in - let rec buildrec n env = function - | [] -> new_Type () - | tm::ltm -> - match cook n tm with - | None -> buildrec n env ltm - | Some (ty1,aritysign) -> - let rec follow n env = function - | d::sign -> - mkProd_or_LetIn_name env - (follow (n+1) (push_rel d env) sign) d - | [] -> - if isdep then - mkProd (Anonymous, ty1, - buildrec (n+1) - (push_rel_assum (Anonymous, ty1) env) - ltm) - else buildrec n env ltm - in follow n env (List.rev aritysign) - in buildrec 0 env tomatchl - -let extract_predicate_conclusion isdep tomatchl pred = - let cook = function - | _,IsInd (_,IndType(_,args)) -> Some (List.length args) - | _,NotInd _ -> None in - let rec decomp_lam_force n l p = - if n=0 then (l,p) else - match kind_of_term p with - | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c - | _ -> (* eta-expansion *) - let na = Name (id_of_string "x") in - decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in - let rec buildrec allnames p = function - | [] -> (List.rev allnames,p) - | tm::ltm -> - match cook tm with - | None -> - let p = - (* adjust to a sign containing the NotInd's *) - if isdep then lift 1 p else p in - let names = if isdep then [Anonymous] else [] in - buildrec (names::allnames) p ltm - | Some n -> - let n = if isdep then n+1 else n in - let names,p = decomp_lam_force n [] p in - buildrec (names::allnames) p ltm - in buildrec [] pred tomatchl - -let set_arity_signature dep n arsign tomatchl pred x = - (* avoid is not exhaustive ! *) - let rec decomp_lam_force n avoid l p = - if n = 0 then (List.rev l,p,avoid) else - match p with - | RLambda (_,(Name id as na),k,_,c) -> - decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c - | _ -> - let x = next_ident_away (id_of_string "x") avoid in - decomp_lam_force (n-1) (x::avoid) (Name x :: l) - (* eta-expansion *) - (let a = RVar (dummy_loc,x) in - match p with - | RApp (loc,p,l) -> RApp (loc,p,l@[a]) - | _ -> (RApp (dummy_loc,p,[a]))) in - let rec decomp_block avoid p = function - | ([], _) -> x := Some p - | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l') -> - let (ind,params) = dest_ind_family indf in - let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p - in - let na,p,avoid' = - if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid' - in - y := - (List.hd na, - if List.for_all ((=) Anonymous) nal then - None - else - Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal)); - decomp_block avoid' p (l,l') - | (_::l),(y::l') -> - y := (Anonymous,None); - decomp_block avoid p (l,l') - | _ -> anomaly "set_arity_signature" - in - decomp_block [] pred (tomatchl,arsign) - let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c = let cook (n, l, env, signs) = function | c,IsInd (_,IndType(indf,realargs)) -> @@ -1569,9 +1476,6 @@ let eq_id avoid id = let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) -let mk_JMeq typ x typ' y = - mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) -let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |]) let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) @@ -1828,24 +1732,6 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity = * A type constraint but no annotation case: it is assumed non dependent. *) - -let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp = - (* We extract the signature of the arity *) - let arsign = extract_arity_signature env tomatchs sign in - let env = List.fold_right push_rels arsign env in - let allnames = List.rev (List.map (List.map pi1) arsign) in - match rtntyp with - | Some rtntyp -> - let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in - let predccl = (j_nf_isevar !isevars predcclj).uj_val in - Some (build_initial_predicate true allnames predccl) - | None -> - match valcon_of_tycon tycon with - | Some ty -> - let names,pred = - oldprepare_predicate_from_tycon loc false env isevars tomatchs sign ty - in Some (build_initial_predicate true names pred) - | None -> None let lift_ctx n ctx = let ctx', _ = @@ -1862,7 +1748,7 @@ let abstract_tomatch env tomatchs = Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names | _ -> let name = next_ident_away_from (id_of_string "filtered_var") names in - (mkRel 1, lift_tomatch_type 1 t) :: lift_ctx 1 prev, + (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx, name :: names) ([], [], []) tomatchs @@ -1912,7 +1798,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = let previd, id = let name = match kind_of_term arg with - Rel n -> pi1 (lookup_rel n (rel_context env)) + Rel n -> pi1 (Environ.lookup_rel n env) | _ -> name in make_prime avoid name @@ -2025,6 +1911,25 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c = ignore(Typing.sort_of env' evm pred); pred with _ -> lift nar c + +let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp = + (* We extract the signature of the arity *) + let arsign = extract_arity_signature env tomatchs sign in + let newenv = List.fold_right push_rels arsign env in + let allnames = List.rev (List.map (List.map pi1) arsign) in + match rtntyp with + | Some rtntyp -> + let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in + let predccl = (j_nf_isevar !isevars predcclj).uj_val in + Some (build_initial_predicate true allnames predccl) + | None -> + match valcon_of_tycon tycon with + | Some ty -> + let pred = + prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) tomatchs arsign ty + in Some (build_initial_predicate true allnames pred) + | None -> None + let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = let typing_fun tycon env = typing_fun tycon env isevars in @@ -2103,26 +2008,25 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra (* with the type of arguments to match *) let tmsign = List.map snd tomatchl in let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in - - (* We push the initial terms to match and push their alias to rhs' envs *) - (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in - - let pb = - { env = env; - isevars = isevars; - pred = pred; - tomatch = initial_pushed; - history = start_history (List.length initial_pushed); - mat = matx; - caseloc = loc; - casestyle= style; - typing_function = typing_fun } in - - let j = compile pb in - (* We check for unused patterns *) - List.iter (check_unused_pattern env) matx; - inh_conv_coerce_to_tycon loc env isevars j tycon + (* We push the initial terms to match and push their alias to rhs' envs *) + (* names of aliases will be recovered from patterns (hence Anonymous here) *) + let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in + let pb = + { env = env; + isevars = isevars; + pred = pred; + tomatch = initial_pushed; + history = start_history (List.length initial_pushed); + mat = matx; + caseloc = loc; + casestyle= style; + typing_function = typing_fun } in + + let j = compile pb in + (* We check for unused patterns *) + List.iter (check_unused_pattern env) matx; + inh_conv_coerce_to_tycon loc env isevars j tycon + end diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 0d44a0c0..9b692d85 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*) +(*i $Id: subtac_classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) open Pretyping open Evd @@ -182,7 +182,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p in isevars := undefined_evars !isevars; Evarutil.check_evars env Evd.empty !isevars termtype; - let hook gr = + let hook vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in let inst = Typeclasses.new_instance k pri global cst in Impargs.declare_manual_implicits false gr ~enriching:false imps; diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 4876b065..c8c7ff72 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -390,7 +390,7 @@ let interp_recursive fixkind l boxed = (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = - States.with_heavy_rollback (fun () -> + States.with_state_protection (fun () -> List.iter (Command.declare_interning_data impls) notations; list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) () in diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index d2e831ef..3dcd43d2 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -17,8 +17,6 @@ open Evd open Declare open Proof_type -type definition_hook = global_reference -> unit - let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) let pperror cmd = Util.errorlabstrm "Program" cmd let error s = pperror (str s) @@ -56,14 +54,14 @@ type program_info = { prg_implicits : (Topconstr.explicitation * (bool * bool)) list; prg_notations : notations ; prg_kind : definition_kind; - prg_hook : definition_hook; + prg_hook : Tacexpr.declaration_hook; } let assumption_message id = Flags.if_verbose message ((string_of_id id) ^ " is assumed") let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC -let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ()) +let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId []) let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t @@ -203,7 +201,7 @@ let declare_definition prg = if Impargs.is_implicit_args () || prg.prg_implicits <> [] then Impargs.declare_manual_implicits false gr prg.prg_implicits; print_message (Subtac_utils.definition_message prg.prg_name); - prg.prg_hook gr; + prg.prg_hook local gr; gr open Pp @@ -234,6 +232,7 @@ let reduce_fix = let declare_mutual_definition l = let len = List.length l in + let first = List.hd l in let fixdefs, fixtypes, fiximps = list_split3 (List.map (fun x -> @@ -241,11 +240,11 @@ let declare_mutual_definition l = snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l) in (* let fixdefs = List.map reduce_fix fixdefs in *) - let fixkind = Option.get (List.hd l).prg_fixkind in + let fixkind = Option.get first.prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in - let boxed = true (* TODO *) in - let fixnames = (List.hd l).prg_deps in + let (local,boxed,kind) = first.prg_kind in + let fixnames = first.prg_deps in let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in let indexes, fixdecls = match fixkind with @@ -260,9 +259,11 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in (* Declare notations *) - List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations; + List.iter (Command.declare_interning_data ([],[])) first.prg_notations; Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames); - (match List.hd kns with ConstRef kn -> kn | _ -> assert false) + let gr = List.hd kns in + let kn = match gr with ConstRef kn -> kn | _ -> assert false in + first.prg_hook local gr; kn let declare_obligation obl body = match obl.obl_status with @@ -525,7 +526,7 @@ let show_term n = my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ my_print_constr (Global.env ()) prg.prg_body) -let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls = +let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls = Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let prg = init_prog_info n b t [] None [] obls implicits kind hook in let obls,_ = prg.prg_obligations in @@ -543,11 +544,11 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind = +let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in let upd = List.fold_left (fun acc (n, b, t, imps, obls) -> - let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun x -> ()) in + let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind hook in ProgMap.add n prg acc) !from_prg l in diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 60c0a413..766af2fa 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -21,13 +21,11 @@ val default_tactic : unit -> Proof_type.tactic val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) val get_proofs_transparency : unit -> bool -type definition_hook = global_reference -> unit - val add_definition : Names.identifier -> Term.constr -> Term.types -> ?implicits:(Topconstr.explicitation * (bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:Proof_type.tactic -> - ?hook:definition_hook -> obligation_info -> progress + ?hook:Tacexpr.declaration_hook -> obligation_info -> progress type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list @@ -36,6 +34,7 @@ val add_mutual_definitions : (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> ?tactic:Proof_type.tactic -> ?kind:Decl_kinds.definition_kind -> + ?hook:Tacexpr.declaration_hook -> notations -> Command.fixpoint_kind -> unit diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 07a75720..3ae7c95d 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 11574 2008-11-10 13:45:05Z msozeau $ *) +(* $Id: subtac_pretyping.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Global open Pp @@ -84,13 +84,6 @@ let find_with_index x l = | [] -> raise Not_found in aux 0 l -let list_split_at index l = - let rec aux i acc = function - hd :: tl when i = index -> (List.rev acc), tl - | hd :: tl -> aux (succ i) (hd :: acc) tl - | [] -> failwith "list_split_at: Invalid argument" - in aux 0 [] l - open Vernacexpr let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env @@ -136,9 +129,9 @@ let subtac_process env isevars id bl c tycon = open Subtac_obligations -let subtac_proof kind env isevars id bl c tycon = +let subtac_proof kind hook env isevars id bl c tycon = let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in let evm' = Subtac_utils.evars_of_term evm evm' coqt in let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in - add_definition id def ty ~implicits:imps ~kind:kind evars + add_definition id def ty ~implicits:imps ~kind ~hook evars diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli index 1d8eb250..ba0b7cd2 100644 --- a/contrib/subtac/subtac_pretyping.mli +++ b/contrib/subtac/subtac_pretyping.mli @@ -19,5 +19,6 @@ val interp : val subtac_process : env -> evar_defs ref -> identifier -> local_binder list -> constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list -val subtac_proof : Decl_kinds.definition_kind -> env -> evar_defs ref -> identifier -> local_binder list -> +val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> + env -> evar_defs ref -> identifier -> local_binder list -> constr_expr -> constr_expr option -> Subtac_obligations.progress diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index cdbc4023..2ee2018e 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -64,15 +64,17 @@ let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec") let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep") let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro") -let jmeq_ind = - lazy (check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq") -let jmeq_rec = - lazy (check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq_rec") -let jmeq_refl = - lazy (check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq_refl") +let jmeq_ind () = + check_required_library ["Coq";"Logic";"JMeq"]; + init_constant ["Logic";"JMeq"] "JMeq" + +let jmeq_rec () = + check_required_library ["Coq";"Logic";"JMeq"]; + init_constant ["Logic";"JMeq"] "JMeq_rec" + +let jmeq_refl () = + check_required_library ["Coq";"Logic";"JMeq"]; + init_constant ["Logic";"JMeq"] "JMeq_refl" let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex") let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro") @@ -277,8 +279,8 @@ let mkSubset name typ prop = let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) -let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |]) -let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |]) +let mk_JMeq typ x typ' y = mkApp (jmeq_ind (), [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (jmeq_refl (), [| typ; x |]) let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 964f668f..9c014286 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -45,9 +45,9 @@ val and_typ : constr lazy_t val eqdep_ind : constr lazy_t val eqdep_rec : constr lazy_t -val jmeq_ind : constr lazy_t -val jmeq_rec : constr lazy_t -val jmeq_refl : constr lazy_t +val jmeq_ind : unit -> constr +val jmeq_rec : unit -> constr +val jmeq_refl : unit -> constr val boolind : constr lazy_t val sumboolind : constr lazy_t @@ -103,7 +103,7 @@ val mk_ex_pi1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr val mk_eq : types -> constr -> constr -> types val mk_eq_refl : types -> constr -> constr -val mk_JMeq : types -> constr-> types -> constr -> types +val mk_JMeq : types -> constr -> types -> constr -> types val mk_JMeq_refl : types -> constr -> constr val mk_conj : types list -> types val mk_not : types -> types |