aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml86
-rw-r--r--tactics/autorewrite.ml90
-rw-r--r--tactics/autorewrite.mli10
-rw-r--r--tactics/btermdn.ml28
-rw-r--r--tactics/class_tactics.ml8
-rw-r--r--tactics/contradiction.ml16
-rw-r--r--tactics/dn.ml48
-rw-r--r--tactics/dnet.ml162
-rw-r--r--tactics/eauto.ml164
-rw-r--r--tactics/elim.ml26
-rw-r--r--tactics/elimschemes.ml6
-rw-r--r--tactics/elimschemes.mli2
-rw-r--r--tactics/eqschemes.ml128
-rw-r--r--tactics/eqschemes.mli8
-rw-r--r--tactics/equality.ml200
-rw-r--r--tactics/equality.mli2
-rw-r--r--tactics/hints.ml186
-rw-r--r--tactics/hints.mli18
-rw-r--r--tactics/hipattern.ml70
-rw-r--r--tactics/hipattern.mli4
-rw-r--r--tactics/ind_tables.mli2
-rw-r--r--tactics/inv.ml76
-rw-r--r--tactics/leminv.ml44
-rw-r--r--tactics/tacticals.ml22
-rw-r--r--tactics/tacticals.mli4
-rw-r--r--tactics/tactics.ml660
-rw-r--r--tactics/tactics.mli8
-rw-r--r--tactics/term_dnet.ml78
28 files changed, 1078 insertions, 1078 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0b465418f2..9c1a975330 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -135,9 +135,9 @@ let conclPattern concl pat tac =
match pat with
| None -> Proofview.tclUNIT Id.Map.empty
| Some pat ->
- try
- Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
- with Constr_matching.PatternMatchingFailure ->
+ try
+ Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
+ with Constr_matching.PatternMatchingFailure ->
Tacticals.New.tclZEROMSG (str "pattern-matching failed")
in
Proofview.Goal.enter begin fun gl ->
@@ -323,9 +323,9 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
let nf c = Evarutil.nf_evar sigma c in
let decl = Tacmach.New.pf_last_hyp gl in
let hyp = Context.Named.Declaration.map_constr nf decl in
- let hintl = make_resolve_hyp env sigma hyp
- in trivial_fail_db dbg mod_delta db_list
- (Hint_db.add_list env sigma hintl local_db)
+ let hintl = make_resolve_hyp env sigma hyp
+ in trivial_fail_db dbg mod_delta db_list
+ (Hint_db.add_list env sigma hintl local_db)
end)
in
Proofview.Goal.enter begin fun gl ->
@@ -350,31 +350,31 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
let f = hintmap_of sigma secvars hdc concl in
if occur_existential sigma concl then
List.map_append
- (fun db ->
- if Hint_db.use_dn db then
- let flags = flags_of_state (Hint_db.transparent_state db) in
- List.map (fun x -> (Some flags,x)) (f db)
- else
- let flags = auto_flags_of_state (Hint_db.transparent_state db) in
- List.map (fun x -> (Some flags,x)) (f db))
- (local_db::db_list)
+ (fun db ->
+ if Hint_db.use_dn db then
+ let flags = flags_of_state (Hint_db.transparent_state db) in
+ List.map (fun x -> (Some flags,x)) (f db)
+ else
+ let flags = auto_flags_of_state (Hint_db.transparent_state db) in
+ List.map (fun x -> (Some flags,x)) (f db))
+ (local_db::db_list)
else
List.map_append (fun db ->
- if Hint_db.use_dn db then
- let flags = flags_of_state (Hint_db.transparent_state db) in
- List.map (fun x -> (Some flags, x)) (f db)
- else
+ if Hint_db.use_dn db then
+ let flags = flags_of_state (Hint_db.transparent_state db) in
+ List.map (fun x -> (Some flags, x)) (f db)
+ else
let st = Hint_db.transparent_state db in
- let flags, l =
- let l =
- match hdc with None -> Hint_db.map_none ~secvars db
- | Some hdc ->
+ let flags, l =
+ let l =
+ match hdc with None -> Hint_db.map_none ~secvars db
+ | Some hdc ->
if TransparentState.is_empty st
- then Hint_db.map_auto sigma ~secvars hdc concl db
- else Hint_db.map_existential sigma ~secvars hdc concl db
- in auto_flags_of_state st, l
- in List.map (fun x -> (Some flags,x)) l)
- (local_db::db_list)
+ then Hint_db.map_auto sigma ~secvars hdc concl db
+ else Hint_db.map_existential sigma ~secvars hdc concl db
+ in auto_flags_of_state st, l
+ in List.map (fun x -> (Some flags,x)) l)
+ (local_db::db_list)
and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
let tactic = function
@@ -384,13 +384,13 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
| Res_pf_THEN_trivial_fail (c,cl) ->
Tacticals.New.tclTHEN
(unify_resolve_gen ~poly flags (c,cl))
- (* With "(debug) trivial", we shouldn't end here, and
- with "debug auto" we don't display the details of inner trivial *)
+ (* With "(debug) trivial", we shouldn't end here, and
+ with "debug auto" we don't display the details of inner trivial *)
(trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)
| Unfold_nth c ->
Proofview.Goal.enter begin fun gl ->
if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
- Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
+ Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
else Tacticals.New.tclFAIL 0 (str"Unbound reference")
end
| Extern tacast ->
@@ -409,12 +409,12 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
try
let head =
try let hdconstr = decompose_app_bound sigma cl in
- Some hdconstr
+ Some hdconstr
with Bound -> None
in
List.map (tac_of_hint dbg db_list local_db cl)
- (priority
- (my_find_search mod_delta sigma db_list local_db secvars head cl))
+ (priority
+ (my_find_search mod_delta sigma db_list local_db secvars head cl))
with Not_found -> []
(** The use of the "core" database can be de-activated by passing
@@ -458,11 +458,11 @@ let possible_resolve sigma dbg mod_delta db_list local_db secvars cl =
try
let head =
try let hdconstr = decompose_app_bound sigma cl in
- Some hdconstr
+ Some hdconstr
with Bound -> None
in
List.map (tac_of_hint dbg db_list local_db cl)
- (my_find_search mod_delta sigma db_list local_db secvars head cl)
+ (my_find_search mod_delta sigma db_list local_db secvars head cl)
with Not_found -> []
let extend_local_db decl db gl =
@@ -490,16 +490,16 @@ let search d n mod_delta db_list local_db =
Proofview.tclEXTEND [] begin
if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
Tacticals.New.tclORELSE0 (dbg_assumption d)
- (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
- ( Proofview.Goal.enter begin fun gl ->
+ (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
+ ( Proofview.Goal.enter begin fun gl ->
let concl = Tacmach.New.pf_concl gl in
let sigma = Tacmach.New.project gl in
let secvars = compute_secvars gl in
- let d' = incr_dbg d in
- Tacticals.New.tclFIRST
- (List.map
- (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
- (possible_resolve sigma d mod_delta db_list local_db secvars concl))
+ let d' = incr_dbg d in
+ Tacticals.New.tclFIRST
+ (List.map
+ (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
+ (possible_resolve sigma d mod_delta db_list local_db secvars concl))
end))
end []
in
@@ -519,7 +519,7 @@ let delta_auto debug mod_delta n lems dbnames =
(search d n mod_delta db_list hints)
end
-let delta_auto =
+let delta_auto =
if Flags.profile then
let key = CProfile.declare_profile "delta_auto" in
CProfile.profile5 key delta_auto
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 0bc410010c..cd6f445503 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -20,11 +20,11 @@ open Locus
(* Rewriting rules *)
type rew_rule = { rew_lemma: constr;
- rew_type: types;
- rew_pat: constr;
- rew_ctx: Univ.ContextSet.t;
- rew_l2r: bool;
- rew_tac: Genarg.glob_generic_argument option }
+ rew_type: types;
+ rew_pat: constr;
+ rew_ctx: Univ.ContextSet.t;
+ rew_l2r: bool;
+ rew_tac: Genarg.glob_generic_argument option }
let subst_hint subst hint =
let cst' = subst_mps subst hint.rew_lemma in
@@ -33,8 +33,8 @@ let subst_hint subst hint =
let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in
if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
{ hint with
- rew_lemma = cst'; rew_type = typ';
- rew_pat = pat'; rew_tac = t' }
+ rew_lemma = cst'; rew_type = typ';
+ rew_pat = pat'; rew_tac = t' }
module HintIdent =
struct
@@ -79,13 +79,13 @@ let print_rewrite_hintdb bas =
let env = Global.env () in
let sigma = Evd.from_env env in
(str "Database " ++ str bas ++ fnl () ++
- prlist_with_sep fnl
- (fun h ->
- str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
+ prlist_with_sep fnl
+ (fun h ->
+ str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++
- Option.cata (fun tac -> str " then use tactic " ++
+ Option.cata (fun tac -> str " then use tactic " ++
Pputils.pr_glb_generic env sigma tac) (mt ()) h.rew_tac)
- (find_rewrites bas))
+ (find_rewrites bas))
type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t
@@ -116,7 +116,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) ->
Tacticals.New.tclTHEN tac
(Tacticals.New.tclREPEAT_MAIN
- (Tacticals.New.tclTHENFIRST (try_rewrite dir ctx csr tc) tac_main)))
+ (Tacticals.New.tclTHENFIRST (try_rewrite dir ctx csr tc) tac_main)))
(Proofview.tclUNIT()) lrul))
(* The AutoRewrite tactic *)
@@ -125,9 +125,9 @@ let autorewrite ?(conds=Naive) tac_main lbas =
(List.fold_left (fun tac bas ->
Tacticals.New.tclTHEN tac
(one_base (fun dir c tac ->
- let tac = (tac, conds) in
- general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c))
- tac_main bas))
+ let tac = (tac, conds) in
+ general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c))
+ tac_main bas))
(Proofview.tclUNIT()) lbas))
let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
@@ -158,19 +158,19 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
else
let compose_tac t1 t2 =
match cl.onhyps with
- | Some [] -> t1
- | _ -> Tacticals.New.tclTHENFIRST t1 t2
+ | Some [] -> t1
+ | _ -> Tacticals.New.tclTHENFIRST t1 t2
in
compose_tac
- (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ())
- (match cl.onhyps with
- | Some l -> try_do_hyps (fun ((_,id),_) -> id) l
- | None ->
- (* try to rewrite in all hypothesis
- (except maybe the rewritten one) *)
+ (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ())
+ (match cl.onhyps with
+ | Some l -> try_do_hyps (fun ((_,id),_) -> id) l
+ | None ->
+ (* try to rewrite in all hypothesis
+ (except maybe the rewritten one) *)
Proofview.Goal.enter begin fun gl ->
let ids = Tacmach.New.pf_ids_of_hyps gl in
- try_do_hyps (fun id -> id) ids
+ try_do_hyps (fun id -> id) ids
end)
let auto_multi_rewrite ?(conds=Naive) lems cl =
@@ -180,10 +180,10 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in
match onconcl,cl.Locus.onhyps with
| false,Some [_] | true,Some [] | false,Some [] ->
- (* autorewrite with .... in clause using tac n'est sur que
- si clause represente soit le but soit UNE hypothese
- *)
- Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl)
+ (* autorewrite with .... in clause using tac n'est sur que
+ si clause represente soit le but soit UNE hypothese
+ *)
+ Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl)
| _ ->
Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
@@ -233,7 +233,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
- let l,res = split_last_two (y::z) in x::l, res
+ let l,res = split_last_two (y::z) in x::l, res
| _ -> raise Not_found
in
try
@@ -255,19 +255,19 @@ let decompose_applied_relation metas env sigma c ctype left2right =
match find_rel ctype with
| Some c -> Some c
| None ->
- let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
- match find_rel (it_mkProd_or_LetIn t' ctx) with
- | Some c -> Some c
- | None -> None
+ let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
+ match find_rel (it_mkProd_or_LetIn t' ctx) with
+ | Some c -> Some c
+ | None -> None
let find_applied_relation ?loc metas env sigma c left2right =
let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
match decompose_applied_relation metas env sigma c ctype left2right with
| Some c -> c
| None ->
- user_err ?loc ~hdr:"decompose_applied_relation"
- (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++
- spc () ++ str"of this term does not end with an applied relation.")
+ user_err ?loc ~hdr:"decompose_applied_relation"
+ (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++
+ spc () ++ str"of this term does not end with an applied relation.")
(* To add rewriting rules to a base *)
let add_rew_rules base lrul =
@@ -279,13 +279,13 @@ let add_rew_rules base lrul =
let lrul =
List.fold_left
(fun dn {CAst.loc;v=((c,ctx),b,t)} ->
- let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
- let info = find_applied_relation ?loc false env sigma c b in
- let pat = if b then info.hyp_left else info.hyp_right in
- let rul = { rew_lemma = c; rew_type = info.hyp_ty;
- rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
- rew_tac = Option.map intern t}
- in incr counter;
- HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
+ let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
+ let info = find_applied_relation ?loc false env sigma c b in
+ let pat = if b then info.hyp_left else info.hyp_right in
+ let rul = { rew_lemma = c; rew_type = info.hyp_ty;
+ rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
+ rew_tac = Option.map intern t}
+ in incr counter;
+ HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index e5125ffe50..6df2ea9b12 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -28,11 +28,11 @@ val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic ->
(** Rewriting rules *)
type rew_rule = { rew_lemma: constr;
- rew_type: types;
- rew_pat: constr;
- rew_ctx: Univ.ContextSet.t;
- rew_l2r: bool;
- rew_tac: Genarg.glob_generic_argument option }
+ rew_type: types;
+ rew_pat: constr;
+ rew_ctx: Univ.ContextSet.t;
+ rew_l2r: bool;
+ rew_tac: Genarg.glob_generic_argument option }
val find_rewrites : string -> rew_rule list
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index d0816b266f..ae3aea5788 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -80,8 +80,8 @@ let constr_val_discr_st sigma ts t =
| Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l)
| Prod (n, d, c) -> Label(ProdLabel, [d; c])
| Lambda (n, d, c) ->
- if List.is_empty l then
- Label(LambdaLabel, [d; c] @ l)
+ if List.is_empty l then
+ Label(LambdaLabel, [d; c] @ l)
else Everything
| Sort _ -> Label(SortLabel, [])
| Evar _ -> Everything
@@ -154,27 +154,27 @@ struct
let add = function
| None ->
- (fun dn (c,v) ->
- Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+ (fun dn (c,v) ->
+ Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
| Some st ->
- (fun dn (c,v) ->
- Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+ (fun dn (c,v) ->
+ Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
let rmv = function
| None ->
- (fun dn (c,v) ->
- Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+ (fun dn (c,v) ->
+ Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
| Some st ->
- (fun dn (c,v) ->
- Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+ (fun dn (c,v) ->
+ Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
let lookup sigma = function
| None ->
- (fun dn t ->
- Dn.lookup dn (bounded_constr_val_discr sigma) (t,!dnet_depth))
+ (fun dn t ->
+ Dn.lookup dn (bounded_constr_val_discr sigma) (t,!dnet_depth))
| Some st ->
- (fun dn t ->
- Dn.lookup dn (bounded_constr_val_discr_st sigma st) (t,!dnet_depth))
+ (fun dn t ->
+ Dn.lookup dn (bounded_constr_val_discr_st sigma st) (t,!dnet_depth))
let app f dn = Dn.app f dn
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index cf5c64c3ae..f8cb8870ea 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -457,7 +457,7 @@ let catchable = function
| Refiner.FailError _ -> true
| e -> Logic.catchable_exception e
-let pr_depth l =
+let pr_depth l =
let rec fmt elts =
match elts with
| [] -> []
@@ -758,8 +758,8 @@ module Search = struct
Feedback.msg_debug
(str"Adding shelved subgoals to the search: " ++
prlist_with_sep spc (pr_ev sigma) goals ++
- str" while shelving " ++
- prlist_with_sep spc (pr_ev sigma) shelved);
+ str" while shelving " ++
+ prlist_with_sep spc (pr_ev sigma) shelved);
shelve_goals shelved <*>
(if List.is_empty goals then tclUNIT ()
else
@@ -776,7 +776,7 @@ module Search = struct
(with_shelf tac >>= fun s ->
let i = !idx in incr idx; result s i None)
(fun e' ->
- if CErrors.noncritical (fst e') then
+ if CErrors.noncritical (fst e') then
(pr_error e'; aux (merge_exceptions e e') tl)
else iraise e')
and aux e = function
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 56e8e7a11f..1f5a6380fd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -66,10 +66,10 @@ let contradiction_context =
| d :: rest ->
let id = NamedDecl.get_id d in
let typ = nf_evar sigma (NamedDecl.get_type d) in
- let typ = whd_all env sigma typ in
+ let typ = whd_all env sigma typ in
if is_empty_type env sigma typ then
- simplest_elim (mkVar id)
- else match EConstr.kind sigma typ with
+ simplest_elim (mkVar id)
+ else match EConstr.kind sigma typ with
| Prod (na,t,u) when is_empty_type env sigma u ->
let is_unit_or_eq = match_with_unit_or_eq_type env sigma t in
Tacticals.New.tclORELSE
@@ -84,17 +84,17 @@ let contradiction_context =
simplest_elim (mkApp (mkVar id,[|p|]))
| None ->
Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type."))
- (Proofview.tclORELSE
+ (Proofview.tclORELSE
(Proofview.Goal.enter begin fun gl ->
let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
- filter_hyp (fun typ -> is_conv_leq typ t)
- (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
+ filter_hyp (fun typ -> is_conv_leq typ t)
+ (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
end)
begin function (e, info) -> match e with
- | Not_found -> seek_neg rest
+ | Not_found -> seek_neg rest
| e -> Proofview.tclZERO ~info e
end)
- | _ -> seek_neg rest
+ | _ -> seek_neg rest
in
let hyps = Proofview.Goal.hyps gl in
seek_neg hyps
diff --git a/tactics/dn.ml b/tactics/dn.ml
index aed2c28323..e1c9b7c0b5 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -11,14 +11,14 @@ struct
type t = (Y.t * int) option
let compare x y =
match x,y with
- None,None -> 0
- | Some (l,n),Some (l',n') ->
- let m = Y.compare l l' in
- if Int.equal m 0 then
- n-n'
- else m
- | Some(l,n),None -> 1
- | None, Some(l,n) -> -1
+ None,None -> 0
+ | Some (l,n),Some (l',n') ->
+ let m = Y.compare l l' in
+ if Int.equal m 0 then
+ n-n'
+ else m
+ | Some(l,n),None -> 1
+ | None, Some(l,n) -> -1
end
module ZSet = Set.Make(Z)
module X_tries =
@@ -50,12 +50,12 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
and pathrec deferred t =
match dna t with
- | None ->
- None :: (path_of_deferred deferred)
- | Some (lbl,[]) ->
- (Some (lbl,0))::(path_of_deferred deferred)
- | Some (lbl,(h::def_subl as v)) ->
- (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
+ | None ->
+ None :: (path_of_deferred deferred)
+ | Some (lbl,[]) ->
+ (Some (lbl,0))::(path_of_deferred deferred)
+ | Some (lbl,(h::def_subl as v)) ->
+ (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
in
pathrec []
@@ -76,16 +76,16 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
let lookup tm dna t =
let rec lookrec t tm =
match dna t with
- | Nothing -> tm_of tm None
- | Label(lbl,v) ->
- tm_of tm None@
- (List.fold_left
- (fun l c ->
- List.flatten(List.map (fun (tm, b) ->
- if b then lookrec c tm
- else [tm,b]) l))
- (tm_of tm (Some(lbl,List.length v))) v)
- | Everything -> skip_arg 1 tm
+ | Nothing -> tm_of tm None
+ | Label(lbl,v) ->
+ tm_of tm None@
+ (List.fold_left
+ (fun l c ->
+ List.flatten(List.map (fun (tm, b) ->
+ if b then lookrec c tm
+ else [tm,b]) l))
+ (tm_of tm (Some(lbl,List.length v))) v)
+ | Everything -> skip_arg 1 tm
in
List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm))
diff --git a/tactics/dnet.ml b/tactics/dnet.ml
index 3171bee7ca..389329c19f 100644
--- a/tactics/dnet.ml
+++ b/tactics/dnet.ml
@@ -62,7 +62,7 @@ struct
module Idset = Set.Make(Ident)
module Mmap = Map.Make(Meta)
module Tmap = Map.Make(struct type t = unit structure
- let compare = T.compare end)
+ let compare = T.compare end)
type idset = Idset.t
@@ -93,23 +93,23 @@ struct
let rec add (Nodes (t,m):t) (w:term_pattern) (id:ident) : t =
match w with Term w ->
( try
- let (n,tl) = split t w in
- let new_node = match n with
- | Terminal (e,is) -> Terminal (e,Idset.add id is)
- | Node e -> Node (T.map2 (fun t p -> add t p id) e w) in
- Nodes ((Tmap.add (head w) new_node tl), m)
- with Not_found ->
- let new_content = T.map (fun p -> add empty p id) w in
- let new_node =
- if T.terminal w then
- Terminal (new_content, Idset.singleton id)
- else Node new_content in
- Nodes ((Tmap.add (head w) new_node t), m) )
+ let (n,tl) = split t w in
+ let new_node = match n with
+ | Terminal (e,is) -> Terminal (e,Idset.add id is)
+ | Node e -> Node (T.map2 (fun t p -> add t p id) e w) in
+ Nodes ((Tmap.add (head w) new_node tl), m)
+ with Not_found ->
+ let new_content = T.map (fun p -> add empty p id) w in
+ let new_node =
+ if T.terminal w then
+ Terminal (new_content, Idset.singleton id)
+ else Node new_content in
+ Nodes ((Tmap.add (head w) new_node t), m) )
| Meta i ->
- let m =
- try Mmap.add i (Idset.add id (Mmap.find i m)) m
- with Not_found -> Mmap.add i (Idset.singleton id) m in
- Nodes (t, m)
+ let m =
+ try Mmap.add i (Idset.add id (Mmap.find i m)) m
+ with Not_found -> Mmap.add i (Idset.singleton id) m in
+ Nodes (t, m)
let add t w id = add t w id
@@ -117,12 +117,12 @@ struct
Idset.union
(Mmap.fold (fun _ -> Idset.union) m Idset.empty)
(Tmap.fold
- ( fun _ n acc ->
- let s2 = match n with
- | Terminal (_,is) -> is
- | Node e -> T.choose find_all e in
- Idset.union acc s2
- ) t Idset.empty)
+ ( fun _ n acc ->
+ let s2 = match n with
+ | Terminal (_,is) -> is
+ | Node e -> T.choose find_all e in
+ Idset.union acc s2
+ ) t Idset.empty)
(* (\* optimization hack: Not_found is caught in fold_pattern *\) *)
(* let fast_inter s1 s2 = *)
@@ -176,13 +176,13 @@ struct
let inter s1 s2 : t = match s1,s2 with
| (None, a | a, None) -> a
| Some a, Some b -> Some (S.inter a b)
- let is_empty : t -> bool = function
+ let is_empty : t -> bool = function
| None -> false
| Some s -> S.is_empty s
(* optimization hack: Not_found is caught in fold_pattern *)
let fast_inter s1 s2 =
if is_empty s1 || is_empty s2 then raise Not_found
- else let r = inter s1 s2 in
+ else let r = inter s1 s2 in
if is_empty r then raise Not_found else r
let full = None
let empty = Some S.empty
@@ -197,29 +197,29 @@ struct
let rec fp_rec metas p (Nodes(t,m) as dn:t) =
(* TODO gérer les dnets non-linéaires *)
let metas = Mmap.fold (fun _ -> Idset.union) m metas in
- match p with
- | Meta m -> defer (metas,m,dn); OIdset.full
- | Term w ->
- let curm = Mmap.fold (fun _ -> Idset.union) m Idset.empty in
- try match select t w with
- | Terminal (_,is) -> Some (Idset.union curm is)
- | Node e ->
- let ids = if complete then T.fold2
- (fun acc w e ->
- OIdset.fast_inter acc (fp_rec metas w e)
- ) OIdset.full w e
- else
- let (all_metas, res) = T.fold2
- (fun (b,acc) w e -> match w with
- | Term _ -> false, OIdset.fast_inter acc (fp_rec metas w e)
- | Meta _ -> b, acc
- ) (true,OIdset.full) w e in
- if all_metas then T.choose (T.choose (fp_rec metas) w) e
- else res in
- OIdset.union ids (Some curm)
- with Not_found ->
- if Idset.is_empty metas then raise Not_found else Some curm in
- let cand =
+ match p with
+ | Meta m -> defer (metas,m,dn); OIdset.full
+ | Term w ->
+ let curm = Mmap.fold (fun _ -> Idset.union) m Idset.empty in
+ try match select t w with
+ | Terminal (_,is) -> Some (Idset.union curm is)
+ | Node e ->
+ let ids = if complete then T.fold2
+ (fun acc w e ->
+ OIdset.fast_inter acc (fp_rec metas w e)
+ ) OIdset.full w e
+ else
+ let (all_metas, res) = T.fold2
+ (fun (b,acc) w e -> match w with
+ | Term _ -> false, OIdset.fast_inter acc (fp_rec metas w e)
+ | Meta _ -> b, acc
+ ) (true,OIdset.full) w e in
+ if all_metas then T.choose (T.choose (fp_rec metas) w) e
+ else res in
+ OIdset.union ids (Some curm)
+ with Not_found ->
+ if Idset.is_empty metas then raise Not_found else Some curm in
+ let cand =
try fp_rec Idset.empty pat dn
with Not_found -> OIdset.empty in
let res = List.fold_left f acc !deferred in
@@ -229,54 +229,54 @@ struct
let rec inter (t1:t) (t2:t) : t =
let inter_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t =
Nodes
- (Tmap.fold
- ( fun k e acc ->
- try Tmap.add k (f e (Tmap.find k t2)) acc
- with Not_found -> acc
- ) t1 Tmap.empty,
- Mmap.fold
- ( fun m s acc ->
- try Mmap.add m (Idset.inter s (Mmap.find m m2)) acc
- with Not_found -> acc
- ) m1 Mmap.empty
- ) in
+ (Tmap.fold
+ ( fun k e acc ->
+ try Tmap.add k (f e (Tmap.find k t2)) acc
+ with Not_found -> acc
+ ) t1 Tmap.empty,
+ Mmap.fold
+ ( fun m s acc ->
+ try Mmap.add m (Idset.inter s (Mmap.find m m2)) acc
+ with Not_found -> acc
+ ) m1 Mmap.empty
+ ) in
inter_map
(fun n1 n2 -> match n1,n2 with
- | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.inter s1 s2)
- | Node e1, Node e2 -> Node (T.map2 inter e1 e2)
- | _ -> assert false
+ | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.inter s1 s2)
+ | Node e1, Node e2 -> Node (T.map2 inter e1 e2)
+ | _ -> assert false
) t1 t2
let rec union (t1:t) (t2:t) : t =
let union_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t =
Nodes
- (Tmap.fold
- ( fun k e acc ->
- try Tmap.add k (f e (Tmap.find k acc)) acc
- with Not_found -> Tmap.add k e acc
- ) t1 t2,
- Mmap.fold
- ( fun m s acc ->
- try Mmap.add m (Idset.inter s (Mmap.find m acc)) acc
- with Not_found -> Mmap.add m s acc
- ) m1 m2
- ) in
+ (Tmap.fold
+ ( fun k e acc ->
+ try Tmap.add k (f e (Tmap.find k acc)) acc
+ with Not_found -> Tmap.add k e acc
+ ) t1 t2,
+ Mmap.fold
+ ( fun m s acc ->
+ try Mmap.add m (Idset.inter s (Mmap.find m acc)) acc
+ with Not_found -> Mmap.add m s acc
+ ) m1 m2
+ ) in
union_map
(fun n1 n2 -> match n1,n2 with
- | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.union s1 s2)
- | Node e1, Node e2 -> Node (T.map2 union e1 e2)
- | _ -> assert false
+ | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.union s1 s2)
+ | Node e1, Node e2 -> Node (T.map2 union e1 e2)
+ | _ -> assert false
) t1 t2
let find_match (p:term_pattern) (t:t) : idset =
let metas = ref Mmap.empty in
let (mset,lset) = fold_pattern ~complete:false
(fun acc (mset,m,t) ->
- let all = OIdset.fast_inter acc
- (Some(let t = try inter t (Mmap.find m !metas) with Not_found -> t in
- metas := Mmap.add m t !metas;
- find_all t)) in
- OIdset.union (Some mset) all
+ let all = OIdset.fast_inter acc
+ (Some(let t = try inter t (Mmap.find m !metas) with Not_found -> t in
+ metas := Mmap.add m t !metas;
+ find_all t)) in
+ OIdset.union (Some mset) all
) None p t in
Option.get (OIdset.inter mset lset)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index ef2402489e..361215bf38 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -154,8 +154,8 @@ and e_my_find_search env sigma db_list local_db secvars hdc concl =
let hint_of_db = hintmap_of sigma secvars hdc concl in
let hintl =
List.map_append (fun db ->
- let flags = auto_flags_of_state (Hint_db.transparent_state db) in
- List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list)
+ let flags = auto_flags_of_state (Hint_db.transparent_state db) in
+ List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list)
in
let tac_of_hint =
fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
@@ -227,12 +227,12 @@ module SearchProblem = struct
let rec aux = function
| [] -> []
| (tac, cost, pptac) :: tacl ->
- try
- let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in
+ try
+ let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in
(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
- (lgls, cost, pptac) :: aux tacl
- with e when CErrors.noncritical e ->
+ (lgls, cost, pptac) :: aux tacl
+ with e when CErrors.noncritical e ->
let e = CErrors.push e in
Refiner.catch_failerror e; aux tacl
in aux l
@@ -262,60 +262,60 @@ module SearchProblem = struct
let assumption_tacs =
let tacs = List.map map_assum hyps in
let l = filter_tactics s.tacres tacs in
- List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
- last_tactic = pp; dblist = s.dblist;
- localdb = List.tl s.localdb;
- prev = ps; local_lemmas = s.local_lemmas}) l
+ List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
+ last_tactic = pp; dblist = s.dblist;
+ localdb = List.tl s.localdb;
+ prev = ps; local_lemmas = s.local_lemmas}) l
in
let intro_tac =
let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in
- List.map
- (fun (lgls, cost, pp) ->
- let g' = first_goal lgls in
- let hintl =
- make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
- in
+ List.map
+ (fun (lgls, cost, pp) ->
+ let g' = first_goal lgls in
+ let hintl =
+ make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+ in
let ldb = Hint_db.add_list (pf_env g') (project g')
- hintl (List.hd s.localdb) in
- { depth = s.depth; priority = cost; tacres = lgls;
- last_tactic = pp; dblist = s.dblist;
- localdb = ldb :: List.tl s.localdb; prev = ps;
+ hintl (List.hd s.localdb) in
+ { depth = s.depth; priority = cost; tacres = lgls;
+ last_tactic = pp; dblist = s.dblist;
+ localdb = ldb :: List.tl s.localdb; prev = ps;
local_lemmas = s.local_lemmas})
- l
+ l
in
let rec_tacs =
- let l =
+ let l =
let concl = Reductionops.nf_evar (project g) (pf_concl g) in
- filter_tactics s.tacres
+ filter_tactics s.tacres
(e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl)
- in
- List.map
- (fun (lgls, cost, pp) ->
- let nbgl' = List.length (sig_it lgls) in
- if nbgl' < nbgl then
- { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp;
+ in
+ List.map
+ (fun (lgls, cost, pp) ->
+ let nbgl' = List.length (sig_it lgls) in
+ if nbgl' < nbgl then
+ { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp;
prev = ps; dblist = s.dblist; localdb = List.tl s.localdb;
local_lemmas = s.local_lemmas }
- else
- let newlocal =
- let hyps = pf_hyps g in
- List.map (fun gl ->
- let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
- let hyps' = pf_hyps gls in
- if hyps' == hyps then List.hd s.localdb
+ else
+ let newlocal =
+ let hyps = pf_hyps g in
+ List.map (fun gl ->
+ let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
+ let hyps' = pf_hyps gls in
+ if hyps' == hyps then List.hd s.localdb
else make_local_hint_db (pf_env gls) (project gls) ~ts:TransparentState.full true s.local_lemmas)
- (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
- in
- { depth = pred s.depth; priority = cost; tacres = lgls;
- dblist = s.dblist; last_tactic = pp; prev = ps;
- localdb = newlocal @ List.tl s.localdb;
+ (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
+ in
+ { depth = pred s.depth; priority = cost; tacres = lgls;
+ dblist = s.dblist; last_tactic = pp; prev = ps;
+ localdb = newlocal @ List.tl s.localdb;
local_lemmas = s.local_lemmas })
- l
+ l
in
List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
let pp s = hov 0 (str " depth=" ++ int s.depth ++ spc () ++
- (Lazy.force s.last_tactic))
+ (Lazy.force s.last_tactic))
end
@@ -361,12 +361,12 @@ let pr_info dbg s =
else
let rec loop s =
match s.prev with
- | Unknown | Init -> s.depth
- | State sp ->
- let mindepth = loop sp in
- let indent = String.make (mindepth - sp.depth) ' ' in
+ | Unknown | Init -> s.depth
+ | State sp ->
+ let mindepth = loop sp in
+ let indent = String.make (mindepth - sp.depth) ' ' in
Feedback.msg_notice (str indent ++ Lazy.force s.last_tactic ++ str ".");
- mindepth
+ mindepth
in
ignore (loop s)
@@ -430,15 +430,15 @@ let make_dimension n = function
let cons a l = a :: l
let autounfolds db occs cls gl =
- let unfolds = List.concat (List.map (fun dbname ->
- let db = try searchtable_map dbname
+ let unfolds = List.concat (List.map (fun dbname ->
+ let db = try searchtable_map dbname
with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname)
in
let (ids, csts) = Hint_db.unfolds db in
let hyps = pf_ids_of_hyps gl in
let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in
Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
- (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
+ (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
in Proofview.V82.of_tactic (unfold_option unfolds cls) gl
let autounfold db cls =
@@ -461,36 +461,36 @@ let autounfold_tac db cls =
autounfold dbs cls
let unfold_head env sigma (ids, csts) c =
- let rec aux c =
+ let rec aux c =
match EConstr.kind sigma c with
| Var id when Id.Set.mem id ids ->
- (match Environ.named_body id env with
- | Some b -> true, EConstr.of_constr b
- | None -> false, c)
+ (match Environ.named_body id env with
+ | Some b -> true, EConstr.of_constr b
+ | None -> false, c)
| Const (cst, u) when Cset.mem cst csts ->
let u = EInstance.kind sigma u in
- true, EConstr.of_constr (Environ.constant_value_in env (cst, u))
+ true, EConstr.of_constr (Environ.constant_value_in env (cst, u))
| App (f, args) ->
- (match aux f with
- | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
- | false, _ ->
- let done_, args' =
- Array.fold_left_i (fun i (done_, acc) arg ->
- if done_ then done_, arg :: acc
- else match aux arg with
- | true, arg' -> true, arg' :: acc
- | false, arg' -> false, arg :: acc)
- (false, []) args
- in
- if done_ then true, mkApp (f, Array.of_list (List.rev args'))
- else false, c)
- | _ ->
- let done_ = ref false in
- let c' = EConstr.map sigma (fun c ->
- if !done_ then c else
- let x, c' = aux c in
- done_ := x; c') c
- in !done_, c'
+ (match aux f with
+ | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
+ | false, _ ->
+ let done_, args' =
+ Array.fold_left_i (fun i (done_, acc) arg ->
+ if done_ then done_, arg :: acc
+ else match aux arg with
+ | true, arg' -> true, arg' :: acc
+ | false, arg' -> false, arg :: acc)
+ (false, []) args
+ in
+ if done_ then true, mkApp (f, Array.of_list (List.rev args'))
+ else false, c)
+ | _ ->
+ let done_ = ref false in
+ let c' = EConstr.map sigma (fun c ->
+ if !done_ then c else
+ let x, c' = aux c in
+ done_ := x; c') c
+ in !done_, c'
in aux c
let autounfold_one db cl =
@@ -499,15 +499,15 @@ let autounfold_one db cl =
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
let st =
- List.fold_left (fun (i,c) dbname ->
- let db = try searchtable_map dbname
- with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname)
+ List.fold_left (fun (i,c) dbname ->
+ let db = try searchtable_map dbname
+ with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname)
in
let (ids, csts) = Hint_db.unfolds db in
- (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
+ (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
in
- let did, c' = unfold_head env sigma st
- (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl)
+ let did, c' = unfold_head env sigma st
+ (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl)
in
if did then
match cl with
diff --git a/tactics/elim.ml b/tactics/elim.ml
index fcc2a94ef5..ea61b8e4df 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -66,8 +66,8 @@ and general_decompose_aux recognizer id =
elimHypThen
(introElimAssumsThen
(fun bas ->
- tclTHEN (clear [id])
- (tclMAP (general_decompose_on_hyp recognizer)
+ tclTHEN (clear [id])
+ (tclMAP (general_decompose_on_hyp recognizer)
(ids_of_named_context bas.Tacticals.assums))))
id
@@ -88,7 +88,7 @@ let general_decompose recognizer c =
[ tclTHEN (intro_using tmphyp_name)
(onLastHypId
(ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma))
- (fun id -> clear [id])));
+ (fun id -> clear [id])));
exact_no_check c ]
end
@@ -136,22 +136,22 @@ let induction_trailer abs_i abs_j bargs =
(onLastHypId
(fun id ->
Proofview.Goal.enter begin fun gl ->
- let idty = pf_unsafe_type_of gl (mkVar id) in
- let fvty = global_vars (pf_env gl) (project gl) idty in
- let possible_bring_hyps =
- (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
+ let idty = pf_unsafe_type_of gl (mkVar id) in
+ let fvty = global_vars (pf_env gl) (project gl) idty in
+ let possible_bring_hyps =
+ (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
in
- let (hyps,_) =
+ let (hyps,_) =
List.fold_left
- (fun (bring_ids,leave_ids) d ->
+ (fun (bring_ids,leave_ids) d ->
let cid = NamedDecl.get_id d in
if not (List.mem cid leave_ids)
then (d::bring_ids,leave_ids)
else (bring_ids,cid::leave_ids))
- ([],fvty) possible_bring_hyps
- in
+ ([],fvty) possible_bring_hyps
+ in
let ids = List.rev (ids_of_named_context hyps) in
- (tclTHENLIST
+ (tclTHENLIST
[revert ids; simple_elimination (mkVar id)])
end
))
@@ -167,7 +167,7 @@ let double_ind h1 h2 =
abs >>= fun (abs_i,abs_j) ->
(tclTHEN (tclDO abs_i intro)
(onLastHypId
- (fun id ->
+ (fun id ->
elimination_then
(introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
end
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 9cd2e7b52c..51f01888aa 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -38,12 +38,12 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
let (mib,mip) = Global.lookup_inductive ind in
let npars =
(* if a constructor of [ind] contains a recursive call, the scheme
- is generalized only wrt recursively uniform parameters *)
+ is generalized only wrt recursively uniform parameters *)
if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs)
then
- mib.mind_nparams_rec
+ mib.mind_nparams_rec
else
- mib.mind_nparams in
+ mib.mind_nparams in
let sigma, sort = Evd.fresh_sort_in_family sigma sort in
let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
let sigma = Evd.minimize_universes sigma in
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 11dbbc7155..093a4c456b 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -12,7 +12,7 @@ open Ind_tables
(** Induction/recursion schemes *)
-val optimize_non_type_induction_scheme :
+val optimize_non_type_induction_scheme :
'a Ind_tables.scheme_kind ->
Indrec.dep_flag ->
Sorts.family ->
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index e8782aa674..1df56be0be 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -42,7 +42,7 @@
One may wonder whether these extensions are worth to be done
regarding the price we have to pay and regarding the rare
- situations where they are needed. However, I believe it meets a
+ situations where they are needed. However, I believe it meets a
natural expectation of the user.
*)
@@ -69,7 +69,7 @@ let hid = Id.of_string "H"
let xid = Id.of_string "X"
let default_id_of_sort = function InSProp | InProp | InSet -> hid | InType -> xid
let fresh env id = next_global_ident_away id Id.Set.empty
-let with_context_set ctx (b, ctx') =
+let with_context_set ctx (b, ctx') =
(b, Univ.ContextSet.union ctx ctx')
let build_dependent_inductive ind (mib,mip) =
@@ -88,7 +88,7 @@ let name_context env hyps =
snd
(List.fold_left
(fun (env,hyps) d ->
- let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+ let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
(env,[]) (List.rev hyps))
let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
@@ -102,7 +102,7 @@ let get_coq_eq ctx =
try
let eq = Globnames.destIndRef (Coqlib.lib_ref "core.eq.type") in
(* Do not force the lazy if they are not defined *)
- let eq, ctx = with_context_set ctx
+ let eq, ctx = with_context_set ctx
(UnivGen.fresh_inductive_instance (Global.env ()) eq) in
mkIndU eq, mkConstructUi (eq,1), ctx
with Not_found ->
@@ -211,16 +211,16 @@ let build_sym_scheme env ind =
name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
let rci = Sorts.Relevant in (* TODO relevance *)
let ci = make_case_info (Global.env()) ind rci RegularStyle in
- let c =
+ let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign_ind
(mkCase (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (nrealargs+1) realsign_ind)
(mkApp (mkIndU indu,Array.concat
- [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
- rel_vect 1 nrealargs;
- rel_vect (2*nrealargs+2) nrealargs])),
+ [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
+ rel_vect 1 nrealargs;
+ rel_vect (2*nrealargs+2) nrealargs])),
mkRel 1 (* varH *),
[|cstr (nrealargs+1)|]))))
in c, UState.of_context_set ctx
@@ -247,9 +247,9 @@ let sym_scheme_kind =
(* *)
(**********************************************************************)
-let const_of_scheme kind env ind ctx =
+let const_of_scheme kind env ind ctx =
let sym_scheme, eff = (find_scheme kind ind) in
- let sym, ctx = with_context_set ctx
+ let sym, ctx = with_context_set ctx
(UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
mkConstU sym, ctx, eff
@@ -273,30 +273,30 @@ let build_sym_involutive_scheme env ind =
name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
let rci = Sorts.Relevant in (* TODO relevance *)
let ci = make_case_info (Global.env()) ind rci RegularStyle in
- let c =
+ let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign_ind
(mkCase (ci,
- my_it_mkLambda_or_LetIn_name
- (lift_rel_context (nrealargs+1) realsign_ind)
- (mkApp (eq,[|
- mkApp
- (mkIndU indu, Array.concat
- [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
- rel_vect (2*nrealargs+2) nrealargs;
- rel_vect 1 nrealargs]);
+ my_it_mkLambda_or_LetIn_name
+ (lift_rel_context (nrealargs+1) realsign_ind)
+ (mkApp (eq,[|
+ mkApp
+ (mkIndU indu, Array.concat
+ [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
+ rel_vect (2*nrealargs+2) nrealargs;
+ rel_vect 1 nrealargs]);
mkApp (sym,Array.concat
- [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
- rel_vect 1 nrealargs;
- rel_vect (2*nrealargs+2) nrealargs;
- [|mkApp (sym,Array.concat
- [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
- rel_vect (2*nrealargs+2) nrealargs;
- rel_vect 1 nrealargs;
- [|mkRel 1|]])|]]);
- mkRel 1|])),
- mkRel 1 (* varH *),
- [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
+ [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
+ rel_vect 1 nrealargs;
+ rel_vect (2*nrealargs+2) nrealargs;
+ [|mkApp (sym,Array.concat
+ [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
+ rel_vect (2*nrealargs+2) nrealargs;
+ rel_vect 1 nrealargs;
+ [|mkRel 1|]])|]]);
+ mkRel 1|])),
+ mkRel 1 (* varH *),
+ [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
in (c, UState.of_context_set ctx), eff
let sym_involutive_scheme_kind =
@@ -405,7 +405,7 @@ let build_l2r_rew_scheme dep env ind kind =
Array.concat [Context.Rel.to_extended_vect mkRel (nrealargs*3+4) paramsctxt1;
rel_vect (nrealargs+4) nrealargs;
rel_vect 1 nrealargs;
- [|mkRel 1|]]) in
+ [|mkRel 1|]]) in
let s, ctx' = UnivGen.fresh_sort_in_family kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
@@ -423,20 +423,20 @@ let build_l2r_rew_scheme dep env ind kind =
(if dep then [|mkRel 2|] else [||])) in
let applied_sym_sym =
mkApp (sym,Array.concat
- [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1;
+ [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1;
rel_vect 4 nrealargs;
rel_vect (nrealargs+4) nrealargs;
[|mkApp (sym,Array.concat
- [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1;
- rel_vect (nrealargs+4) nrealargs;
- rel_vect 4 nrealargs;
- [|mkRel 2|]])|]]) in
+ [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1;
+ rel_vect (nrealargs+4) nrealargs;
+ rel_vect 4 nrealargs;
+ [|mkRel 2|]])|]]) in
let main_body =
mkCase (ci,
my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
applied_sym_C 3,
[|mkVar varHC|]) in
- let c =
+ let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign
(mkNamedLambda (make_annot varP indr)
@@ -525,11 +525,11 @@ let build_l2r_forward_rew_scheme dep env ind kind =
mkApp (mkVar varP,Array.append
(rel_vect (nrealargs+2) nrealargs)
(if dep then [|cstr (2*nrealargs+2) (nrealargs+2)|]
- else [||])) in
+ else [||])) in
let applied_PG =
mkApp (mkVar varP,Array.append (rel_vect 3 nrealargs)
(if dep then [|cstr (3*nrealargs+4) 3|] else [||])) in
- let c =
+ let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign
(mkNamedLambda (make_annot varH indr) applied_ind
@@ -538,14 +538,14 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(lift_rel_context (nrealargs+1) realsign_ind)
(mkNamedProd (make_annot varP indr)
(my_it_mkProd_or_LetIn
- (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s)
+ (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s)
(mkNamedProd (make_annot varHC indr) applied_PC applied_PG)),
(mkVar varH),
[|mkNamedLambda (make_annot varP indr)
(my_it_mkProd_or_LetIn
- (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
+ (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
(mkNamedLambda (make_annot varHC indr) applied_PC'
- (mkVar varHC))|])))))
+ (mkVar varHC))|])))))
in c, UState.of_context_set ctx
(**********************************************************************)
@@ -578,7 +578,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(* statement but no need for symmetry of the equality. *)
(**********************************************************************)
-let build_r2l_forward_rew_scheme dep env ind kind =
+let build_r2l_forward_rew_scheme dep env ind kind =
let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
get_non_sym_eq_data env indu in
@@ -603,8 +603,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
let applied_PG =
mkApp (mkVar varP,
if dep then Context.Rel.to_extended_vect mkRel 0 realsign_ind
- else Context.Rel.to_extended_vect mkRel 1 realsign) in
- let c =
+ else Context.Rel.to_extended_vect mkRel 1 realsign) in
+ let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign_ind
(mkNamedLambda (make_annot varP indr)
@@ -619,8 +619,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
mkRel 3 (* varH *),
[|mkLambda
(make_annot (Name varHC) indr,
- lift (nrealargs+3) applied_PC,
- mkRel 1)|]),
+ lift (nrealargs+3) applied_PC,
+ mkRel 1)|]),
[|mkVar varHC|]))))))
in c, UState.of_context_set ctx
@@ -648,14 +648,14 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
let ctx,_ = decompose_prod_assum t in
match ctx with
| hp :: p :: ind :: indargs ->
- let c' =
+ let c' =
my_it_mkLambda_or_LetIn indargs
(mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
- (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
- (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
+ (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
+ (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
(EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma
- (EConstr.of_constr (applist (c,
- Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
+ (EConstr.of_constr (applist (c,
+ Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
in c', ctx'
| _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme.")
@@ -679,7 +679,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
(* (H:I q1..qm a1..an), *)
(* P b1..bn C -> P a1..an H *)
(**********************************************************************)
-
+
let build_r2l_rew_scheme dep env ind k =
let sigma = Evd.from_env env in
let (sigma, indu) = Evd.fresh_inductive_instance env sigma ind in
@@ -772,7 +772,7 @@ let rew_r2l_scheme_kind =
(* TODO: extend it to types with more than one index *)
let build_congr env (eq,refl,ctx) ind =
- let (ind,u as indu), ctx = with_context_set ctx
+ let (ind,u as indu), ctx = with_context_set ctx
(UnivGen.fresh_inductive_instance env ind) in
let (mib,mip) = lookup_mind_specif env ind in
if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then
@@ -802,7 +802,7 @@ let build_congr env (eq,refl,ctx) ind =
let ci = make_case_info (Global.env()) ind rci RegularStyle in
let uni, ctx = Univ.extend_in_context_set (UnivGen.new_global_univ ()) ctx in
let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
- let c =
+ let c =
my_it_mkLambda_or_LetIn paramsctxt
(mkNamedLambda (make_annot varB Sorts.Relevant) (mkType uni)
(mkNamedLambda (make_annot varf Sorts.Relevant) (mkArrow (lift 1 ty) tyr (mkVar varB))
@@ -810,26 +810,26 @@ let build_congr env (eq,refl,ctx) ind =
(mkNamedLambda (make_annot varH Sorts.Relevant)
(applist
(mkIndU indu,
- Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @
- Context.Rel.to_extended_list mkRel 0 realsign))
+ Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @
+ Context.Rel.to_extended_list mkRel 0 realsign))
(mkCase (ci,
my_it_mkLambda_or_LetIn_name
- (lift_rel_context (mip.mind_nrealargs+3) realsign)
+ (lift_rel_context (mip.mind_nrealargs+3) realsign)
(mkLambda
(make_annot Anonymous Sorts.Relevant,
applist
(mkIndU indu,
- Context.Rel.to_extended_list mkRel (2*mip.mind_nrealdecls+3)
- paramsctxt
- @ Context.Rel.to_extended_list mkRel 0 realsign),
+ Context.Rel.to_extended_list mkRel (2*mip.mind_nrealdecls+3)
+ paramsctxt
+ @ Context.Rel.to_extended_list mkRel 0 realsign),
mkApp (eq,
- [|mkVar varB;
+ [|mkVar varB;
mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
- mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
+ mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
mkVar varH,
[|mkApp (refl,
[|mkVar varB;
- mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|]))))))
+ mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|]))))))
in c, UState.of_context_set ctx
let congr_scheme_kind = declare_individual_scheme_object "_congr"
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index b3e10013ac..fd4221f7c0 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -24,9 +24,9 @@ val rew_l2r_forward_dep_scheme_kind : individual scheme_kind
val rew_r2l_dep_scheme_kind : individual scheme_kind
val rew_r2l_scheme_kind : individual scheme_kind
-val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family ->
+val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family ->
constr Evd.in_evar_universe_context
-val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family ->
+val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family ->
constr Evd.in_evar_universe_context * Evd.side_effects
val build_r2l_forward_rew_scheme :
bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
@@ -38,12 +38,12 @@ val build_l2r_forward_rew_scheme :
val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context
val sym_scheme_kind : individual scheme_kind
-val build_sym_involutive_scheme : env -> inductive ->
+val build_sym_involutive_scheme : env -> inductive ->
constr Evd.in_evar_universe_context * Evd.side_effects
val sym_involutive_scheme_kind : individual scheme_kind
(** Builds a congruence scheme for an equality type *)
val congr_scheme_kind : individual scheme_kind
-val build_congr : env -> constr * constr * Univ.ContextSet.t -> inductive ->
+val build_congr : env -> constr * constr * Univ.ContextSet.t -> inductive ->
constr Evd.in_evar_universe_context
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1f125a3c59..fc37d5a254 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -241,7 +241,7 @@ let rewrite_keyed_unif_flags = {
let rewrite_elim with_evars frzevars cls c e =
Proofview.Goal.enter begin fun gl ->
let flags = if Unification.is_keyed_unification ()
- then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in
+ then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in
let flags = make_flags frzevars (Tacmach.New.project gl) flags c in
general_elim_clause with_evars flags cls c e
end
@@ -366,7 +366,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
then
let sort = elimination_sort_of_clause cls gl in
let c =
- match EConstr.kind sigma hdcncl with
+ match EConstr.kind sigma hdcncl with
| Ind (ind_sp,u) ->
begin match lft2rgt, cls with
| Some true, None
@@ -381,19 +381,19 @@ let find_elim hdcncl lft2rgt dep cls ot =
try
let _ = Global.lookup_constant c1' in c1'
with Not_found ->
- user_err ~hdr:"Equality.find_elim"
+ user_err ~hdr:"Equality.find_elim"
(str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
- end
+ end
| _ ->
begin match if is_eq then eq_elimination_ref false sort else None with
| Some r -> destConstRef r
| None -> destConstRef (lookup_eliminator env ind_sp sort)
end
end
- | _ ->
- (* cannot occur since we checked that we are in presence of
- Logic.eq or Jmeq just before *)
- assert false
+ | _ ->
+ (* cannot occur since we checked that we are in presence of
+ Logic.eq or Jmeq just before *)
+ assert false
in
pf_constr_of_global (GlobRef.ConstRef c)
else
@@ -410,9 +410,9 @@ let find_elim hdcncl lft2rgt dep cls ot =
| true, _, false -> rew_r2l_forward_dep_scheme_kind
in
match EConstr.kind sigma hdcncl with
- | Ind (ind,u) ->
-
- let c, eff = find_scheme scheme_name ind in
+ | Ind (ind,u) ->
+
+ let c, eff = find_scheme scheme_name ind in
Proofview.tclEFFECTS eff <*>
pf_constr_of_global (GlobRef.ConstRef c)
| _ -> assert false
@@ -463,27 +463,27 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in
match match_with_equality_type env sigma t with
| Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
- let lft2rgt = adjust_rewriting_direction args lft2rgt in
+ let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
- l with_evars frzevars dep_proof_ok hdcncl
+ l with_evars frzevars dep_proof_ok hdcncl
| None ->
- Proofview.tclORELSE
+ Proofview.tclORELSE
begin
- rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls
- lft2rgt occs (c,l) ~new_goals:[]) tac
+ rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls
+ lft2rgt occs (c,l) ~new_goals:[]) tac
end
begin function
| (e, info) ->
Proofview.tclEVARMAP >>= fun sigma ->
- let env' = push_rel_context rels env in
- let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
+ let env' = push_rel_context rels env in
+ let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
match match_with_equality_type env sigma t' with
- | Some (hdcncl,args) ->
- let lft2rgt = adjust_rewriting_direction args lft2rgt in
- leibniz_rewrite_ebindings_clause cls lft2rgt tac c
- (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl
- | None -> Proofview.tclZERO ~info e
- (* error "The provided term does not end with an equality or a declared rewrite relation." *)
+ | Some (hdcncl,args) ->
+ let lft2rgt = adjust_rewriting_direction args lft2rgt in
+ leibniz_rewrite_ebindings_clause cls lft2rgt tac c
+ (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl
+ | None -> Proofview.tclZERO ~info e
+ (* error "The provided term does not end with an equality or a declared rewrite relation." *)
end
end
@@ -517,44 +517,44 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
in
match cl.onhyps with
| Some l ->
- (* If a precise list of locations is given, success is mandatory for
- each of these locations. *)
- let rec do_hyps = function
- | [] -> Proofview.tclUNIT ()
- | ((occs,id),_) :: l ->
- tclTHENFIRST
- (general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars)
- (do_hyps l)
- in
- if cl.concl_occs == NoOccurrences then do_hyps l else
- tclTHENFIRST
- (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
+ (* If a precise list of locations is given, success is mandatory for
+ each of these locations. *)
+ let rec do_hyps = function
+ | [] -> Proofview.tclUNIT ()
+ | ((occs,id),_) :: l ->
+ tclTHENFIRST
+ (general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars)
+ (do_hyps l)
+ in
+ if cl.concl_occs == NoOccurrences then do_hyps l else
+ tclTHENFIRST
+ (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
(do_hyps l)
| None ->
- (* Otherwise, if we are told to rewrite in all hypothesis via the
+ (* Otherwise, if we are told to rewrite in all hypothesis via the
syntax "* |-", we fail iff all the different rewrites fail *)
- let rec do_hyps_atleastonce = function
- | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.")
- | id :: l ->
+ let rec do_hyps_atleastonce = function
+ | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.")
+ | id :: l ->
tclIFTHENFIRSTTRYELSEMUST
- (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars)
- (do_hyps_atleastonce l)
- in
- let do_hyps =
- (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
- let ids gl =
- let ids_in_c = Termops.global_vars_set (Proofview.Goal.env gl) (project gl) (fst c) in
+ (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars)
+ (do_hyps_atleastonce l)
+ in
+ let do_hyps =
+ (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
+ let ids gl =
+ let ids_in_c = Termops.global_vars_set (Proofview.Goal.env gl) (project gl) (fst c) in
let ids_of_hyps = pf_ids_of_hyps gl in
- Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
- in
+ Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
+ in
Proofview.Goal.enter begin fun gl ->
do_hyps_atleastonce (ids gl)
end
- in
- if cl.concl_occs == NoOccurrences then do_hyps else
+ in
+ if cl.concl_occs == NoOccurrences then do_hyps else
tclIFTHENFIRSTTRYELSEMUST
- (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
- do_hyps
+ (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
+ do_hyps
let apply_special_clear_request clear_flag f =
Proofview.Goal.enter begin fun gl ->
@@ -615,9 +615,9 @@ let check_setoid cl =
let concloccs = Locusops.occurrences_map (fun x -> x) cl.concl_occs in
Option.fold_left
(List.fold_left
- (fun b ((occ,_),_) ->
+ (fun b ((occ,_),_) ->
b||(not (Locusops.is_all_occurrences (Locusops.occurrences_map (fun x -> x) occ)))
- )
+ )
)
(not (Locusops.is_all_occurrences concloccs) &&
(concloccs <> NoOccurrences))
@@ -631,7 +631,7 @@ let replace_core clause l2r eq =
(onLastHypId (fun id ->
tclTHEN
(tclTRY (general_rewrite_clause l2r false (mkVar id,NoBindings) clause))
- (clear [id])))
+ (clear [id])))
(* eq,sym_eq : equality on Type and its symmetry theorem
c1 c2 : c1 is to be replaced by c2
@@ -649,7 +649,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
let get_type_of = pf_apply get_type_of gl in
let t1 = get_type_of c1
and t2 = get_type_of c2 in
- let evd =
+ let evd =
if unsafe then Some (Tacmach.New.project gl)
else
try Some (Evarconv.unify_delay (Proofview.Goal.env gl) (Tacmach.New.project gl) t1 t2)
@@ -760,37 +760,37 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
| Construct ((ind1,i1 as sp1),u1), Construct (sp2,_)
when Int.equal (List.length args1) (constructor_nallargs env sp1)
->
- let sorts' =
+ let sorts' =
CList.intersect Sorts.family_equal sorts (sorts_below (top_allowed_sort env (fst sp1)))
in
(* both sides are fully applied constructors, so either we descend,
or we can discriminate here. *)
- if eq_constructor sp1 sp2 then
+ if eq_constructor sp1 sp2 then
let nparams = inductive_nparams env ind1 in
- let params1,rargs1 = List.chop nparams args1 in
- let _,rargs2 = List.chop nparams args2 in
+ let params1,rargs1 = List.chop nparams args1 in
+ let _,rargs2 = List.chop nparams args2 in
let (mib,mip) = lookup_mind_specif env ind1 in
let params1 = List.map EConstr.Unsafe.to_constr params1 in
let u1 = EInstance.kind sigma u1 in
let ctxt = (get_constructor ((ind1,u1),mib,mip,params1) i1).cs_args in
let adjust i = CVars.adjust_rel_to_rel_context ctxt (i+1) - 1 in
List.flatten
- (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
- 0 rargs1 rargs2)
+ (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
+ 0 rargs1 rargs2)
else if List.mem_f Sorts.family_equal InType sorts' && not no_discr
then (* see build_discriminator *)
- raise (DiscrFound (List.rev posn,sp1,sp2))
- else
+ raise (DiscrFound (List.rev posn,sp1,sp2))
+ else
(* if we cannot eliminate to Type, we cannot discriminate but we
- may still try to project *)
- project env sorts posn (applist (hd1,args1)) (applist (hd2,args2))
+ may still try to project *)
+ project env sorts posn (applist (hd1,args1)) (applist (hd2,args2))
| _ ->
- let t1_0 = applist (hd1,args1)
+ let t1_0 = applist (hd1,args1)
and t2_0 = applist (hd2,args2) in
if is_conv env sigma t1_0 t2_0 then
- []
+ []
else
- project env sorts posn t1_0 t2_0
+ project env sorts posn t1_0 t2_0
in
try
let sorts = if keep_proofs then [InSet;InType;InProp] else [InSet;InType] in
@@ -881,7 +881,7 @@ let descend_then env sigma head dirn =
let IndType (indf,_) =
try find_rectype env sigma (get_type_of env sigma head)
with Not_found ->
- user_err Pp.(str "Cannot project on an inductive type derived from a dependency.")
+ user_err Pp.(str "Cannot project on an inductive type derived from a dependency.")
in
let indp,_ = (dest_ind_family indf) in
let ind, _ = check_privacy env indp in
@@ -894,12 +894,12 @@ let descend_then env sigma head dirn =
(fun sigma dirnval (dfltval,resty) ->
let deparsign = make_arity_signature env sigma true indf in
let p =
- it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
+ it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
let build_branch i =
- let result = if Int.equal i dirn then dirnval else dfltval in
- let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.(i-1).cs_args in
- let args = name_context env sigma cs_args in
- it_mkLambda_or_LetIn result args in
+ let result = if Int.equal i dirn then dirnval else dfltval in
+ let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.(i-1).cs_args in
+ let args = name_context env sigma cs_args in
+ it_mkLambda_or_LetIn result args in
let brl =
List.map build_branch
(List.interval 1 (Array.length mip.mind_consnames)) in
@@ -934,8 +934,8 @@ let build_selector env sigma dirn c ind special default =
CP : changed assert false in a more informative error
*)
user_err ~hdr:"Equality.construct_discriminator"
- (str "Cannot discriminate on inductive constructors with \
- dependent types.") in
+ (str "Cannot discriminate on inductive constructors with \
+ dependent types.") in
let (indp,_) = dest_ind_family indf in
let ind, _ = check_privacy env indp in
let typ = Retyping.get_type_of env sigma default in
@@ -1055,9 +1055,9 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let env = Proofview.Goal.env gl in
match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
| Inr _ ->
- tclZEROMSG (str"Not a discriminable equality.")
+ tclZEROMSG (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
- discr_positions env sigma u eq_clause cpath dirn
+ discr_positions env sigma u eq_clause cpath dirn
end
let onEquality with_evars tac (c,lbindc) =
@@ -1216,17 +1216,17 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
sigma, dflt
with Evarconv.UnableToUnify _ ->
- user_err Pp.(str "Cannot solve a unification problem.")
+ user_err Pp.(str "Cannot solve a unification problem.")
else
let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with
- | (_sigS,[a;p]) -> (a, p)
- | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
+ | (_sigS,[a;p]) -> (a, p)
+ | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
let sigma, ev = Evarutil.new_evar env sigma a in
let rty = beta_applist sigma (p_i_minus_1,[ev]) in
let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in
let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in
match evopt with
- | Some w ->
+ | Some w ->
let w_type = unsafe_type_of env sigma w in
begin match Evarconv.unify_leq_delay env sigma w_type a with
| sigma ->
@@ -1235,14 +1235,14 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
| exception Evarconv.UnableToUnify _ ->
user_err Pp.(str "Cannot solve a unification problem.")
end
- | None ->
+ | None ->
(* This at least happens if what has been detected as a
dependency is not one; use an evasive error message;
even if the problem is upwards: unification should be
tried in the first place in make_iterated_tuple instead
of approximatively computing the free rels; then
unsolved evars would mean not binding rel *)
- user_err Pp.(str "Cannot solve a unification problem.")
+ user_err Pp.(str "Cannot solve a unification problem.")
in
let sigma = Evd.clear_metas sigma in
let sigma, scf = sigrec_clausal_form sigma siglen ty in
@@ -1328,7 +1328,7 @@ let rec build_injrec env sigma dflt c = function
let res = kont sigma subval (dfltval,tuplety) in
sigma, (res, tuplety,dfltval)
with
- UserError _ -> failwith "caught"
+ UserError _ -> failwith "caught"
let build_injector env sigma dflt c cpath =
let sigma, (injcode,resty,_) = build_injrec env sigma dflt c cpath in
@@ -1405,8 +1405,8 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
let pf = Clenvtac.clenv_value_cast_meta inj_clause in
let ty = simplify_args env sigma (clenv_type inj_clause) in
- evdref := sigma;
- Some (pf, ty)
+ evdref := sigma;
+ Some (pf, ty)
with Failure _ -> None
in
let injectors = List.map_filter filter posns in
@@ -1438,7 +1438,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
tclZEROMSG (str"Nothing to inject.")
| Inr posns ->
inject_at_positions env sigma l2r u eq_clause posns
- (tac (clenv_value eq_clause))
+ (tac (clenv_value eq_clause))
let get_previous_hyp_position id gl =
let env, sigma = Proofview.Goal.(env gl, sigma gl) in
@@ -1497,11 +1497,11 @@ let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause =
let env = Proofview.Goal.env gl in
match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with
| Inl (cpath, (_,dirn), _) ->
- discr_positions env sigma u clause cpath dirn
+ discr_positions env sigma u clause cpath dirn
| Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
ntac (clenv_value clause) 0
| Inr posns ->
- inject_at_positions env sigma true u clause posns
+ inject_at_positions env sigma true u clause posns
(ntac (clenv_value clause))
end
@@ -1636,9 +1636,9 @@ let cutSubstInHyp l2r eqn id =
let try_rewrite tac =
Proofview.tclORELSE tac begin function (e, info) -> match e with
| Constr_matching.PatternMatchingFailure ->
- tclZEROMSG (str "Not a primitive equality here.")
+ tclZEROMSG (str "Not a primitive equality here.")
| e when catchable_exception e ->
- tclZEROMSG
+ tclZEROMSG
(strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
| e -> Proofview.tclZERO ~info e
end
@@ -1766,7 +1766,7 @@ let subst_one_var dep_proof_ok x =
Context.Named.fold_outside test ~init:() hyps;
user_err ~hdr:"Subst"
(str "Cannot find any non-recursive equality over " ++ Id.print x ++
- str".")
+ str".")
with FoundHyp res -> res in
subst_one dep_proof_ok x res
end
@@ -1903,12 +1903,12 @@ let rewrite_assumption_cond cond_eq_term cl =
| [] -> user_err Pp.(str "No such assumption.")
| hyp ::rest ->
let id = NamedDecl.get_id hyp in
- begin
- try
+ begin
+ try
let dir = cond_eq_term (NamedDecl.get_type hyp) gl in
- general_rewrite_clause dir false (mkVar id,NoBindings) cl
- with | Failure _ | UserError _ -> arec rest gl
- end
+ general_rewrite_clause dir false (mkVar id,NoBindings) cl
+ with | Failure _ | UserError _ -> arec rest gl
+ end
in
Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 8225195ca7..a9ccadf53a 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -57,7 +57,7 @@ val general_rewrite_bindings_in :
?tac:(unit Proofview.tactic * conditions) ->
Id.t -> constr with_bindings -> evars_flag -> unit Proofview.tactic
val general_rewrite_in :
- orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
+ orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(unit Proofview.tactic * conditions) -> Id.t -> constr -> evars_flag -> unit Proofview.tactic
val general_rewrite_clause :
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ac18d5ce97..eb50a2a67c 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -253,9 +253,9 @@ type stored_data = int * full_hint
(* First component is the index of insertion in the table, to keep most recent first semantics. *)
module Bounded_net = Btermdn.Make(struct
- type t = stored_data
- let compare = pri_order_int
- end)
+ type t = stored_data
+ let compare = pri_order_int
+ end)
type search_entry = {
sentry_nopat : stored_data list;
@@ -275,18 +275,18 @@ let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid
let add_tac pat t st se =
match pat with
- | None ->
+ | None ->
if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se
else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat }
- | Some pat ->
+ | Some pat ->
if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se
else { se with
sentry_pat = List.insert pri_order t se.sentry_pat;
sentry_bnet = Bounded_net.add st se.sentry_bnet (pat, t); }
let rebuild_dn st se =
- let dn' =
- List.fold_left
+ let dn' =
+ List.fold_left
(fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
Bounded_net.empty se.sentry_pat
in
@@ -302,9 +302,9 @@ let is_transparent_gr ts = let open GlobRef in function
| ConstRef cst -> TransparentState.is_transparent_constant ts cst
| IndRef _ | ConstructRef _ -> false
-let strip_params env sigma c =
+let strip_params env sigma c =
match EConstr.kind sigma c with
- | App (f, args) ->
+ | App (f, args) ->
(match EConstr.kind sigma f with
| Const (cst,_) ->
(match Recordops.find_primitive_projection cst with
@@ -322,10 +322,10 @@ let strip_params env sigma c =
let instantiate_hint env sigma p =
let mk_clenv (c, cty, ctx) =
let sigma = Evd.merge_context_set univ_flexible sigma ctx in
- let cl = mk_clenv_from_env env sigma None (c,cty) in
- {cl with templval =
- { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
- env = empty_env}
+ let cl = mk_clenv_from_env env sigma None (c,cty) in
+ {cl with templval =
+ { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
+ env = empty_env}
in
let code = match p.code.obj with
| Res_pf c -> Res_pf (c, mk_clenv c)
@@ -359,11 +359,11 @@ let path_matches hp hints =
match hp, hints with
| PathAtom _, [] -> false
| PathAtom PathAny, (_ :: hints') -> k hints'
- | PathAtom p, (h :: hints') ->
+ | PathAtom p, (h :: hints') ->
if hints_path_atom_eq p h then k hints' else false
- | PathStar hp', hints ->
+ | PathStar hp', hints ->
k hints || aux hp' hints (fun hints' -> aux hp hints' k)
- | PathSeq (hp, hp'), hints ->
+ | PathSeq (hp, hp'), hints ->
aux hp hints (fun hints' -> aux hp' hints' k)
| PathOr (hp, hp'), hints ->
aux hp hints k || aux hp' hints k
@@ -392,7 +392,7 @@ let path_seq p p' =
| PathEpsilon, p' -> p'
| p, PathEpsilon -> p
| p, p' -> PathSeq (p, p')
-
+
let rec path_derivate hp hint =
let rec derivate_atoms hints hints' =
match hints, hints' with
@@ -404,7 +404,7 @@ let rec path_derivate hp hint =
in
match hp with
| PathAtom PathAny -> PathEpsilon
- | PathAtom (PathHints grs) ->
+ | PathAtom (PathHints grs) ->
(match grs, hint with
| h :: _, PathAny -> PathEmpty
| hints, PathHints hints' -> derivate_atoms hints hints'
@@ -412,9 +412,9 @@ let rec path_derivate hp hint =
| PathStar p -> if path_matches p [hint] then hp else PathEpsilon
| PathSeq (hp, hp') ->
let hpder = path_derivate hp hint in
- if matches_epsilon hp then
+ if matches_epsilon hp then
PathOr (path_seq hpder hp', path_derivate hp' hint)
- else if is_empty hpder then PathEmpty
+ else if is_empty hpder then PathEmpty
else path_seq hpder hp'
| PathOr (hp, hp') ->
PathOr (path_derivate hp hint, path_derivate hp' hint)
@@ -427,11 +427,11 @@ let rec normalize_path h =
| PathSeq (PathEmpty, _) | PathSeq (_, PathEmpty) -> PathEmpty
| PathSeq (PathEpsilon, p) | PathSeq (p, PathEpsilon) -> normalize_path p
| PathOr (PathEmpty, p) | PathOr (p, PathEmpty) -> normalize_path p
- | PathOr (p, q) ->
+ | PathOr (p, q) ->
let p', q' = normalize_path p, normalize_path q in
if hints_path_eq p p' && hints_path_eq q q' then h
else normalize_path (PathOr (p', q'))
- | PathSeq (p, q) ->
+ | PathSeq (p, q) ->
let p', q' = normalize_path p, normalize_path q in
if hints_path_eq p p' && hints_path_eq q q' then h
else normalize_path (PathSeq (p', q'))
@@ -450,13 +450,13 @@ let pp_hints_path_gen prg =
| PathStar (PathAtom PathAny) -> str"_*"
| PathStar p -> str "(" ++ aux p ++ str")*"
| PathSeq (p, p') -> aux p ++ spc () ++ aux p'
- | PathOr (p, p') ->
+ | PathOr (p, p') ->
str "(" ++ aux p ++ spc () ++ str"|" ++ cut () ++ spc () ++
aux p' ++ str ")"
| PathEmpty -> str"emp"
| PathEpsilon -> str"eps"
in aux
-
+
let pp_hints_path = pp_hints_path_gen pr_global
let glob_hints_path_atom p =
@@ -552,18 +552,18 @@ struct
{ db with hintdb_max_id = succ db.hintdb_max_id }, h
let empty ?name st use_dn = { hintdb_state = st;
- hintdb_cut = PathEmpty;
- hintdb_unfolds = (Id.Set.empty, Cset.empty);
- hintdb_max_id = 0;
- use_dn = use_dn;
+ hintdb_cut = PathEmpty;
+ hintdb_unfolds = (Id.Set.empty, Cset.empty);
+ hintdb_max_id = 0;
+ use_dn = use_dn;
hintdb_map = GlobRef.Map.empty;
- hintdb_nopat = [];
- hintdb_name = name; }
+ hintdb_nopat = [];
+ hintdb_name = name; }
let find key db =
try GlobRef.Map.find key db.hintdb_map
with Not_found -> empty_se
-
+
let realize_tac secvars (id,tac) =
if Id.Pred.subset tac.secvars secvars then Some tac
else
@@ -588,11 +588,11 @@ struct
(try ignore(head_evar sigma arg); false
with Evarutil.NoHeadEvar -> true)
| ModeOutput -> true
-
+
let matches_mode sigma args mode =
Array.length mode == Array.length args &&
Array.for_all2 (match_mode sigma) mode args
-
+
let matches_modes sigma args modes =
if List.is_empty modes then true
else List.exists (matches_mode sigma args) modes
@@ -609,7 +609,7 @@ struct
let map_all ~secvars k db =
let se = find k db in
merge_entry secvars db se.sentry_nopat se.sentry_pat
-
+
(* Precondition: concl has no existentials *)
let map_auto sigma ~secvars (k,args) concl db =
let se = find k db in
@@ -644,7 +644,7 @@ struct
let idv = id, { v with db = db.hintdb_name } in
let k = match gr with
| Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr &&
- is_unfold v.code.obj then None else Some gr
+ is_unfold v.code.obj then None else Some gr
| None -> None
in
let dnst = if db.use_dn then Some db.hintdb_state else None in
@@ -652,18 +652,18 @@ struct
match k with
| None ->
let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in
- if not (List.exists is_present db.hintdb_nopat) then
+ if not (List.exists is_present db.hintdb_nopat) then
(* FIXME *)
- { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
- else db
+ { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
+ else db
| Some gr ->
- let oval = find gr db in
+ let oval = find gr db in
{ db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
let rebuild_db st' db =
let db' =
{ db with hintdb_map = GlobRef.Map.map (rebuild_dn st') db.hintdb_map;
- hintdb_state = st'; hintdb_nopat = [] }
+ hintdb_state = st'; hintdb_nopat = [] }
in
List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat
@@ -674,14 +674,14 @@ struct
| Unfold_nth egr ->
let addunf ts (ids, csts) =
let open TransparentState in
- match egr with
+ match egr with
| EvalVarRef id ->
{ ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts)
| EvalConstRef cst ->
{ ts with tr_cst = Cpred.add cst ts.tr_cst }, (ids, Cset.add cst csts)
- in
- let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
- state, { db with hintdb_unfolds = unfs }, true
+ in
+ let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
+ state, { db with hintdb_unfolds = unfs }, true
| _ -> db.hintdb_state, db, false
in
let db = if db.use_dn && rebuild then rebuild_db st' db else db in
@@ -807,19 +807,19 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
| Prod _ -> failwith "make_exact_entry"
| _ ->
let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in
- let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_exact_entry"
- in
- let pri = match info.hint_priority with None -> 0 | Some p -> p in
- let pat = match info.hint_pattern with
- | Some pat -> snd pat
- | None -> pat
- in
+ let hd =
+ try head_pattern_bound pat
+ with BoundPattern -> failwith "make_exact_entry"
+ in
+ let pri = match info.hint_priority with None -> 0 | Some p -> p in
+ let pat = match info.hint_pattern with
+ | Some pat -> snd pat
+ | None -> pat
+ in
(Some hd,
- { pri; poly; pat = Some pat; name;
- db = None; secvars;
- code = with_uid (Give_exact (c, cty, ctx)); })
+ { pri; poly; pat = Some pat; name;
+ db = None; secvars;
+ code = with_uid (Give_exact (c, cty, ctx)); })
let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) =
let cty = if hnf then hnf_constr env sigma cty else cty in
@@ -912,7 +912,7 @@ let make_resolves env sigma flags info ~poly ?name cr =
user_err ~hdr:"Hint"
(pr_leconstr_env env sigma c ++ spc() ++
(if pi1 flags then str"cannot be used as a hint."
- else str "can be used as a hint only for eauto."));
+ else str "can be used as a hint only for eauto."));
ents
(* used to add an hypothesis to the local hint database *)
@@ -949,9 +949,9 @@ let make_extern pri pat tacast =
name = PathAny;
db = None;
secvars = Id.Pred.empty; (* Approximation *)
- code = with_uid (Extern tacast) })
+ code = with_uid (Extern tacast) })
-let make_mode ref m =
+let make_mode ref m =
let open Term in
let ty, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
let ctx, t = decompose_prod ty in
@@ -959,10 +959,10 @@ let make_mode ref m =
let m' = Array.of_list m in
if not (n == Array.length m') then
user_err ~hdr:"Hint"
- (pr_global ref ++ str" has " ++ int n ++
- str" arguments while the mode declares " ++ int (Array.length m'))
+ (pr_global ref ++ str" has " ++ int n ++
+ str" arguments while the mode declares " ++ int (Array.length m'))
else m'
-
+
let make_trivial env sigma poly ?(name=PathAny) r =
let c,ctx = fresh_global_or_constr env sigma poly r in
let sigma = Evd.merge_context_set univ_flexible sigma ctx in
@@ -970,9 +970,9 @@ let make_trivial env sigma poly ?(name=PathAny) r =
let hd = head_constr sigma t in
let ce = mk_clenv_from_env env sigma None (c,t) in
(Some hd, { pri=1;
- poly = poly;
+ poly = poly;
pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
- name = name;
+ name = name;
db = None;
secvars = secvars_of_constr env sigma c;
code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
@@ -1096,7 +1096,7 @@ let subst_autohint (subst, obj) =
if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx)
| Give_exact (c,t,ctx) ->
let c' = subst_mps subst c in
- let t' = subst_mps subst t in
+ let t' = subst_mps subst t in
if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx)
| Res_pf_THEN_trivial_fail (c,t,ctx) ->
let c' = subst_mps subst c in
@@ -1106,8 +1106,8 @@ let subst_autohint (subst, obj) =
let ref' = subst_evaluable_reference subst ref in
if ref==ref' then data.code.obj else Unfold_nth ref'
| Extern tac ->
- let tac' = Genintern.generic_substitute subst tac in
- if tac==tac' then data.code.obj else Extern tac'
+ let tac' = Genintern.generic_substitute subst tac in
+ if tac==tac' then data.code.obj else Extern tac'
in
let name' = subst_path_atom subst data.name in
let uid' = subst_kn subst data.code.uid in
@@ -1154,10 +1154,10 @@ let classify_autohint obj =
let inAutoHint : hint_obj -> obj =
declare_object {(default_object "AUTOHINT") with
cache_function = cache_autohint;
- load_function = load_autohint;
- open_function = open_autohint;
- subst_function = subst_autohint;
- classify_function = classify_autohint; }
+ load_function = load_autohint;
+ open_function = open_autohint;
+ subst_function = subst_autohint;
+ classify_function = classify_autohint; }
let make_hint ?(local = false) name action = {
hint_local = local;
@@ -1227,7 +1227,7 @@ let add_extern info tacast local dbname =
| Some (_, pat) -> Some pat
in
let hint = make_hint ~local dbname
- (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
+ (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
Lib.add_anonymous_leaf (inAutoHint hint)
let add_externs info tacast local dbnames =
@@ -1274,10 +1274,10 @@ let prepare_hint check env init (sigma,c) =
let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in
if not (closed0 sigma c) then
- user_err Pp.(str "Hints with holes dependent on a bound variable not supported.");
+ user_err Pp.(str "Hints with holes dependent on a bound variable not supported.");
if occur_existential sigma t then
- (* Not clever enough to construct dependency graph of evars *)
- user_err Pp.(str "Not clever enough to deal with evars dependent in other evars.");
+ (* Not clever enough to construct dependency graph of evars *)
+ user_err Pp.(str "Not clever enough to deal with evars dependent in other evars.");
raise (Found (c,t))
| _ -> EConstr.iter sigma find_next_evar c in
let rec iter c =
@@ -1350,7 +1350,7 @@ let interp_hints ~poly =
match c with
| HintsReference c ->
let gr = global_with_alias c in
- (PathHints [gr], poly, IsGlobRef gr)
+ (PathHints [gr], poly, IsGlobRef gr)
| HintsConstr c -> (PathAny, poly, f poly c)
in
let fp = Constrintern.intern_constr_pattern env sigma in
@@ -1376,14 +1376,14 @@ let interp_hints ~poly =
| HintsConstructors lqid ->
let constr_hints_of_ind qid =
let ind = global_inductive_with_alias qid in
- let mib,_ = Global.lookup_inductive ind in
+ let mib,_ = Global.lookup_inductive ind in
Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
List.init (nconstructors env ind)
- (fun i -> let c = (ind,i+1) in
+ (fun i -> let c = (ind,i+1) in
let gr = GlobRef.ConstructRef c in
- empty_hint_info,
+ empty_hint_info,
(Declareops.inductive_is_polymorphic mib), true,
- PathHints [gr], IsGlobRef gr)
+ PathHints [gr], IsGlobRef gr)
in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
| HintsExtern (pri, patcom, tacexp) ->
let pat = Option.map (fp sigma) patcom in
@@ -1415,11 +1415,11 @@ let expand_constructor_hints env sigma lems =
match EConstr.kind sigma lem with
| Ind (ind,u) ->
List.init (nconstructors env ind)
- (fun i ->
- let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd)
- (Evd.universe_context_set sigma) in
- not (Univ.ContextSet.is_empty ctx),
- IsConstr (mkConstructU ((ind,i+1),u),ctx))
+ (fun i ->
+ let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd)
+ (Evd.universe_context_set sigma) in
+ not (Univ.ContextSet.is_empty ctx),
+ IsConstr (mkConstructU ((ind,i+1),u),ctx))
| _ ->
let (c, ctx) = prepare_hint false env sigma (evd,lem) in
[not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx)]) lems
@@ -1436,7 +1436,7 @@ let make_local_hint_db env sigma ts eapply lems =
let lems = List.map map lems in
let sign = EConstr.named_context env in
let ts = match ts with
- | None -> Hint_db.transparent_state (searchtable_map "core")
+ | None -> Hint_db.transparent_state (searchtable_map "core")
| Some ts -> ts
in
let hintlist = List.map_append (make_resolve_hyp env sigma) sign in
@@ -1510,19 +1510,19 @@ let pr_hint_term env sigma cl =
let dbs = current_db () in
let valid_dbs =
let fn = try
- let hdc = decompose_app_bound sigma cl in
- if occur_existential sigma cl then
- Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl
- else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl
- with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
+ let hdc = decompose_app_bound sigma cl in
+ if occur_existential sigma cl then
+ Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl
+ else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl
+ with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
in
let fn db = List.map (fun x -> 0, x) (fn db) in
List.map (fun (name, db) -> (name, db, fn db)) dbs
in
if List.is_empty valid_dbs then
- (str "No hint applicable for current goal")
+ (str "No hint applicable for current goal")
else
- (str "Applicable Hints :" ++ fnl () ++
+ (str "Applicable Hints :" ++ fnl () ++
hov 0 (prlist (pr_hints_db env sigma) valid_dbs))
with Match_failure _ | Failure _ ->
(str "No hint applicable for current goal")
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 5b89f8b381..2a9b71387e 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -112,7 +112,7 @@ type 'a hints_path_gen =
type pre_hints_path = Libnames.qualid hints_path_gen
type hints_path = GlobRef.t hints_path_gen
-
+
val normalize_path : hints_path -> hints_path
val path_matches : hints_path -> hints_path_atom list -> bool
val path_derivate : hints_path -> hints_path_atom -> hints_path
@@ -139,17 +139,17 @@ module Hint_db :
(** All hints associated to the reference *)
val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
- (** All hints associated to the reference, respecting modes if evars appear in the
- arguments, _not_ using the discrimination net. *)
+ (** All hints associated to the reference, respecting modes if evars appear in the
+ arguments, _not_ using the discrimination net. *)
val map_existential : evar_map -> secvars:Id.Pred.t ->
(GlobRef.t * constr array) -> constr -> t -> full_hint list
- (** All hints associated to the reference, respecting modes if evars appear in the
- arguments and using the discrimination net. *)
+ (** All hints associated to the reference, respecting modes if evars appear in the
+ arguments and using the discrimination net. *)
val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list
- (** All hints associated to the reference, respecting modes if evars appear in the
- arguments. *)
+ (** All hints associated to the reference, respecting modes if evars appear in the
+ arguments. *)
val map_auto : evar_map -> secvars:Id.Pred.t ->
(GlobRef.t * constr array) -> constr -> t -> full_hint list
@@ -217,7 +217,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
(** [make_exact_entry info (c, ctyp, ctx)].
[c] is the term given as an exact proof to solve the goal;
[ctyp] is the type of [c].
- [ctx] is its (refreshable) universe context.
+ [ctx] is its (refreshable) universe context.
In info:
[hint_priority] is the hint's desired priority, it is 0 if unspecified
[hint_pattern] is the hint's desired pattern, it is inferred if not specified
@@ -232,7 +232,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> poly:bool -> ?name:hints_
products;
[c] is the term given as an exact proof to solve the goal;
[cty] is the type of [c].
- [ctx] is its (refreshable) universe context.
+ [ctx] is its (refreshable) universe context.
In info:
[hint_priority] is the hint's desired priority, it is computed as the number of products in [cty]
if unspecified
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 61e0e41eb9..90a9a7acd9 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -49,9 +49,9 @@ let match_with_non_recursive_type env sigma t =
(match EConstr.kind sigma hdapp with
| Ind (ind,u) ->
if (Environ.lookup_mind (fst ind) env).mind_finite == CoFinite then
- Some (hdapp,args)
- else
- None
+ Some (hdapp,args)
+ else
+ None
| _ -> None)
| _ -> None
@@ -65,7 +65,7 @@ let is_non_recursive_type env sigma t = Option.has_some (match_with_non_recursiv
let rec has_nodep_prod_after n env sigma c =
match EConstr.kind sigma c with
| Prod (_,_,b) | LetIn (_,_,_,b) ->
- ( n>0 || Vars.noccurn sigma 1 b)
+ ( n>0 || Vars.noccurn sigma 1 b)
&& (has_nodep_prod_after (n-1) env sigma b)
| _ -> true
@@ -100,36 +100,36 @@ let match_with_one_constructor env sigma style onlybinary allow_rec t =
| Ind ind ->
let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
if Int.equal (Array.length mip.mind_consnames) 1
- && (allow_rec || not (mis_is_recursive (fst ind,mib,mip)))
+ && (allow_rec || not (mis_is_recursive (fst ind,mib,mip)))
&& (Int.equal mip.mind_nrealargs 0)
then
- if is_strict_conjunction style (* strict conjunction *) then
+ if is_strict_conjunction style (* strict conjunction *) then
let (ctx, _) = mip.mind_nf_lc.(0) in
let ctx = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
- if
+ if
(* Constructor has a type of the form
c : forall (a_0 ... a_n : Type) (x_0 : A_0) ... (x_n : A_n). T **)
- List.for_all
- (fun decl -> let c = RelDecl.get_type decl in
- is_local_assum decl &&
+ List.for_all
+ (fun decl -> let c = RelDecl.get_type decl in
+ is_local_assum decl &&
Constr.isRel c &&
Int.equal (Constr.destRel c) mib.mind_nparams) ctx
- then
- Some (hdapp,args)
- else None
- else
+ then
+ Some (hdapp,args)
+ else None
+ else
let ctx, cty = mip.mind_nf_lc.(0) in
let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
let ctyp = whd_beta_prod sigma
(Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in
- let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
+ let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then
- (* Record or non strict conjunction *)
- Some (hdapp,List.rev cargs)
- else
- None
+ (* Record or non strict conjunction *)
+ Some (hdapp,List.rev cargs)
+ else
+ None
else
- None
+ None
| _ -> None in
match res with
| Some (hdapp, args) when not onlybinary -> res
@@ -185,10 +185,10 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) env sigma t =
then
if strict then
if test_strict_disjunction (mib, mip) then
- Some (hdapp,args)
- else
- None
- else
+ Some (hdapp,args)
+ else
+ None
+ else
let map (ctx, cty) =
let ar = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
pi2 (destProd sigma (prod_applist sigma ar args))
@@ -196,7 +196,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) env sigma t =
let cargs = Array.map map mip.mind_nf_lc in
Some (hdapp,Array.to_list cargs)
else
- None
+ None
| _ -> None in
match res with
| Some (hdapp,args) when not onlybinary -> res
@@ -215,7 +215,7 @@ let match_with_empty_type env sigma t =
| Ind (ind, _) ->
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let nconstr = Array.length mip.mind_consnames in
- if Int.equal nconstr 0 then Some hdapp else None
+ if Int.equal nconstr 0 then Some hdapp else None
| _ -> None
let is_empty_type env sigma t = Option.has_some (match_with_empty_type env sigma t)
@@ -230,9 +230,9 @@ let match_with_unit_or_eq_type env sigma t =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let nconstr = Array.length mip.mind_consnames in
if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then
- Some hdapp
- else
- None
+ Some hdapp
+ else
+ None
| _ -> None
let is_unit_or_eq_type env sigma t = Option.has_some (match_with_unit_or_eq_type env sigma t)
@@ -307,16 +307,16 @@ let match_with_equation env sigma t =
let (mib,mip) = Global.lookup_inductive ind in
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
- if Int.equal nconstr 1 then
+ if Int.equal nconstr 1 then
let (ctx, cty) = constr_types.(0) in
let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
if is_matching env sigma coq_refl_leibniz1_pattern cty then
- None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
+ None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
else if is_matching env sigma coq_refl_leibniz2_pattern cty then
- None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+ None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
else if is_matching env sigma coq_refl_jm_pattern cty then
- None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
- else raise NoEquationFound
+ None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+ else raise NoEquationFound
else raise NoEquationFound
| _ -> raise NoEquationFound
@@ -485,7 +485,7 @@ let match_sigma env sigma ex =
| App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f ->
build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr)
| _ -> raise PatternMatchingFailure
-
+
let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *)
match_sigma env ex
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 5ff257fbfe..803305a1ca 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -120,7 +120,7 @@ val match_with_equation:
(***** Destructing patterns bound to some theory *)
-(** Match terms [eq A t u], [identity A t u] or [JMeq A t A u]
+(** Match terms [eq A t u], [identity A t u] or [JMeq A t A u]
Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
val find_eq_data_decompose : Proofview.Goal.t -> constr ->
coq_eq_data * EInstance.t * (types * constr * constr)
@@ -132,7 +132,7 @@ val find_this_eq_data_decompose : Proofview.Goal.t -> constr ->
(** A variant that returns more informative structure on the equality found *)
val find_eq_data : evar_map -> constr -> coq_eq_data * EInstance.t * equation_kind
-(** Match a term of the form [(existT A P t p)]
+(** Match a term of the form [(existT A P t p)]
Returns associated lemmas and [A,P,t,p] *)
val find_sigma_data_decompose : Environ.env -> evar_map -> constr ->
coq_sigma_data * (EInstance.t * constr * constr * constr * constr)
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index e9a792c264..7e544b09dc 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -43,7 +43,7 @@ val declare_individual_scheme_object : string -> ?aux:string ->
(** Force generation of a (mutually) scheme with possibly user-level names *)
-val define_individual_scheme : individual scheme_kind ->
+val define_individual_scheme : individual scheme_kind ->
internal_flag (** internal *) ->
Id.t option -> inductive -> Constant.t * Evd.side_effects
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 49d0428a6f..be0421d42d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -84,30 +84,30 @@ let make_inv_predicate env evd indf realargs id status concl =
let (hyps,concl) =
match status with
| NoDep ->
- (* We push the arity and leave concl unchanged *)
- let hyps_arity,_ = get_arity env indf in
- let hyps_arity = List.map (fun d -> map_rel_decl EConstr.of_constr d) hyps_arity in
- (hyps_arity,concl)
+ (* We push the arity and leave concl unchanged *)
+ let hyps_arity,_ = get_arity env indf in
+ let hyps_arity = List.map (fun d -> map_rel_decl EConstr.of_constr d) hyps_arity in
+ (hyps_arity,concl)
| Dep dflt_concl ->
- if not (occur_var env !evd id concl) then
- user_err ~hdr:"make_inv_predicate"
+ if not (occur_var env !evd id concl) then
+ user_err ~hdr:"make_inv_predicate"
(str "Current goal does not depend on " ++ Id.print id ++ str".");
(* We abstract the conclusion of goal with respect to
realargs and c to * be concl in order to rewrite and have
c also rewritten when the case * will be done *)
- let pred =
+ let pred =
match dflt_concl with
| Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
| None ->
- let sort = get_sort_family_of env !evd concl in
+ let sort = get_sort_family_of env !evd concl in
let sort = evd_comb1 Evd.fresh_sort_in_family evd sort in
- let p = make_arity env !evd true indf sort in
- let evd',(p,ptyp) = Unification.abstract_list_all env
+ let p = make_arity env !evd true indf sort in
+ let evd',(p,ptyp) = Unification.abstract_list_all env
!evd p concl (realargs@[mkVar id])
- in evd := evd'; p in
- let hyps,bodypred = decompose_lam_n_assum !evd (nrealargs+1) pred in
- (* We lift to make room for the equations *)
- (hyps,lift nrealargs bodypred)
+ in evd := evd'; p in
+ let hyps,bodypred = decompose_lam_n_assum !evd (nrealargs+1) pred in
+ (* We lift to make room for the equations *)
+ (hyps,lift nrealargs bodypred)
in
let nhyps = Context.Rel.length hyps in
let env' = push_rel_context hyps env in
@@ -124,11 +124,11 @@ let make_inv_predicate env evd indf realargs id status concl =
let (xi, ti) = compute_eqn env' !evd nhyps n ai in
let (lhs,eqnty,rhs) =
if closed0 !evd ti then
- (xi,ti,ai)
+ (xi,ti,ai)
else
- let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in
- evd := sigma; res
- in
+ let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in
+ evd := sigma; res
+ in
let eq_term = eqdata.Coqlib.eq in
let eq = evd_comb1 (Evd.fresh_global env) evd eq_term in
let eqn = applist (eq,[eqnty;lhs;rhs]) in
@@ -195,9 +195,9 @@ let dependent_hyps env id idlist gl =
let rec dep_rec =function
| [] -> []
| d::l ->
- (* Update the type of id1: it may have been subject to rewriting *)
- let d = pf_get_hyp (NamedDecl.get_id d) gl in
- if occur_var_in_decl env (project gl) id d
+ (* Update the type of id1: it may have been subject to rewriting *)
+ let d = pf_get_hyp (NamedDecl.get_id d) gl in
+ if occur_var_in_decl env (project gl) id d
then d :: dep_rec l
else dep_rec l
in
@@ -380,14 +380,14 @@ let projectAndApply as_mode thin avoid id eqname names depids =
tclTHENLIST
[if as_mode then clear [id] else tclIDTAC;
(tclMAP_i (false,false) neqns (function (idopt,_) ->
- tclTRY (tclTHEN
+ tclTRY (tclTHEN
(intro_move_avoid idopt avoid Logic.MoveLast)
- (* try again to substitute and if still not a variable after *)
- (* decomposition, arbitrarily try to rewrite RL !? *)
- (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id))))))
- names);
+ (* try again to substitute and if still not a variable after *)
+ (* decomposition, arbitrarily try to rewrite RL !? *)
+ (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id))))))
+ names);
(if as_mode then tclIDTAC else clear [id])]
- (* Doing the above late breaks the computation of dids in
+ (* Doing the above late breaks the computation of dids in
generalizeRewriteIntros, and hence breaks proper intros_replacing
but it is needed for compatibility *)
in
@@ -396,7 +396,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
(* and apply a trailer which again try to substitute *)
(fun id ->
dEqThen ~keep_proofs:None false (deq_trailer id)
- (Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings))))
+ (Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings))))
id
let nLastDecls i tac =
@@ -420,17 +420,17 @@ let rewrite_equations as_mode othin neqns names ba =
clear (ids_of_named_context nodepids);
(nLastDecls neqns (fun ctx -> bring_hyps (List.rev ctx)));
(nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx)));
- tclMAP_i (true,false) neqns (fun (idopt,names) ->
+ tclMAP_i (true,false) neqns (fun (idopt,names) ->
(tclTHEN
(intro_move_avoid idopt avoid Logic.MoveLast)
- (onLastHypId (fun id ->
- tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
- names;
- tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
+ (onLastHypId (fun id ->
+ tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
+ names;
+ tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
let idopt = if as_mode then Some (NamedDecl.get_id d) else None in
intro_move idopt (if thin then Logic.MoveLast else !first_eq))
- nodepids;
- (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)]
+ nodepids;
+ (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)]
| None ->
(* simple inversion *)
if as_mode then
@@ -505,10 +505,10 @@ let wrap_inv_error id = function (e, info) -> match e with
Proofview.tclENV >>= fun env ->
Proofview.tclEVARMAP >>= fun sigma ->
tclZEROMSG (
- (strbrk "Inversion would require case analysis on sort " ++
+ (strbrk "Inversion would require case analysis on sort " ++
pr_sort sigma k ++
- strbrk " which is not allowed for inductive definition " ++
- pr_inductive env (fst i) ++ str "."))
+ strbrk " which is not allowed for inductive definition " ++
+ pr_inductive env (fst i) ++ str "."))
| e -> Proofview.tclZERO ~info e
(* The most general inversion tactic *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 2af3947dd1..cf58c9306c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -105,11 +105,11 @@ let max_prefix_sign lid sign =
let rec max_rec (resid,prefix) = function
| [] -> (resid,prefix)
| (id::l) ->
- let pre = sign_prefix id sign in
- if sign_length pre > sign_length prefix then
+ let pre = sign_prefix id sign in
+ if sign_length pre > sign_length prefix then
max_rec (id,pre) l
else
- max_rec (resid,prefix) l
+ max_rec (resid,prefix) l
in
match lid with
| [] -> nil_sign
@@ -119,11 +119,11 @@ let rec add_prods_sign env sigma t =
match EConstr.kind sigma (whd_all env sigma t) with
| Prod (na,c1,b) ->
let id = id_of_name_using_hdchar env sigma t na.binder_name in
- let b'= subst1 (mkVar id) b in
+ let b'= subst1 (mkVar id) b in
add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b'
| LetIn (na,c1,t1,b) ->
let id = id_of_name_using_hdchar env sigma t na.binder_name in
- let b'= subst1 (mkVar id) b in
+ let b'= subst1 (mkVar id) b in
add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b'
| _ -> (env,t)
@@ -149,7 +149,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
let pty = make_arity env sigma true indf sort in
let r = relevance_of_inductive_type env ind in
let goal =
- mkProd
+ mkProd
(make_annot Anonymous r, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
in
pty,goal
@@ -157,14 +157,14 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
let i = mkAppliedInd ind in
let ivars = global_vars env sigma i in
let revargs,ownsign =
- fold_named_context
- (fun env d (revargs,hyps) ->
+ fold_named_context
+ (fun env d (revargs,hyps) ->
let d = map_named_decl EConstr.of_constr d in
let id = NamedDecl.get_id d in
if Id.List.mem id ivars then
- ((mkVar id)::revargs, Context.Named.add d hyps)
- else
- (revargs,hyps))
+ ((mkVar id)::revargs, Context.Named.add d hyps)
+ else
+ (revargs,hyps))
env ~init:([],[])
in
let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
@@ -209,7 +209,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
(fun env d sign ->
let d = map_named_decl EConstr.of_constr d in
if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
- else Context.Named.add d sign)
+ else Context.Named.add d sign)
invEnv ~init:Context.Named.empty
end in
let avoid = ref Id.Set.empty in
@@ -218,11 +218,11 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
let rec fill_holes c =
match EConstr.kind sigma c with
| Evar (e,args) ->
- let h = next_ident_away (Id.of_string "H") !avoid in
- let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
- avoid := Id.Set.add h !avoid;
+ let h = next_ident_away (Id.of_string "H") !avoid in
+ let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
+ avoid := Id.Set.add h !avoid;
ownSign := Context.Named.add (LocalAssum (make_annot h Sorts.Relevant,ty)) !ownSign;
- applist (mkVar h, inst)
+ applist (mkVar h, inst)
| _ -> EConstr.map sigma fill_holes c
in
let c = fill_holes pfterm in
@@ -250,7 +250,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac =
add_inversion_lemma ~poly na env sigma c sort bool tac
with
| UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
- user_err ~hdr:"Inv needs Nodep Prop Set" s
+ user_err ~hdr:"Inv needs Nodep Prop Set" s
(* ================================= *)
(* Applying a given inversion lemma *)
@@ -264,12 +264,12 @@ let lemInv id c =
Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
with
| NoSuchBinding ->
- user_err
- (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
+ user_err
+ (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
| UserError (a,b) ->
- user_err ~hdr:"LemInv"
- (str "Cannot refine current goal with the lemma " ++
- pr_leconstr_env (pf_env gls) (project gls) c)
+ user_err ~hdr:"LemInv"
+ (str "Cannot refine current goal with the lemma " ++
+ pr_leconstr_env (pf_env gls) (project gls) c)
end
let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index b93c4a176f..ed7ab9164a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -166,7 +166,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns =
user_err ?loc (str "Expects " ++ msg p1 p2 ++ str ".") in
let errn n =
user_err ?loc (str "Expects a disjunctive pattern with " ++ int n
- ++ str " branches.") in
+ ++ str " branches.") in
let err1' p1 p2 =
user_err ?loc (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
let errforthcoming ?loc =
@@ -246,7 +246,7 @@ let elimination_sort_of_clause = function
| Some id -> elimination_sort_of_hyp id
-let pf_with_evars glsev k gls =
+let pf_with_evars glsev k gls =
let evd, a = glsev gls in
tclTHEN (Refiner.tclEVARS evd) (k a) gls
@@ -411,7 +411,7 @@ module New = struct
let tclTRY t =
tclORELSE0 t (tclUNIT ())
-
+
let tclTRYb t =
tclORELSE0L (t <*> tclUNIT true) (tclUNIT false)
@@ -498,7 +498,7 @@ module New = struct
| Evd.Evar_empty -> Some (evk,evi)
| Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with
| Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
- | _ ->
+ | _ ->
(* We make the assumption that there is no way to refine an
evar remaining after typing from the initial term given to
apply/elim and co tactics, is it correct? *)
@@ -567,11 +567,11 @@ module New = struct
let nthHypId m gl =
(* We only use [id] *)
nthDecl m gl |> NamedDecl.get_id
- let nthHyp m gl =
+ let nthHyp m gl =
mkVar (nthHypId m gl)
let onNthHypId m tac =
- Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end
+ Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end
let onNthHyp m tac =
Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end
@@ -644,12 +644,12 @@ module New = struct
match EConstr.kind elimclause.evd p with
| Meta p -> p
| _ ->
- let name_elim =
- match EConstr.kind sigma elim with
+ let name_elim =
+ match EConstr.kind sigma elim with
| Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
| _ -> mt ()
- in
- user_err ~hdr:"Tacticals.general_elim_then_using"
+ in
+ user_err ~hdr:"Tacticals.general_elim_then_using"
(str "The elimination combinator " ++ name_elim ++ str " is unknown.")
in
let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
@@ -733,7 +733,7 @@ module New = struct
tac branches
end
- let case_on_ba tac ba =
+ let case_on_ba tac ba =
Proofview.Goal.enter begin fun gl ->
let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
tac branches
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index c6aef6a554..31d26834d6 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -68,7 +68,7 @@ val afterHyp : Id.t -> Goal.goal sigma -> named_context
val ifOnHyp : (Id.t * types -> bool) ->
(Id.t -> tactic) -> (Id.t -> tactic) ->
- Id.t -> tactic
+ Id.t -> tactic
val onHyps : (Goal.goal sigma -> named_context) ->
(named_context -> tactic) -> tactic
@@ -109,7 +109,7 @@ val get_and_check_or_and_pattern :
bool list array -> intro_patterns array
(** Tolerate "[]" to mean a disjunctive pattern of any length *)
-val fix_empty_or_and_pattern : int ->
+val fix_empty_or_and_pattern : int ->
delayed_open_constr or_and_intro_pattern_expr ->
delayed_open_constr or_and_intro_pattern_expr
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6fd18b83d1..33c9c11350 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -446,7 +446,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
sign',t,concl,sigma
else
(if check && mem_named_context_val id sign then
- user_err (str "Variable " ++ Id.print id ++ str " is already declared.");
+ user_err (str "Variable " ++ Id.print id ++ str " is already declared.");
push_named_context_val (LocalAssum (make_annot id r,t)) sign,t,concl,sigma) in
let nf_t = nf_betaiota env sigma t in
Proofview.tclTHEN
@@ -660,24 +660,24 @@ let bind_red_expr_occurrences occs nbcl redexp =
else
match redexp with
| Unfold (_::_::_) ->
- error_illegal_clause ()
+ error_illegal_clause ()
| Unfold [(occl,c)] ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- Unfold [(occs,c)]
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ Unfold [(occs,c)]
| Pattern (_::_::_) ->
- error_illegal_clause ()
+ error_illegal_clause ()
| Pattern [(occl,c)] ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- Pattern [(occs,c)]
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ Pattern [(occs,c)]
| Simpl (f,Some (occl,c)) ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- Simpl (f,Some (occs,c))
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ Simpl (f,Some (occs,c))
| CbvVm (Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
@@ -690,9 +690,9 @@ let bind_red_expr_occurrences occs nbcl redexp =
CbvNative (Some (occs,c))
| Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
| ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
- error_occurrences_not_unsupported ()
+ error_occurrences_not_unsupported ()
| Unfold [] | Pattern [] ->
- assert false
+ assert false
(* The following two tactics apply an arbitrary
reduction function either to the conclusion or to a
@@ -809,7 +809,7 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
if deep then begin
let t2 = Retyping.get_type_of env sigma origc in
let sigma, t2 = Evarsolve.refresh_universes
- ~onlyalg:true (Some false) env sigma t2 in
+ ~onlyalg:true (Some false) env sigma t2 in
match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with
| None ->
if
@@ -891,7 +891,7 @@ let change ~check chg c cls =
e_change_in_hyps ~check:false ~reorder f hyps
end
-let change_concl t =
+let change_concl t =
change_in_concl ~check:true None (make_change_arg t)
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
@@ -999,7 +999,7 @@ let find_intro_names ctxt gl =
let build_intro_tac id dest tac = match dest with
| MoveLast -> Tacticals.New.tclTHEN (introduction id) (tac id)
- | dest -> Tacticals.New.tclTHENLIST
+ | dest -> Tacticals.New.tclTHENLIST
[introduction id; move_hyp id dest; tac id]
let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
@@ -1011,10 +1011,10 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
match EConstr.kind sigma concl with
| Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
let name = find_name false (LocalAssum (name,t)) name_flag gl in
- build_intro_tac name move_flag tac
+ build_intro_tac name move_flag tac
| LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
let name = find_name false (LocalDef (name,b,t)) name_flag gl in
- build_intro_tac name move_flag tac
+ build_intro_tac name move_flag tac
| Evar ev when force_flag ->
let sigma, t = Evardefine.define_evar_as_product env sigma ev in
Tacticals.New.tclTHEN
@@ -1028,9 +1028,9 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
(* probably also a pity that intro does zeta *)
else Proofview.tclUNIT ()
end <*>
- Proofview.tclORELSE
- (Tacticals.New.tclTHEN hnf_in_concl
- (intro_then_gen name_flag move_flag false dep_flag tac))
+ Proofview.tclORELSE
+ (Tacticals.New.tclTHEN hnf_in_concl
+ (intro_then_gen name_flag move_flag false dep_flag tac))
begin function (e, info) -> match e with
| RefinerError (env, sigma, IntroNeedsProduct) ->
Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
@@ -1107,9 +1107,9 @@ let intros_possibly_replacing ids =
let hyps = Proofview.Goal.hyps gl in
let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in
Tacticals.New.tclTHEN
- (Tacticals.New.tclMAP (fun id ->
- Tacticals.New.tclTRY (clear_for_replacing [id]))
- (if suboptimal then ids else List.rev ids))
+ (Tacticals.New.tclMAP (fun id ->
+ Tacticals.New.tclTRY (clear_for_replacing [id]))
+ (if suboptimal then ids else List.rev ids))
(Tacticals.New.tclMAP (fun (id,pos) ->
Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id))
posl)
@@ -1182,9 +1182,9 @@ let depth_of_quantified_hypothesis red h gl =
| None ->
user_err ~hdr:"lookup_quantified_hypothesis"
(str "No " ++ msg_quantified_hypothesis h ++
- strbrk " in current goal" ++
- (if red then strbrk " even after head-reduction" else mt ()) ++
- str".")
+ strbrk " in current goal" ++
+ (if red then strbrk " even after head-reduction" else mt ()) ++
+ str".")
let intros_until_gen red h =
Proofview.Goal.enter begin fun gl ->
@@ -1215,7 +1215,7 @@ let rec intros_move = function
| [] -> Proofview.tclUNIT ()
| (hyp,destopt) :: rest ->
Tacticals.New.tclTHEN (intro_gen (NamingMustBe (CAst.make hyp)) destopt false false)
- (intros_move rest)
+ (intros_move rest)
(* Apply a tactic on a quantified hypothesis, an hypothesis in context
or a term with bindings *)
@@ -1365,8 +1365,8 @@ let do_replace id = function
let clenv_refine_in with_evars targetid id sigma0 clenv tac =
let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
let clenv =
- { clenv with evd = Typeclasses.resolve_typeclasses
- ~fail:(not with_evars) clenv.env clenv.evd }
+ { clenv with evd = Typeclasses.resolve_typeclasses
+ ~fail:(not with_evars) clenv.env clenv.evd }
in
let new_hyp_typ = clenv_type clenv in
if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
@@ -1518,8 +1518,8 @@ let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma c with
| Var id when lbindc == NoBindings ->
- Tacticals.New.tclTHEN (try_intros_until_id_check id)
- (general_case_analysis_in_context with_evars clear_flag cx)
+ Tacticals.New.tclTHEN (try_intros_until_id_check id)
+ (general_case_analysis_in_context with_evars clear_flag cx)
| _ ->
general_case_analysis_in_context with_evars clear_flag cx
@@ -1569,10 +1569,10 @@ let elim with_evars clear_flag (c,lbindc as cx) elim =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma c with
| Var id when lbindc == NoBindings ->
- Tacticals.New.tclTHEN (try_intros_until_id_check id)
- (elim_in_context with_evars clear_flag cx elim)
+ Tacticals.New.tclTHEN (try_intros_until_id_check id)
+ (elim_in_context with_evars clear_flag cx elim)
| _ ->
- elim_in_context with_evars clear_flag cx elim
+ elim_in_context with_evars clear_flag cx elim
(* The simplest elimination tactic, with no substitutions at all. *)
@@ -1605,36 +1605,36 @@ let make_projection env sigma params cstr sign elim i n c u =
let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in
let branch = it_mkLambda_or_LetIn b cs_args in
if
- (* excludes dependent projection types *)
- noccur_between sigma 1 (n-i-1) t
- (* to avoid surprising unifications, excludes flexible
- projection types or lambda which will be instantiated by Meta/Evar *)
- && not (isEvar sigma (fst (whd_betaiota_stack sigma t)))
- && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t))
+ (* excludes dependent projection types *)
+ noccur_between sigma 1 (n-i-1) t
+ (* to avoid surprising unifications, excludes flexible
+ projection types or lambda which will be instantiated by Meta/Evar *)
+ && not (isEvar sigma (fst (whd_betaiota_stack sigma t)))
+ && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t))
then
let t = lift (i+1-n) t in
- let abselim = beta_applist sigma (elim, params@[t;branch]) in
- let args = Context.Rel.to_extended_vect mkRel 0 sign in
- let c = beta_applist sigma (abselim, [mkApp (c, args)]) in
- Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
+ let abselim = beta_applist sigma (elim, params@[t;branch]) in
+ let args = Context.Rel.to_extended_vect mkRel 0 sign in
+ let c = beta_applist sigma (abselim, [mkApp (c, args)]) in
+ Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
else
- None
+ None
| DefinedRecord l ->
(* goes from left to right when i increases! *)
match List.nth l i with
| Some proj ->
- let args = Context.Rel.to_extended_vect mkRel 0 sign in
- let proj =
+ let args = Context.Rel.to_extended_vect mkRel 0 sign in
+ let proj =
match Recordops.find_primitive_projection proj with
| Some proj ->
- mkProj (Projection.make proj false, mkApp (c, args))
+ mkProj (Projection.make proj false, mkApp (c, args))
| None ->
- mkApp (mkConstU (proj,u), Array.append (Array.of_list params)
- [|mkApp (c, args)|])
- in
- let app = it_mkLambda_or_LetIn proj sign in
- let t = Retyping.get_type_of env sigma app in
- Some (app, t)
+ mkApp (mkConstU (proj,u), Array.append (Array.of_list params)
+ [|mkApp (c, args)|])
+ in
+ let app = it_mkLambda_or_LetIn proj sign in
+ let t = Retyping.get_type_of env sigma app in
+ Some (app, t)
| None -> None
in elim
@@ -1649,32 +1649,32 @@ let descend_in_conjunctions avoid tac (err, info) c =
match match_with_tuple env sigma ccl with
| Some (_,_,isrec) ->
let n = (constructors_nrealargs env ind).(0) in
- let sort = Tacticals.New.elimination_sort_of_goal gl in
- let IndType (indf,_) = find_rectype env sigma ccl in
- let (_,inst), params = dest_ind_family indf in
- let params = List.map EConstr.of_constr params in
- let cstr = (get_constructors env indf).(0) in
- let elim =
- try DefinedRecord (Recordops.lookup_projections ind)
- with Not_found ->
+ let sort = Tacticals.New.elimination_sort_of_goal gl in
+ let IndType (indf,_) = find_rectype env sigma ccl in
+ let (_,inst), params = dest_ind_family indf in
+ let params = List.map EConstr.of_constr params in
+ let cstr = (get_constructors env indf).(0) in
+ let elim =
+ try DefinedRecord (Recordops.lookup_projections ind)
+ with Not_found ->
let u = EInstance.kind sigma u in
- let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in
- let elim = EConstr.of_constr elim in
- NotADefinedRecordUseScheme elim in
- Tacticals.New.tclORELSE0
- (Tacticals.New.tclFIRST
- (List.init n (fun i ->
+ let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in
+ let elim = EConstr.of_constr elim in
+ NotADefinedRecordUseScheme elim in
+ Tacticals.New.tclORELSE0
+ (Tacticals.New.tclFIRST
+ (List.init n (fun i ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
- match make_projection env sigma params cstr sign elim i n c u with
- | None -> Tacticals.New.tclFAIL 0 (mt())
- | Some (p,pt) ->
- Tacticals.New.tclTHENS
- (assert_before_gen false (NamingAvoid avoid) pt)
+ match make_projection env sigma params cstr sign elim i n c u with
+ | None -> Tacticals.New.tclFAIL 0 (mt())
+ | Some (p,pt) ->
+ Tacticals.New.tclTHENS
+ (assert_before_gen false (NamingAvoid avoid) pt)
[Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p));
- (* Might be ill-typed due to forbidden elimination. *)
- Tacticals.New.onLastHypId (tac (not isrec))]
+ (* Might be ill-typed due to forbidden elimination. *)
+ Tacticals.New.onLastHypId (tac (not isrec))]
end)))
(Proofview.tclZERO ~info err)
| None -> Proofview.tclZERO ~info err
@@ -1783,7 +1783,7 @@ let apply_with_delayed_bindings_gen b e l =
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let (sigma, cb) = f env sigma in
- Tacticals.New.tclWITHHOLES e
+ Tacticals.New.tclWITHHOLES e
(general_apply ~respect_opaque:(not b) b b e k CAst.(make ?loc cb)) sigma
end
in
@@ -1903,7 +1903,7 @@ let apply_in_delayed_once ?(respect_opaque = false) with_delta
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (sigma, c) = f env sigma in
- Tacticals.New.tclWITHHOLES with_evars
+ Tacticals.New.tclWITHHOLES with_evars
(apply_in_once ~respect_opaque with_delta with_destruct with_evars
naming id (clear_flag,CAst.(make ?loc c)) tac)
sigma
@@ -2007,7 +2007,7 @@ let assumption =
match ans with
| Some sigma ->
(Proofview.Unsafe.tclEVARS sigma) <*>
- exact_no_check (mkVar (NamedDecl.get_id decl))
+ exact_no_check (mkVar (NamedDecl.get_id decl))
| None -> arec gl only_eq rest
in
let assumption_tac gl =
@@ -2127,7 +2127,7 @@ let keep hyps =
let hyp = NamedDecl.get_id decl in
if Id.List.mem hyp hyps
|| List.exists (occur_var_in_decl env sigma hyp) keep
- || occur_var env sigma hyp ccl
+ || occur_var env sigma hyp ccl
then (clear,decl::keep)
else (hyp::clear,keep))
~init:([],[]) (Proofview.Goal.env gl)
@@ -2173,7 +2173,7 @@ let bring_hyps hyps =
end
end
-let revert hyps =
+let revert hyps =
Proofview.Goal.enter begin fun gl ->
let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in
(bring_hyps ctx) <*> (clear hyps)
@@ -2187,7 +2187,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
if Int.equal i 0 then error "The constructors are numbered starting from 1.";
begin match expctdnumopt with
| Some n when not (Int.equal n nconstr) ->
- user_err ~hdr:"Tactics.check_number_of_constructors"
+ user_err ~hdr:"Tactics.check_number_of_constructors"
(str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
| _ -> ()
end;
@@ -2351,8 +2351,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
let l2r = not l2r in (* equality of the form eq_true *)
if isVar sigma c then
let id' = destVar sigma c in
- Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl)
- (clear_var_and_eq id'),
+ Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl)
+ (clear_var_and_eq id'),
early_clear id' thin
else
Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]),
@@ -2362,7 +2362,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
thin in
(* Skip the side conditions of the rewriting step *)
Tacticals.New.tclTHENFIRST eqtac (tac thin)
- end
+ end
let prepare_naming ?loc = function
| IntroIdentifier id -> NamingMustBe (CAst.make ?loc id)
@@ -2473,12 +2473,12 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
match pat with
| IntroForthcoming onlydeps ->
intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
- destopt onlydeps n bound
+ destopt onlydeps n bound
(fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound
(n+List.length ids) tac l)
| IntroAction pat ->
intro_then_gen (make_tmp_naming avoid l pat)
- destopt true false
+ destopt true false
(intro_pattern_action ?loc with_evars (b || not (List.is_empty l)) false
pat thin destopt
(fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0
@@ -2496,12 +2496,12 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac
(fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l))
| IntroAnonymous ->
intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
- destopt true false
+ destopt true false
(fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
| IntroFresh id ->
(* todo: avoid thinned names to interfere with generation of fresh name *)
intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l)))
- destopt true false
+ destopt true false
(fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
@@ -2538,7 +2538,7 @@ and prepare_intros ?loc with_evars dft destopt = function
(fun _ l -> clear_wildcards l) in
fun id ->
intro_pattern_action ?loc with_evars true true ipat [] destopt tac id)
- | IntroForthcoming _ -> user_err ?loc
+ | IntroForthcoming _ -> user_err ?loc
(str "Introduction pattern for one hypothesis expected.")
let intro_patterns_head_core with_evars b destopt bound pat =
@@ -2670,12 +2670,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
let refl = applist (refl, [t;mkVar id]) in
let term = mkNamedLetIn (make_annot id Sorts.Relevant) c t
(mkLetIn (make_annot (Name heq) Sorts.Relevant, refl, eq, ccl)) in
- let sigma, _ = Typing.type_of env sigma term in
+ let sigma, _ = Typing.type_of env sigma term in
let ans = term,
Tacticals.New.tclTHENLIST
- [
+ [
intro_gen (NamingMustBe CAst.(make ?loc heq)) (decode_hyp lastlhyp) true false;
- clear_body [heq;id]]
+ clear_body [heq;id]]
in
(sigma, ans)
| None ->
@@ -2830,19 +2830,19 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
let generalized_name env sigma c t ids cl = function
| Name id as na ->
if Id.List.mem id ids then
- user_err (Id.print id ++ str " is already used.");
+ user_err (Id.print id ++ str " is already used.");
na
| Anonymous ->
match EConstr.kind sigma c with
| Var id ->
- (* Keep the name even if not occurring: may be used by intros later *)
- Name id
+ (* Keep the name even if not occurring: may be used by intros later *)
+ Name id
| _ ->
- if noccurn sigma 1 cl then Anonymous else
- (* On ne s'etait pas casse la tete : on avait pris pour nom de
+ if noccurn sigma 1 cl then Anonymous else
+ (* On ne s'etait pas casse la tete : on avait pris pour nom de
variable la premiere lettre du type, meme si "c" avait ete une
constante dont on aurait pu prendre directement le nom *)
- named_hd env sigma t Anonymous
+ named_hd env sigma t Anonymous
(* Abstract over [c] in [forall x1:A1(c)..xi:Ai(c).T(c)] producing
[forall x, x1:A1(x1), .., xi:Ai(x). T(x)] with all [c] abtracted in [Ai]
@@ -2890,7 +2890,7 @@ let generalize_dep ?(with_let=false) c =
let tothin' =
match EConstr.kind sigma c with
| Var id when mem_named_context_val id (val_of_named_context sign) && not (Id.List.mem id init_ids)
- -> id::tothin
+ -> id::tothin
| _ -> tothin
in
let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
@@ -2936,19 +2936,19 @@ let new_generalize_gen_let lconstr =
let env = Proofview.Goal.env gl in
let ids = Tacmach.New.pf_ids_of_hyps gl in
let newcl, sigma, args =
- List.fold_right_i
- (fun i ((_,c,b),_ as o) (cl, sigma, args) ->
- let sigma, t = Typing.type_of env sigma c in
- let args = if Option.is_empty b then c :: args else args in
+ List.fold_right_i
+ (fun i ((_,c,b),_ as o) (cl, sigma, args) ->
+ let sigma, t = Typing.type_of env sigma c in
+ let args = if Option.is_empty b then c :: args else args in
let cl, sigma = generalize_goal_gen env sigma ids i o t cl in
(cl, sigma, args))
- 0 lconstr (concl, sigma, [])
+ 0 lconstr (concl, sigma, [])
in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Refine.refine ~typecheck:false begin fun sigma ->
+ (Refine.refine ~typecheck:false begin fun sigma ->
let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true newcl in
(sigma, applist (ev, args))
- end)
+ end)
end
let generalize_gen lconstr =
@@ -3052,7 +3052,7 @@ let specialize (c,lbind) ipat =
let repl = do_replace (Some id) naming in
Tacticals.New.tclTHENFIRST
(assert_before_then_gen repl naming typ tac)
- (exact_no_check term)
+ (exact_no_check term)
| _ ->
match ipat with
| None ->
@@ -3067,7 +3067,7 @@ let specialize (c,lbind) ipat =
let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in
Tacticals.New.tclTHENFIRST
(assert_before_then_gen false naming typ tac)
- (exact_no_check term)
+ (exact_no_check term)
in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac
end
@@ -3253,16 +3253,16 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
let (hyprec,names) =
consume_pattern avoid (Name hyprecname) depind gl names
in
- dest_intro_patterns with_evars avoid thin MoveLast [hyprec] (fun ids' thin ->
- peel_tac ra' (update_dest dests ids') names thin)
+ dest_intro_patterns with_evars avoid thin MoveLast [hyprec] (fun ids' thin ->
+ peel_tac ra' (update_dest dests ids') names thin)
end)
end
| (IndArg,_,dep,hyprecname) :: ra' ->
Proofview.Goal.enter begin fun gl ->
- (* Rem: does not happen in Coq schemes, only in user-defined schemes *)
+ (* Rem: does not happen in Coq schemes, only in user-defined schemes *)
let pat,names =
consume_pattern avoid (Name hyprecname) dep gl names in
- dest_intro_patterns with_evars avoid thin MoveLast [pat] (fun ids thin ->
+ dest_intro_patterns with_evars avoid thin MoveLast [pat] (fun ids thin ->
peel_tac ra' (update_dest dests ids) names thin)
end
| (RecArg,_,dep,recvarname) :: ra' ->
@@ -3270,14 +3270,14 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
let (pat,names) =
consume_pattern avoid (Name recvarname) dep gl names in
let dest = get_recarg_dest dests in
- dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
+ dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
end
| (OtherArg,_,dep,_) :: ra' ->
Proofview.Goal.enter begin fun gl ->
let (pat,names) = consume_pattern avoid Anonymous dep gl names in
let dest = get_recarg_dest dests in
- safe_dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
+ safe_dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
end
| [] ->
@@ -3301,8 +3301,8 @@ let expand_projections env sigma c =
| _ -> map_constr_with_full_binders sigma push_rel aux env c
in
aux env c
-
-
+
+
(* Marche pas... faut prendre en compte l'occurrence précise... *)
let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
@@ -3327,14 +3327,14 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
else
let c = List.nth argl (i-1) in
match EConstr.kind sigma c with
- | Var id when not (List.exists (fun c -> occur_var env sigma id c) args') &&
+ | Var id when not (List.exists (fun c -> occur_var env sigma id c) args') &&
not (List.exists (fun c -> occur_var env sigma id c) params') ->
(* Based on the knowledge given by the user, all
constraints on the variable are generalizable in the
current environment so that it is clearable after destruction *)
- atomize_one (i-1) (c::args) (c::args') (Id.Set.add id avoid)
- | _ ->
- let c' = expand_projections env' sigma c in
+ atomize_one (i-1) (c::args) (c::args') (Id.Set.add id avoid)
+ | _ ->
+ let c' = expand_projections env' sigma c in
let dependent t = dependent sigma c t in
if List.exists dependent params' ||
List.exists dependent args'
@@ -3344,7 +3344,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
follow the (old) discipline of not generalizing over
this term, since we don't try to invert the
constraint anyway. *)
- atomize_one (i-1) (c::args) (c'::args') avoid
+ atomize_one (i-1) (c::args) (c'::args') avoid
else
(* We reason blindly on the term and do as if it were
generalizable, ignoring the constraints coming from
@@ -3355,9 +3355,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
let type_of = Tacmach.New.pf_unsafe_type_of gl in
id_of_name_using_hdchar env sigma (type_of c) Anonymous in
let x = fresh_id_in_env avoid id env in
- Tacticals.New.tclTHEN
- (letin_tac None (Name x) c None allHypsAndConcl)
- (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (Id.Set.add x avoid))
+ Tacticals.New.tclTHEN
+ (letin_tac None (Name x) c None allHypsAndConcl)
+ (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (Id.Set.add x avoid))
in
atomize_one (List.length argl) [] [] Id.Set.empty
end
@@ -3454,30 +3454,30 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
toclear := hyp::!toclear;
rhyp
end else
- let dephyp0 = List.is_empty inhyps &&
- (Option.cata (fun id -> occur_var_in_decl env sigma id decl) false hyp0_opt)
+ let dephyp0 = List.is_empty inhyps &&
+ (Option.cata (fun id -> occur_var_in_decl env sigma id decl) false hyp0_opt)
in
let depother = List.is_empty inhyps &&
- (Id.Set.exists (fun id -> occur_var_in_decl env sigma id decl) indvars ||
+ (Id.Set.exists (fun id -> occur_var_in_decl env sigma id decl) indvars ||
List.exists (fun decl' -> occur_var_in_decl env sigma (NamedDecl.get_id decl') decl) !decldeps)
in
if not (List.is_empty inhyps) && Id.List.mem hyp inhyps
|| dephyp0 || depother
then begin
- decldeps := decl::!decldeps;
- avoid := Id.Set.add hyp !avoid;
+ decldeps := decl::!decldeps;
+ avoid := Id.Set.add hyp !avoid;
maindep := dephyp0 || !maindep;
- if !before then begin
+ if !before then begin
toclear := hyp::!toclear;
- rstatus := (hyp,rhyp)::!rstatus
+ rstatus := (hyp,rhyp)::!rstatus
end
- else begin
- toclear := hyp::!toclear;
- ldeps := hyp::!ldeps (* status computed in 2nd phase *)
+ else begin
+ toclear := hyp::!toclear;
+ ldeps := hyp::!ldeps (* status computed in 2nd phase *)
end;
- MoveBefore hyp end
+ MoveBefore hyp end
else
- MoveBefore hyp
+ MoveBefore hyp
in
let _ = fold_named_context seek_deps env ~init:MoveFirst in
(* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *)
@@ -3543,7 +3543,7 @@ type elim_scheme = {
indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni)
if HI is in premisses, None otherwise *)
concl: types; (* Qi x1...xni HI (f...), HI and (f...)
- are optional and mutually exclusive *)
+ are optional and mutually exclusive *)
indarg_in_concl: bool; (* true if HI appears at the end of conclusion *)
farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *)
}
@@ -3584,8 +3584,8 @@ let make_up_names n ind_opt cname =
let base_ind =
if is_hyp then
match ind_opt with
- | None -> Id.of_string ind_prefix
- | Some ind_id -> add_prefix ind_prefix (Nametab.basename_of_global ind_id)
+ | None -> Id.of_string ind_prefix
+ | Some ind_id -> add_prefix ind_prefix (Nametab.basename_of_global ind_id)
else add_prefix ind_prefix cname in
let hyprecname = make_base n base_ind in
let avoid =
@@ -3633,7 +3633,7 @@ let lift_togethern n l =
let l', _ =
List.fold_right
(fun x (acc, n) ->
- (lift n x :: acc, succ n))
+ (lift n x :: acc, succ n))
l ([], n)
in l'
@@ -3644,14 +3644,14 @@ let ids_of_constr sigma ?(all=false) vars c =
match EConstr.kind sigma c with
| Var id -> Id.Set.add id vars
| App (f, args) ->
- (match EConstr.kind sigma f with
- | Construct ((ind,_),_)
- | Ind (ind,_) ->
+ (match EConstr.kind sigma f with
+ | Construct ((ind,_),_)
+ | Ind (ind,_) ->
let (mib,mip) = Global.lookup_inductive ind in
- Array.fold_left_from
- (if all then 0 else mib.Declarations.mind_nparams)
- aux vars args
- | _ -> EConstr.fold sigma aux vars c)
+ Array.fold_left_from
+ (if all then 0 else mib.Declarations.mind_nparams)
+ aux vars args
+ | _ -> EConstr.fold sigma aux vars c)
| _ -> EConstr.fold sigma aux vars c
in aux vars c
@@ -3662,7 +3662,7 @@ let decompose_indapp sigma f args =
let (mib,mip) = Global.lookup_inductive ind in
let first = mib.Declarations.mind_nparams_rec in
let pars, args = Array.chop first args in
- mkApp (f, pars), args
+ mkApp (f, pars), args
| _ -> f, args
let mk_term_eq homogeneous env sigma ty t ty' t' =
@@ -3722,13 +3722,13 @@ let hyps_of_vars env sigma sign nogen hyps =
Context.Named.fold_inside
(fun (hs,hl) d ->
let x = NamedDecl.get_id d in
- if Id.Set.mem x nogen then (hs,hl)
- else if Id.Set.mem x hs then (hs,x::hl)
- else
- let xvars = global_vars_set_of_decl env sigma d in
- if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then
- (Id.Set.add x hs, x :: hl)
- else (hs, hl))
+ if Id.Set.mem x nogen then (hs,hl)
+ else if Id.Set.mem x hs then (hs,x::hl)
+ else
+ let xvars = global_vars_set_of_decl env sigma d in
+ if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then
+ (Id.Set.add x hs, x :: hl)
+ else (hs, hl))
~init:(hyps,[])
sign
in lh
@@ -3739,14 +3739,14 @@ let linear sigma vars args =
let seen = ref vars in
try
Array.iter (fun i ->
- let rels = ids_of_constr sigma ~all:true Id.Set.empty i in
- let seen' =
- Id.Set.fold (fun id acc ->
- if Id.Set.mem id acc then raise Seen
- else Id.Set.add id acc)
- rels !seen
- in seen := seen')
- args;
+ let rels = ids_of_constr sigma ~all:true Id.Set.empty i in
+ let seen' =
+ Id.Set.fold (fun id acc ->
+ if Id.Set.mem id acc then raise Seen
+ else Id.Set.add id acc)
+ rels !seen
+ in seen := seen')
+ args;
true
with Seen -> false
@@ -3785,62 +3785,62 @@ let abstract_args gl generalize_vars dep id defined f args =
let leq = constr_cmp !sigma Reduction.CUMUL liftargty ty in
match EConstr.kind !sigma arg with
| Var id when not (is_defined_variable env id) && leq && not (Id.Set.mem id nongenvars) ->
- (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls,
- Id.Set.add id nongenvars, Id.Set.remove id vars, env)
+ (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls,
+ Id.Set.add id nongenvars, Id.Set.remove id vars, env)
| _ ->
- let name = get_id name in
+ let name = get_id name in
let decl = LocalAssum (make_annot (Name name) ty_relevance, ty) in
- let ctx = decl :: ctx in
- let c' = mkApp (lift 1 c, [|mkRel 1|]) in
- let args = arg :: args in
- let liftarg = lift (List.length ctx) arg in
- let eq, refl =
- if leq then
- let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in
+ let ctx = decl :: ctx in
+ let c' = mkApp (lift 1 c, [|mkRel 1|]) in
+ let args = arg :: args in
+ let liftarg = lift (List.length ctx) arg in
+ let eq, refl =
+ if leq then
+ let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in
let sigma', refl = mkRefl sigma' (lift (-lenctx) ty) arg in
sigma := sigma'; eq, refl
- else
- let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in
+ else
+ let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in
let sigma', refl = mkHRefl sigma' argty arg in
sigma := sigma'; eq, refl
- in
- let eqs = eq :: lift_list eqs in
- let refls = refl :: refls in
- let argvars = ids_of_constr !sigma vars arg in
- (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls,
- nongenvars, Id.Set.union argvars vars, env)
+ in
+ let eqs = eq :: lift_list eqs in
+ let refls = refl :: refls in
+ let argvars = ids_of_constr !sigma vars arg in
+ (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls,
+ nongenvars, Id.Set.union argvars vars, env)
in
let f', args' = decompose_indapp !sigma f args in
let dogen, f', args' =
let parvars = ids_of_constr !sigma ~all:true Id.Set.empty f' in
if not (linear !sigma parvars args') then true, f, args
else
- match Array.findi (fun i x -> not (isVar !sigma x) || is_defined_variable env (destVar !sigma x)) args' with
- | None -> false, f', args'
- | Some nonvar ->
- let before, after = Array.chop nonvar args' in
- true, mkApp (f', before), after
+ match Array.findi (fun i x -> not (isVar !sigma x) || is_defined_variable env (destVar !sigma x)) args' with
+ | None -> false, f', args'
+ | Some nonvar ->
+ let before, after = Array.chop nonvar args' in
+ true, mkApp (f', before), after
in
if dogen then
let tyf' = Tacmach.New.pf_unsafe_type_of gl f' in
let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
- Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
+ Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
in
let args, refls = List.rev args, List.rev refls in
let vars =
- if generalize_vars then
- let nogen = Id.Set.add id nogen in
- hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars
- else []
+ if generalize_vars then
+ let nogen = Id.Set.add id nogen in
+ hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars
+ else []
in
let body, c' =
- if defined then Some c', Retyping.get_type_of ctxenv !sigma c'
- else None, c'
+ if defined then Some c', Retyping.get_type_of ctxenv !sigma c'
+ else None, c'
in
let typ = Tacmach.New.pf_get_hyp_typ id gl in
let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in
let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in
- Some (tac, dep, succ (List.length ctx), vars)
+ Some (tac, dep, succ (List.length ctx), vars)
else None
let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
@@ -3852,10 +3852,10 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
let oldid = Tacmach.New.pf_get_new_id id gl in
match Tacmach.New.pf_get_hyp id gl with
| LocalAssum (_,t) -> let f, args = decompose_app sigma t in
- (f, args, false, id, oldid)
+ (f, args, false, id, oldid)
| LocalDef (_,t,_) ->
- let f, args = decompose_app sigma t in
- (f, args, true, id, oldid)
+ let f, args = decompose_app sigma t in
+ (f, args, true, id, oldid)
in
if List.is_empty args then Proofview.tclUNIT ()
else
@@ -3864,23 +3864,23 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
match newc with
| None -> Proofview.tclUNIT ()
| Some (tac, dep, n, vars) ->
- let tac =
- if dep then
+ let tac =
+ if dep then
Tacticals.New.tclTHENLIST [
tac;
- rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
- generalize_dep ~with_let:true (mkVar oldid)]
+ rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
+ generalize_dep ~with_let:true (mkVar oldid)]
else Tacticals.New.tclTHENLIST [
tac;
- clear [id];
- Tacticals.New.tclDO n intro]
- in
- if List.is_empty vars then tac
- else Tacticals.New.tclTHEN tac
+ clear [id];
+ Tacticals.New.tclDO n intro]
+ in
+ if List.is_empty vars then tac
+ else Tacticals.New.tclTHEN tac
(Tacticals.New.tclFIRST
[revert vars ;
- Tacticals.New.tclMAP (fun id ->
- Tacticals.New.tclTRY (generalize_dep ~with_let:true (mkVar id))) vars])
+ Tacticals.New.tclMAP (fun id ->
+ Tacticals.New.tclTRY (generalize_dep ~with_let:true (mkVar id))) vars])
end
let compare_upto_variables sigma x y =
@@ -3905,26 +3905,26 @@ let specialize_eqs id =
let rec aux in_eqs ctx acc ty =
match EConstr.kind !evars ty with
| Prod (na, t, b) ->
- (match EConstr.kind !evars t with
+ (match EConstr.kind !evars t with
| App (eq, [| eqty; x; y |]) when EConstr.is_global !evars Coqlib.(lib_ref "core.eq.type") eq ->
- let c = if noccur_between !evars 1 (List.length ctx) x then y else x in
- let pt = mkApp (eq, [| eqty; c; c |]) in
+ let c = if noccur_between !evars 1 (List.length ctx) x then y else x in
+ let pt = mkApp (eq, [| eqty; c; c |]) in
let ind = destInd !evars eq in
- let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in
- if unif (push_rel_context ctx env) evars pt t then
- aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
- else acc, in_eqs, ctx, ty
- | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq ->
- let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in
- let pt = mkApp (heq, [| eqt; c; eqt; c |]) in
+ let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in
+ if unif (push_rel_context ctx env) evars pt t then
+ aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
+ else acc, in_eqs, ctx, ty
+ | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq ->
+ let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in
+ let pt = mkApp (heq, [| eqt; c; eqt; c |]) in
let ind = destInd !evars heq in
- let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in
- if unif (push_rel_context ctx env) evars pt t then
- aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
- else acc, in_eqs, ctx, ty
- | _ ->
- if in_eqs then acc, in_eqs, ctx, ty
- else
+ let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in
+ if unif (push_rel_context ctx env) evars pt t then
+ aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
+ else acc, in_eqs, ctx, ty
+ | _ ->
+ if in_eqs then acc, in_eqs, ctx, ty
+ else
let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in
evars := sigma;
aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
@@ -3944,7 +3944,7 @@ let specialize_eqs id =
if worked then
Tacticals.New.tclTHENFIRST
(internal_cut true id ty')
- (exact_no_check ((* refresh_universes_strict *) acc'))
+ (exact_no_check ((* refresh_universes_strict *) acc'))
else
Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ Id.print id)
end
@@ -3973,10 +3973,10 @@ let decompose_paramspred_branch_args sigma elimt =
let rec cut_noccur elimt acc2 =
match EConstr.kind sigma elimt with
| Prod(nme,tpe,elimt') ->
- let hd_tpe,_ = decompose_app sigma (snd (decompose_prod_assum sigma tpe)) in
- if not (occur_rel sigma 1 elimt') && isRel sigma hd_tpe
+ let hd_tpe,_ = decompose_app sigma (snd (decompose_prod_assum sigma tpe)) in
+ if not (occur_rel sigma 1 elimt') && isRel sigma hd_tpe
then cut_noccur elimt' (LocalAssum (nme,tpe)::acc2)
- else let acc3,ccl = decompose_prod_assum sigma elimt in acc2 , acc3 , ccl
+ else let acc3,ccl = decompose_prod_assum sigma elimt in acc2 , acc3 , ccl
| App(_, _) | Rel _ -> acc2 , [] , elimt
| _ -> error_ind_scheme "" in
let rec cut_occur elimt acc1 =
@@ -4048,8 +4048,8 @@ let compute_elim_sig sigma ?elimc elimt =
if !res.farg_in_concl
then begin
res := { !res with
- indarg = None;
- indarg_in_concl = false; farg_in_concl = true };
+ indarg = None;
+ indarg_in_concl = false; farg_in_concl = true };
raise Exit
end;
(* 2- If no args_indargs (=!res.nargs at this point) then no indarg *)
@@ -4059,34 +4059,34 @@ let compute_elim_sig sigma ?elimc elimt =
match List.hd args_indargs with
| LocalDef (hiname,_,hi) -> error_ind_scheme ""
| LocalAssum (hiname,hi) ->
- let hi_ind, hi_args = decompose_app sigma hi in
- let hi_is_ind = (* hi est d'un type globalisable *)
- match EConstr.kind sigma hi_ind with
- | Ind (mind,_) -> true
- | Var _ -> true
- | Const _ -> true
- | Construct _ -> true
- | _ -> false in
- let hi_args_enough = (* hi a le bon nbre d'arguments *)
- Int.equal (List.length hi_args) (List.length params + !res.nargs -1) in
- (* FIXME: Ces deux tests ne sont pas suffisants. *)
- if not (hi_is_ind && hi_args_enough) then raise Exit (* No indarg *)
- else (* Last arg is the indarg *)
- res := {!res with
- indarg = Some (List.hd !res.args);
- indarg_in_concl = occur_rel sigma 1 ccl;
- args = List.tl !res.args; nargs = !res.nargs - 1;
- };
- raise Exit);
+ let hi_ind, hi_args = decompose_app sigma hi in
+ let hi_is_ind = (* hi est d'un type globalisable *)
+ match EConstr.kind sigma hi_ind with
+ | Ind (mind,_) -> true
+ | Var _ -> true
+ | Const _ -> true
+ | Construct _ -> true
+ | _ -> false in
+ let hi_args_enough = (* hi a le bon nbre d'arguments *)
+ Int.equal (List.length hi_args) (List.length params + !res.nargs -1) in
+ (* FIXME: Ces deux tests ne sont pas suffisants. *)
+ if not (hi_is_ind && hi_args_enough) then raise Exit (* No indarg *)
+ else (* Last arg is the indarg *)
+ res := {!res with
+ indarg = Some (List.hd !res.args);
+ indarg_in_concl = occur_rel sigma 1 ccl;
+ args = List.tl !res.args; nargs = !res.nargs - 1;
+ };
+ raise Exit);
raise Exit(* exit anyway *)
with Exit -> (* Ending by computing indref: *)
match !res.indarg with
| None -> !res (* No indref *)
| Some (LocalDef _) -> error_ind_scheme ""
| Some (LocalAssum (_,ind)) ->
- let indhd,indargs = decompose_app sigma ind in
- try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) }
- with e when CErrors.noncritical e ->
+ let indhd,indargs = decompose_app sigma ind in
+ try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) }
+ with e when CErrors.noncritical e ->
error "Cannot find the inductive type of the inductive scheme."
let compute_scheme_signature evd scheme names_info ind_type_guess =
@@ -4096,23 +4096,23 @@ let compute_scheme_signature evd scheme names_info ind_type_guess =
let cond, check_concl =
match scheme.indarg with
| Some (LocalDef _) ->
- error "Strange letin, cannot recognize an induction scheme."
+ error "Strange letin, cannot recognize an induction scheme."
| None -> (* Non standard scheme *)
- let cond hd = EConstr.eq_constr evd hd ind_type_guess && not scheme.farg_in_concl
- in (cond, fun _ _ -> ())
+ let cond hd = EConstr.eq_constr evd hd ind_type_guess && not scheme.farg_in_concl
+ in (cond, fun _ _ -> ())
| Some (LocalAssum (_,ind)) -> (* Standard scheme from an inductive type *)
- let indhd,indargs = decompose_app evd ind in
- let cond hd = EConstr.eq_constr evd hd indhd in
- let check_concl is_pred p =
- (* Check again conclusion *)
- let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f == IndArg in
- let ind_is_ok =
- List.equal (fun c1 c2 -> EConstr.eq_constr evd c1 c2)
- (List.lastn scheme.nargs indargs)
- (Context.Rel.to_extended_list mkRel 0 scheme.args) in
- if not (ccl_arg_ok && ind_is_ok) then
- error_ind_scheme "the conclusion of"
- in (cond, check_concl)
+ let indhd,indargs = decompose_app evd ind in
+ let cond hd = EConstr.eq_constr evd hd indhd in
+ let check_concl is_pred p =
+ (* Check again conclusion *)
+ let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f == IndArg in
+ let ind_is_ok =
+ List.equal (fun c1 c2 -> EConstr.eq_constr evd c1 c2)
+ (List.lastn scheme.nargs indargs)
+ (Context.Rel.to_extended_list mkRel 0 scheme.args) in
+ if not (ccl_arg_ok && ind_is_ok) then
+ error_ind_scheme "the conclusion of"
+ in (cond, check_concl)
in
let is_pred n c =
let hd = fst (decompose_app evd c) in
@@ -4124,27 +4124,27 @@ let compute_scheme_signature evd scheme names_info ind_type_guess =
let rec check_branch p c =
match EConstr.kind evd c with
| Prod (_,t,c) ->
- (is_pred p t, true, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c
+ (is_pred p t, true, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c
| LetIn (_,_,_,c) ->
- (OtherArg, false, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c
+ (OtherArg, false, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c
| _ when is_pred p c == IndArg -> []
| _ -> raise Exit
in
let rec find_branches p lbrch =
match lbrch with
| LocalAssum (_,t) :: brs ->
- (try
- let lchck_brch = check_branch p t in
- let n = List.fold_left
- (fun n (b,_,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in
- let recvarname, hyprecname, avoid =
- make_up_names n scheme.indref names_info in
- let namesign =
- List.map (fun (b,is_assum,dep) ->
- (b,is_assum,dep,if b == IndArg then hyprecname else recvarname))
- lchck_brch in
- (avoid,namesign) :: find_branches (p+1) brs
- with Exit-> error_ind_scheme "the branches of")
+ (try
+ let lchck_brch = check_branch p t in
+ let n = List.fold_left
+ (fun n (b,_,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in
+ let recvarname, hyprecname, avoid =
+ make_up_names n scheme.indref names_info in
+ let namesign =
+ List.map (fun (b,is_assum,dep) ->
+ (b,is_assum,dep,if b == IndArg then hyprecname else recvarname))
+ lchck_brch in
+ (avoid,namesign) :: find_branches (p+1) brs
+ with Exit-> error_ind_scheme "the branches of")
| LocalDef _ :: _ -> error_ind_scheme "the branches of"
| [] -> check_concl is_pred p; []
in
@@ -4210,12 +4210,12 @@ let find_induction_type isrec elim hyp0 gl =
(* We drop the scheme waiting to know if it is dependent *)
scheme, ElimOver (isrec,hyp0)
| Some e ->
- let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
- let scheme = compute_elim_sig sigma ~elimc elimt in
- if Option.is_empty scheme.indarg then error "Cannot find induction type";
- let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in
+ let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
+ let scheme = compute_elim_sig sigma ~elimc elimt in
+ if Option.is_empty scheme.indarg then error "Cannot find induction type";
+ let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in
let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in
- scheme, ElimUsing (elim,indsign)
+ scheme, ElimUsing (elim,indsign)
in
match scheme.indref with
| None -> error_ind_scheme ""
@@ -4251,9 +4251,9 @@ let recolle_clenv i params args elimclause gl =
let lindmv =
Array.map
(fun x ->
- match EConstr.kind elimclause.evd x with
- | Meta mv -> mv
- | _ -> user_err ~hdr:"elimination_clause"
+ match EConstr.kind elimclause.evd x with
+ | Meta mv -> mv
+ | _ -> user_err ~hdr:"elimination_clause"
(str "The type of the elimination clause is not well-formed."))
arr in
let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in
@@ -4399,18 +4399,18 @@ let clear_unselected_context id inhyps cls =
Proofview.Goal.enter begin fun gl ->
if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) &&
cls.concl_occs == NoOccurrences
- then user_err
+ then user_err
(str "Conclusion must be mentioned: it depends on " ++ Id.print id
++ str ".");
match cls.onhyps with
| Some hyps ->
let to_erase d =
let id' = NamedDecl.get_id d in
- if Id.List.mem id' inhyps then (* if selected, do not erase *) None
- else
- (* erase if not selected and dependent on id or selected hyps *)
- let test id = occur_var_in_decl (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id d in
- if List.exists test (id::inhyps) then Some id' else None in
+ if Id.List.mem id' inhyps then (* if selected, do not erase *) None
+ else
+ (* erase if not selected and dependent on id or selected hyps *)
+ let test id = occur_var_in_decl (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id d in
+ if List.exists test (id::inhyps) then Some id' else None in
let ids = List.map_filter to_erase (Proofview.Goal.hyps gl) in
clear ids
| None -> Proofview.tclUNIT ()
@@ -4591,7 +4591,7 @@ let induction_gen clear_flag isrec with_evars elim
isrec with_evars info_arg elim id arg t inhyps cls
(induction_with_atomization_of_ind_arg
isrec with_evars elim names id)
- end
+ end
(* Induction on a list of arguments. First make induction arguments
atomic (using letins), then do induction. The specificity here is
@@ -4610,32 +4610,32 @@ let induction_gen_l isrec with_evars elim names lc =
| [] -> Proofview.tclUNIT ()
| c::l' ->
Proofview.tclEVARMAP >>= fun sigma ->
- match EConstr.kind sigma c with
- | Var id when not (mem_named_context_val id (Global.named_context_val ()))
- && not with_evars ->
+ match EConstr.kind sigma c with
+ | Var id when not (mem_named_context_val id (Global.named_context_val ()))
+ && not with_evars ->
let () = newlc:= id::!newlc in
- atomize_list l'
+ atomize_list l'
- | _ ->
+ | _ ->
Proofview.Goal.enter begin fun gl ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
let sigma = Tacmach.New.project gl in
Proofview.tclENV >>= fun env ->
let x =
- id_of_name_using_hdchar env sigma (type_of c) Anonymous in
+ id_of_name_using_hdchar env sigma (type_of c) Anonymous in
let id = new_fresh_id Id.Set.empty x gl in
- let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
+ let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
let () = newlc:=id::!newlc in
- Tacticals.New.tclTHEN
- (letin_tac None (Name id) c None allHypsAndConcl)
- (atomize_list newl')
+ Tacticals.New.tclTHEN
+ (letin_tac None (Name id) c None allHypsAndConcl)
+ (atomize_list newl')
end in
Tacticals.New.tclTHENLIST
[
(atomize_list lc);
(Proofview.tclUNIT () >>= fun () -> (* ensure newlc has been computed *)
- induction_without_atomization isrec with_evars elim names !newlc)
+ induction_without_atomization isrec with_evars elim names !newlc)
]
(* Induction either over a term, over a quantified premisse, or over
@@ -4657,8 +4657,8 @@ let induction_destruct isrec with_evars (lc,elim) =
if not (Option.is_empty cls) then error "'in' clause not supported here.";
let _,c = force_destruction_arg false env sigma c in
onInductionArg
- (fun _clear_flag c ->
- induction_gen_l isrec with_evars elim names
+ (fun _clear_flag c ->
+ induction_gen_l isrec with_evars elim names
[with_no_bindings c,eqname]) c
| _ ->
(* standard induction *)
@@ -4694,12 +4694,12 @@ let induction_destruct isrec with_evars (lc,elim) =
let newlc =
List.map (fun (x,(eqn,names),cls) ->
if cls != None then error "'in' clause not yet supported here.";
- match x with (* FIXME: should we deal with ElimOnIdent? *)
+ match x with (* FIXME: should we deal with ElimOnIdent? *)
| _clear_flag,ElimOnConstr x ->
if eqn <> None then error "'eqn' clause not supported here.";
(with_no_bindings x,names)
- | _ -> error "Don't know where to find some argument.")
- lc in
+ | _ -> error "Don't know where to find some argument.")
+ lc in
(* Check that "as", if any, is given only on the last argument *)
let names,rest = List.sep_last (List.map snd newlc) in
if List.exists (fun n -> not (Option.is_empty n)) rest then
@@ -4729,10 +4729,10 @@ let elim_scheme_type elim t =
match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with
| Meta mv ->
let clause' =
- (* t is inductive, then CUMUL or CONV is irrelevant *)
- clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
+ (* t is inductive, then CUMUL or CONV is irrelevant *)
+ clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
(clenv_meta_type clause mv) clause in
- Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
+ Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
| _ -> anomaly (Pp.str "elim_scheme_type.")
end
@@ -4815,7 +4815,7 @@ let prove_symmetry hdcncl eq_kind =
(Tacticals.New.tclTHENLIST
[ intro;
Tacticals.New.onLastHyp simplest_case;
- one_constructor 1 NoBindings ])
+ one_constructor 1 NoBindings ])
let match_with_equation sigma c =
Proofview.tclENV >>= fun env ->
@@ -4915,9 +4915,9 @@ let prove_transitivity hdcncl eq_kind t =
Tacticals.New.tclTHENFIRST (cut eq2)
(Tacticals.New.tclTHENFIRST (cut eq1)
(Tacticals.New.tclTHENLIST
- [ Tacticals.New.tclDO 2 intro;
- Tacticals.New.onLastHyp simplest_case;
- assumption ]))
+ [ Tacticals.New.tclDO 2 intro;
+ Tacticals.New.onLastHyp simplest_case;
+ assumption ]))
end
let transitivity_red allowred t =
@@ -4933,8 +4933,8 @@ let transitivity_red allowred t =
Tacticals.New.tclTHEN
(convert_concl ~check:false concl DEFAULTcast)
(match t with
- | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply
- | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
+ | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply
+ | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
| None,eq,eq_kind ->
match t with
| None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
@@ -4981,8 +4981,8 @@ let unify ?(state=TransparentState.full) x y =
try
let core_flags =
{ (default_unify_flags ()).core_unify_flags with
- modulo_delta = state;
- modulo_conv_on_closed_terms = Some state} in
+ modulo_delta = state;
+ modulo_conv_on_closed_terms = Some state} in
(* What to do on merge and subterm flags?? *)
let flags = { (default_unify_flags ()) with
core_unify_flags = core_flags;
@@ -5021,7 +5021,7 @@ module New = struct
let reduce_after_refine =
reduce
(Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;
- rZeta=false;rDelta=false;rConst=[]})
+ rZeta=false;rDelta=false;rConst=[]})
{onhyps = Some []; concl_occs = AllOccurrences }
let refine ~typecheck c =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d3c800df20..308399c5db 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -221,12 +221,12 @@ val eapply_with_bindings : constr with_bindings -> unit Proofview.tactic
val cut_and_apply : constr -> unit Proofview.tactic
val apply_in :
- advanced_flag -> evars_flag -> Id.t ->
+ advanced_flag -> evars_flag -> Id.t ->
(clear_flag * constr with_bindings CAst.t) list ->
intro_pattern option -> unit Proofview.tactic
val apply_delayed_in :
- advanced_flag -> evars_flag -> Id.t ->
+ advanced_flag -> evars_flag -> Id.t ->
(clear_flag * delayed_open_constr_with_bindings CAst.t) list ->
intro_pattern option -> unit Proofview.tactic
@@ -270,9 +270,9 @@ type elim_scheme = {
args: rel_context; (** (xni, Ti_ni) ... (x1, Ti_1) *)
nargs: int; (** number of arguments *)
indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni)
- if HI is in premisses, None otherwise *)
+ if HI is in premisses, None otherwise *)
concl: types; (** Qi x1...xni HI (f...), HI and (f...)
- are optional and mutually exclusive *)
+ are optional and mutually exclusive *)
indarg_in_concl: bool; (** true if HI appears at the end of conclusion *)
farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *)
}
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 58db147b10..7f2a6f94b5 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -66,8 +66,8 @@ struct
| DInt _ -> str "INT"
| DFloat _ -> str "FLOAT"
| DCons ((t,dopt),tl) -> f t ++ (match dopt with
- Some t' -> str ":=" ++ f t'
- | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl
+ Some t' -> str ":=" ++ f t'
+ | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl
| DNil -> str "[]"
(*
@@ -82,9 +82,9 @@ struct
| DApp (t,u) -> DApp (f t,f u)
| DCase (ci,p,c,bl) -> DCase (ci, f p, f c, Array.map f bl)
| DFix (ia,i,ta,ca) ->
- DFix (ia,i,Array.map f ta,Array.map f ca)
+ DFix (ia,i,Array.map f ta,Array.map f ca)
| DCoFix(i,ta,ca) ->
- DCoFix (i,Array.map f ta,Array.map f ca)
+ DCoFix (i,Array.map f ta,Array.map f ca)
| DCons ((t,topt),u) -> DCons ((f t,Option.map f topt), f u)
let compare_ci ci1 ci2 =
@@ -175,9 +175,9 @@ struct
| DApp (t,u) -> f (f acc t) u
| DCase (ci,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
| DFix (ia,i,ta,ca) ->
- Array.fold_left f (Array.fold_left f acc ta) ca
+ Array.fold_left f (Array.fold_left f acc ta) ca
| DCoFix(i,ta,ca) ->
- Array.fold_left f (Array.fold_left f acc ta) ca
+ Array.fold_left f (Array.fold_left f acc ta) ca
| DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u
let choose f = function
@@ -199,17 +199,17 @@ struct
match c1,c2 with
| (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _
| DInt _, DInt _ | DFloat _, DFloat _) -> acc
- | (DCtx (c1,t1), DCtx (c2,t2)
- | DApp (c1,t1), DApp (c2,t2)
- | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2
- | DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) ->
- Array.fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2
- | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
- Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
- | DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) ->
- Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
- | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
- f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
+ | (DCtx (c1,t1), DCtx (c2,t2)
+ | DApp (c1,t1), DApp (c2,t2)
+ | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2
+ | DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) ->
+ Array.fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2
+ | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
+ Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
+ | DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) ->
+ Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
+ | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
+ f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
| (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
| DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _), _ -> assert false
@@ -220,18 +220,18 @@ struct
match c1,c2 with
| (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _
| DInt _, DInt _ | DFloat _, DFloat _) as cc ->
- let (c,_) = cc in c
- | DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2)
- | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2)
- | DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2)
- | DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) ->
- DCase (ci, f p1 p2, f c1 c2, Array.map2 f bl1 bl2)
- | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
- DFix (ia,i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
- | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) ->
- DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
- | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
- DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
+ let (c,_) = cc in c
+ | DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2)
+ | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2)
+ | DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2)
+ | DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) ->
+ DCase (ci, f p1 p2, f c1 c2, Array.map2 f bl1 bl2)
+ | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
+ DFix (ia,i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
+ | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) ->
+ DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
+ | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
+ DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
| (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
| DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _), _ -> assert false
@@ -274,8 +274,8 @@ module Make =
struct
module TDnet : Dnet.S with type ident=Ident.t
- and type 'a structure = 'a DTerm.t
- and type meta = int
+ and type 'a structure = 'a DTerm.t
+ and type meta = int
= Dnet.Make(DTerm)(Ident)(Int)
type t = TDnet.t
@@ -328,7 +328,7 @@ struct
| App (f,ca) ->
Array.fold_left (fun c a -> Term (DApp (c,a)))
(pat_of_constr f) (Array.map pat_of_constr ca)
- | Proj (p,c) ->
+ | Proj (p,c) ->
Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c))
| Int i -> Term (DInt i)
| Float f -> Term (DFloat f)
@@ -392,16 +392,16 @@ struct
let dpat = under_prod (empty_ctx dpat) in
TDnet.Idset.fold
(fun id acc ->
- let c_id = Opt.reduce (Ident.constr_of id) in
- let c_id = EConstr.of_constr c_id in
- let (ctx,wc) =
+ let c_id = Opt.reduce (Ident.constr_of id) in
+ let c_id = EConstr.of_constr c_id in
+ let (ctx,wc) =
try Termops.align_prod_letin Evd.empty whole_c c_id (* FIXME *)
- with Invalid_argument _ -> [],c_id in
- let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
- try
+ with Invalid_argument _ -> [],c_id in
+ let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
+ try
let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in
id :: acc
- with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc
+ with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc
) (TDnet.find_match dpat dn) []
(*
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:15:56 +0000