summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/interface/depends.ml8
-rw-r--r--contrib/subtac/subtac.ml14
-rw-r--r--contrib/subtac/subtac_cases.ml192
-rw-r--r--contrib/subtac/subtac_classes.ml4
-rw-r--r--contrib/subtac/subtac_command.ml2
-rw-r--r--contrib/subtac/subtac_obligations.ml27
-rw-r--r--contrib/subtac/subtac_obligations.mli5
-rw-r--r--contrib/subtac/subtac_pretyping.ml13
-rw-r--r--contrib/subtac/subtac_pretyping.mli3
-rw-r--r--contrib/subtac/subtac_utils.ml24
-rw-r--r--contrib/subtac/subtac_utils.mli8
-rw-r--r--contrib/xml/proofTree2Xml.ml44
12 files changed, 100 insertions, 204 deletions
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index e59de34a..e0f43193 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -58,8 +58,8 @@ let explore_tree pfs =
| Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
| Intro identifier -> "Intro"
| Cut (bool, _, identifier, types) -> "Cut"
- | FixRule (identifier, int, l) -> "FixRule"
- | Cofix (identifier, l) -> "Cofix"
+ | FixRule (identifier, int, l, _) -> "FixRule"
+ | Cofix (identifier, l, _) -> "Cofix"
| Convert_concl (types, cast_kind) -> "Convert_concl"
| Convert_hyp named_declaration -> "Convert_hyp"
| Thin identifier_list -> "Thin"
@@ -411,8 +411,8 @@ and depends_of_prim_rule pr acc = match pr with
| Refine c -> depends_of_constr c acc
| Intro id -> acc
| Cut (_, _, _, t) -> depends_of_constr t acc (* TODO: check what 3nd argument contains *)
- | FixRule (_, _, l) -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
- | Cofix (_, l) -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
+ | FixRule (_, _, l, _) -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
+ | Cofix (_, l, _) -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
| Convert_concl (t, _) -> depends_of_constr t acc
| Convert_hyp (_, None, t) -> depends_of_constr t acc
| Convert_hyp (_, (Some c), t) -> depends_of_constr c (depends_of_constr t acc)
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
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index a501fb6a..7503d632 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -82,8 +82,8 @@ let first_word s =
let string_of_prim_rule x = match x with
| Proof_type.Intro _-> "Intro"
| Proof_type.Cut _ -> "Cut"
- | Proof_type.FixRule (_,_,_) -> "FixRule"
- | Proof_type.Cofix (_,_)-> "Cofix"
+ | Proof_type.FixRule _ -> "FixRule"
+ | Proof_type.Cofix _ -> "Cofix"
| Proof_type.Refine _ -> "Refine"
| Proof_type.Convert_concl _ -> "Convert_concl"
| Proof_type.Convert_hyp _->"Convert_hyp"
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 05:14:34 +0000