aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml22
-rw-r--r--plugins/ltac/extraargs.mlg4
-rw-r--r--plugins/ltac/extratactics.mlg50
-rw-r--r--plugins/ltac/g_ltac.mlg32
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg2
-rw-r--r--plugins/ltac/g_tactic.mlg156
-rw-r--r--plugins/ltac/pltac.ml2
-rw-r--r--plugins/ltac/rewrite.ml1103
-rw-r--r--plugins/ltac/rewrite.mli12
-rw-r--r--plugins/ltac/taccoerce.ml10
-rw-r--r--plugins/ltac/tacenv.ml2
-rw-r--r--plugins/ltac/tacintern.ml34
-rw-r--r--plugins/ltac/tacinterp.ml74
-rw-r--r--plugins/ltac/tacsubst.ml10
-rw-r--r--plugins/ltac/tactic_matching.ml6
-rw-r--r--plugins/ltac/tactic_option.ml14
-rw-r--r--plugins/ltac/tactic_option.mli2
18 files changed, 769 insertions, 768 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 5211bedd46..c87eb7c3c9 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -51,20 +51,20 @@ let instantiate_tac n c ido =
let sigma = gl.sigma in
let evl =
match ido with
- ConclLocation () -> evar_list sigma (pf_concl gl)
+ ConclLocation () -> evar_list sigma (pf_concl gl)
| HypLocation (id,hloc) ->
let decl = Environ.lookup_named id (pf_env gl) in
- match hloc with
- InHyp ->
- (match decl with
+ match hloc with
+ InHyp ->
+ (match decl with
| LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ)
- | _ -> user_err Pp.(str "Please be more specific: in type or value?"))
- | InHypTypeOnly ->
- evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
- | InHypValueOnly ->
- (match decl with
+ | _ -> user_err Pp.(str "Please be more specific: in type or value?"))
+ | InHypTypeOnly ->
+ evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
+ | InHypValueOnly ->
+ (match decl with
| LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
- | _ -> user_err Pp.(str "Not a defined hypothesis.")) in
+ | _ -> user_err Pp.(str "Not a defined hypothesis.")) in
if List.length evl < n then
user_err Pp.(str "Not enough uninstantiated existential variables.");
if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
@@ -97,7 +97,7 @@ let let_evar name typ =
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tactics.pose_tac (Name.Name id) evar)
end
-
+
let hget_evar n =
let open EConstr in
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index e6e6e29d4f..bab6bfd78e 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -115,8 +115,8 @@ let interp_occs ist gl l =
match l with
| ArgArg x -> x
| ArgVar ({ CAst.v = id } as locid) ->
- (try int_list_of_VList (Id.Map.find id ist.lfun)
- with Not_found | CannotCoerceTo _ -> [interp_int ist locid])
+ (try int_list_of_VList (Id.Map.find id ist.lfun)
+ with Not_found | CannotCoerceTo _ -> [interp_int ist locid])
let interp_occs ist gl l =
Tacmach.project gl , interp_occs ist gl l
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index f7215a9d13..a9e5271e81 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -204,7 +204,7 @@ TACTIC EXTEND dependent_rewrite
END
(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to
- "replace u with t" or "enough (t=u) as <-" and
+ "replace u with t" or "enough (t=u) as <-" and
"cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *)
TACTIC EXTEND cut_rewrite
@@ -314,8 +314,8 @@ let add_rewrite_hint ~poly bases ort t lcsr =
let ctx =
let ctx = UState.context_set ctx in
if poly then ctx
- else (* This is a global universe context that shouldn't be
- refreshed at every use of the hint, declare it globally. *)
+ else (* This is a global universe context that shouldn't be
+ refreshed at every use of the hint, declare it globally. *)
(Declare.declare_universe_context ~poly:false ctx;
Univ.ContextSet.empty)
in
@@ -595,7 +595,7 @@ TACTIC EXTEND dep_generalize_eqs_vars
| ["dependent" "generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~force_dep:true ~generalize_vars:true id }
END
-(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T]
+(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T]
where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated
during dependent induction. For internal use. *)
@@ -613,17 +613,17 @@ END
{
-let subst_var_with_hole occ tid t =
+let subst_var_with_hole occ tid t =
let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
let locref = ref 0 in
let rec substrec x = match DAst.get x with
| GVar id ->
- if Id.equal id tid
+ if Id.equal id tid
then
- (decr occref;
- if Int.equal !occref 0 then x
+ (decr occref;
+ if Int.equal !occref 0 then x
else
- (incr locref;
+ (incr locref;
DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
GHole (Evar_kinds.QuestionMark {
Evar_kinds.qm_obligation=Evar_kinds.Define true;
@@ -648,7 +648,7 @@ let subst_hole_with_term occ tc t =
decr occref;
if Int.equal !occref 0 then tc
else
- (incr locref;
+ (incr locref;
DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
GHole (Evar_kinds.QuestionMark {
Evar_kinds.qm_obligation=Evar_kinds.Define true;
@@ -670,7 +670,7 @@ let hResolve id c occ t =
let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in
let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in
let rec resolve_hole t_hole =
- try
+ try
Pretyping.understand env sigma t_hole
with
| Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
@@ -686,7 +686,7 @@ let hResolve id c occ t =
end
let hResolve_auto id c t =
- let rec resolve_auto n =
+ let rec resolve_auto n =
try
hResolve id c n t
with
@@ -727,7 +727,7 @@ exception Found of unit Proofview.tactic
let rewrite_except h =
Proofview.Goal.enter begin fun gl ->
let hyps = Tacmach.New.pf_ids_of_hyps gl in
- Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else
+ Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else
Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
hyps
end
@@ -750,9 +750,9 @@ let mkCaseEq a : unit Proofview.tactic =
(* FIXME: this looks really wrong. Does anybody really use
this tactic? *)
let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in
- change_concl c
+ change_concl c
end;
- simplest_case a]
+ simplest_case a]
end
@@ -769,8 +769,8 @@ let case_eq_intros_rewrite x =
let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in
Tacticals.New.tclTHENLIST [
Tacticals.New.tclDO (n'-n-1) intro;
- introduction h;
- rewrite_except h]
+ introduction h;
+ rewrite_except h]
end
]
end
@@ -781,14 +781,14 @@ let rec find_a_destructable_match sigma t =
let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in
match EConstr.kind sigma t with
| Case (_,_,x,_) when closed0 sigma x ->
- if isVar sigma x then
- (* TODO check there is no rel n. *)
- raise (Found (Tacinterp.eval_tactic dest))
- else
- (* let _ = Pp.msgnl (Printer.pr_lconstr x) in *)
- raise (Found (case_eq_intros_rewrite x))
+ if isVar sigma x then
+ (* TODO check there is no rel n. *)
+ raise (Found (Tacinterp.eval_tactic dest))
+ else
+ (* let _ = Pp.msgnl (Printer.pr_lconstr x) in *)
+ raise (Found (case_eq_intros_rewrite x))
| _ -> EConstr.iter sigma (fun c -> find_a_destructable_match sigma c) t
-
+
let destauto t =
Proofview.tclEVARMAP >>= fun sigma ->
@@ -796,7 +796,7 @@ let destauto t =
Tacticals.New.tclZEROMSG (str "No destructable match found")
with Found tac -> tac
-let destauto_in id =
+let destauto_in id =
Proofview.Goal.enter begin fun gl ->
let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index cab8ed0a55..81a6651745 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -69,8 +69,8 @@ let test_bracket_ident =
| KEYWORD "[" ->
(match stream_nth 1 strm with
| IDENT _ -> ()
- | _ -> raise Stream.Failure)
- | _ -> raise Stream.Failure)
+ | _ -> raise Stream.Failure)
+ | _ -> raise Stream.Failure)
(* Tactics grammar rules *)
@@ -110,11 +110,11 @@ GRAMMAR EXTEND Gram
| ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) }
| ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> {
let (first,tail) = tg in
- match l , tail with
+ match l , tail with
| false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
- | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last)
+ | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last)
| false , None -> TacThen (ta0,TacDispatch first)
- | true , None -> TacThens (ta0,first) } ]
+ | true , None -> TacThens (ta0,first) } ]
| "3" RIGHTA
[ IDENT "try"; ta = tactic_expr -> { TacTry ta }
| IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) }
@@ -148,12 +148,12 @@ GRAMMAR EXTEND Gram
| b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
{ TacMatch (b,c,mrl) }
| IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
- { TacFirst l }
+ { TacFirst l }
| IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
- { TacSolve l }
+ { TacSolve l }
| IDENT "idtac"; l = LIST0 message_token -> { TacId l }
| g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
- l = LIST0 message_token -> { TacFail (g,n,l) }
+ l = LIST0 message_token -> { TacFail (g,n,l) }
| st = simple_tactic -> { st }
| a = tactic_arg -> { TacArg(CAst.make ~loc a) }
| r = reference; la = LIST0 tactic_arg_compat ->
@@ -247,12 +247,12 @@ GRAMMAR EXTEND Gram
| na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) }
| na = name; ":="; mpv = match_pattern ->
{ let t, ty =
- match mpv with
- | Term t -> (match t with
- | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty)
- | _ -> mpv, None)
- | _ -> mpv, None
- in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) }
+ match mpv with
+ | Term t -> (match t with
+ | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty)
+ | _ -> mpv, None)
+ | _ -> mpv, None
+ in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) }
] ]
;
match_context_rule:
@@ -337,9 +337,9 @@ GRAMMAR EXTEND Gram
| g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSubproof g } ] ]
;
command:
- [ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
+ [ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] ->
- { Vernacexpr.VernacProof (Some (in_tac ta), l) }
+ { Vernacexpr.VernacProof (Some (in_tac ta), l) }
| IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] ->
{ Vernacexpr.VernacProof (ta,Some l) } ] ]
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 61cc77c42a..5a7a634ed0 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -20,7 +20,7 @@ open Stdarg
open Tacarg
open Extraargs
-let (set_default_tactic, get_default_tactic, print_default_tactic) =
+let (set_default_tactic, get_default_tactic, print_default_tactic) =
Tactic_option.declare_tactic_option "Program tactic"
let () =
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index d25448b5cb..2209edcbb4 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -71,7 +71,7 @@ END
type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast
type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
-let interp_strategy ist gl s =
+let interp_strategy ist gl s =
let sigma = project gl in
sigma, strategy_of_ast s
let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 1b00a93834..d82eadcfc7 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -45,10 +45,10 @@ let test_lpar_id_coloneq =
(match stream_nth 1 strm with
| IDENT _ ->
(match stream_nth 2 strm with
- | KEYWORD ":=" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ | KEYWORD ":=" -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
(* Hack to recognize "(x)" *)
let test_lpar_id_rpar =
@@ -59,10 +59,10 @@ let test_lpar_id_rpar =
(match stream_nth 1 strm with
| IDENT _ ->
(match stream_nth 2 strm with
- | KEYWORD ")" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ | KEYWORD ")" -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
(* idem for (x:=t) and (1:=t) *)
let test_lpar_idnum_coloneq =
@@ -86,22 +86,22 @@ let check_for_coloneq =
Pcoq.Entry.of_parser "lpar_id_colon"
(fun _ strm ->
let rec skip_to_rpar p n =
- match List.last (Stream.npeek n strm) with
+ match List.last (Stream.npeek n strm) with
| KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
| KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1)
- | KEYWORD "." -> err ()
- | _ -> skip_to_rpar p (n+1) in
+ | KEYWORD "." -> err ()
+ | _ -> skip_to_rpar p (n+1) in
let rec skip_names n =
- match List.last (Stream.npeek n strm) with
+ match List.last (Stream.npeek n strm) with
| IDENT _ | KEYWORD "_" -> skip_names (n+1)
- | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *)
- | _ -> err () in
+ | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *)
+ | _ -> err () in
let rec skip_binders n =
- match List.last (Stream.npeek n strm) with
+ match List.last (Stream.npeek n strm) with
| KEYWORD "(" -> skip_binders (skip_names (n+1))
| IDENT _ | KEYWORD "_" -> skip_binders (n+1)
- | KEYWORD ":=" -> ()
- | _ -> err () in
+ | KEYWORD ":=" -> ()
+ | _ -> err () in
match stream_nth 0 strm with
| KEYWORD "(" -> skip_binders 2
| _ -> err ())
@@ -110,8 +110,8 @@ let lookup_at_as_comma =
Pcoq.Entry.of_parser "lookup_at_as_comma"
(fun _ strm ->
match stream_nth 0 strm with
- | KEYWORD (","|"at"|"as") -> ()
- | _ -> err ())
+ | KEYWORD (","|"at"|"as") -> ()
+ | _ -> err ())
open Constr
open Prim
@@ -164,7 +164,7 @@ let mkTacCase with_evar = function
| ic ->
if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
then
- user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported.");
+ user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported.");
TacInductionDestruct (false,with_evar,ic)
let rec mkCLambdaN_simple_loc ?loc bll c =
@@ -188,7 +188,7 @@ let merge_occurrences loc cl = function
| None ->
if Locusops.clause_with_generic_occurrences cl then (None, cl)
else
- user_err ~loc (str "Found an \"at\" clause without \"with\" clause.")
+ user_err ~loc (str "Found an \"at\" clause without \"with\" clause.")
| Some (occs, p) ->
let ans = match occs with
| AllOccurrences -> cl
@@ -264,7 +264,7 @@ GRAMMAR EXTEND Gram
occs_nums:
[ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
| "-"; n = nat_or_var; nl = LIST0 int_or_var ->
- (* have used int_or_var instead of nat_or_var for compatibility *)
+ (* have used int_or_var instead of nat_or_var for compatibility *)
{ AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ]
;
occs:
@@ -296,12 +296,12 @@ GRAMMAR EXTEND Gram
tc = LIST1 simple_intropattern SEP "," ; ")" ->
{ IntroAndPattern (si::tc) }
| "("; si = simple_intropattern; "&";
- tc = LIST1 simple_intropattern SEP "&" ; ")" ->
- (* (A & B & C) is translated into (A,(B,C)) *)
- { let rec pairify = function
- | ([]|[_]|[_;_]) as l -> l
+ tc = LIST1 simple_intropattern SEP "&" ; ")" ->
+ (* (A & B & C) is translated into (A,(B,C)) *)
+ { let rec pairify = function
+ | ([]|[_]|[_;_]) as l -> l
| t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
- in IntroAndPattern (pairify (si::tc)) } ] ]
+ in IntroAndPattern (pairify (si::tc)) } ] ]
;
equality_intropattern:
[ [ "->" -> { IntroRewrite true }
@@ -439,7 +439,7 @@ GRAMMAR EXTEND Gram
[ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
| -> { None } ] ]
;
- orient:
+ orient_rw:
[ [ "->" -> { true }
| "<-" -> { false }
| -> { true } ] ]
@@ -451,10 +451,10 @@ GRAMMAR EXTEND Gram
] ]
;
fixdecl:
- [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot;
+ [ [ "("; id = ident; bl=LIST0 simple_binder; ann=struct_annot;
":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ]
;
- fixannot:
+ struct_annot:
[ [ "{"; IDENT "struct"; id=name; "}" -> { Some id }
| -> { None } ] ]
;
@@ -506,7 +506,7 @@ GRAMMAR EXTEND Gram
] ]
;
oriented_rewriter :
- [ [ b = orient; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ]
+ [ [ b = orient_rw; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ]
;
induction_clause:
[ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
@@ -550,24 +550,24 @@ GRAMMAR EXTEND Gram
| IDENT "case"; icl = induction_clause_list -> { TacAtom (CAst.make ~loc @@ mkTacCase false icl) }
| IDENT "ecase"; icl = induction_clause_list -> { TacAtom (CAst.make ~loc @@ mkTacCase true icl) }
| "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
- { TacAtom (CAst.make ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) }
+ { TacAtom (CAst.make ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) }
| "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
- { TacAtom (CAst.make ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) }
+ { TacAtom (CAst.make ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) }
| IDENT "pose"; bl = bindings_with_parameters ->
- { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) }
+ { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) }
| IDENT "pose"; b = constr; na = as_name ->
- { TacAtom (CAst.make ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) }
+ { TacAtom (CAst.make ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) }
| IDENT "epose"; bl = bindings_with_parameters ->
- { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) }
+ { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) }
| IDENT "epose"; b = constr; na = as_name ->
- { TacAtom (CAst.make ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) }
+ { TacAtom (CAst.make ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) }
| IDENT "set"; bl = bindings_with_parameters; p = clause_dft_concl ->
- { let (id,c) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) }
+ { let (id,c) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) }
| IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
{ TacAtom (CAst.make ~loc @@ TacLetTac (false,na,c,p,true,None)) }
| IDENT "eset"; bl = bindings_with_parameters; p = clause_dft_concl ->
- { let (id,c) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) }
+ { let (id,c) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) }
| IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl ->
{ TacAtom (CAst.make ~loc @@ TacLetTac (true,na,c,p,true,None)) }
| IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
@@ -579,51 +579,51 @@ GRAMMAR EXTEND Gram
(* Alternative syntax for "pose proof c as id" *)
| IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
- c = lconstr; ")" ->
+ c = lconstr; ")" ->
{ let { CAst.loc = loc; v = id } = lid in
TacAtom (CAst.make ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
- c = lconstr; ")" ->
+ c = lconstr; ")" ->
{ let { CAst.loc = loc; v = id } = lid in
TacAtom (CAst.make ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
(* Alternative syntax for "assert c as id by tac" *)
| IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":";
- c = lconstr; ")"; tac=by_tactic ->
+ c = lconstr; ")"; tac=by_tactic ->
{ let { CAst.loc = loc; v = id } = lid in
TacAtom (CAst.make ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":";
- c = lconstr; ")"; tac=by_tactic ->
+ c = lconstr; ")"; tac=by_tactic ->
{ let { CAst.loc = loc; v = id } = lid in
TacAtom (CAst.make ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
(* Alternative syntax for "enough c as id by tac" *)
| IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":";
- c = lconstr; ")"; tac=by_tactic ->
+ c = lconstr; ")"; tac=by_tactic ->
{ let { CAst.loc = loc; v = id } = lid in
TacAtom (CAst.make ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":";
- c = lconstr; ")"; tac=by_tactic ->
+ c = lconstr; ")"; tac=by_tactic ->
{ let { CAst.loc = loc; v = id } = lid in
TacAtom (CAst.make ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
- { TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) }
| IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
- { TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) }
| IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- { TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) }
| IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- { TacAtom (CAst.make ~loc @@ TacAssert (true,true,None,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (true,true,None,ipat,c)) }
| IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- { TacAtom (CAst.make ~loc @@ TacAssert (false,false,Some tac,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (false,false,Some tac,ipat,c)) }
| IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- { TacAtom (CAst.make ~loc @@ TacAssert (true,false,Some tac,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (true,false,Some tac,ipat,c)) }
| IDENT "generalize"; c = constr ->
- { TacAtom (CAst.make ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) }
+ { TacAtom (CAst.make ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) }
| IDENT "generalize"; c = constr; l = LIST1 constr ->
- { let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in
+ { let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in
TacAtom (CAst.make ~loc @@ TacGeneralize (List.map gen_everywhere (c::l))) }
| IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs;
na = as_name;
@@ -632,41 +632,41 @@ GRAMMAR EXTEND Gram
(* Derived basic tactics *)
| IDENT "induction"; ic = induction_clause_list ->
- { TacAtom (CAst.make ~loc @@ TacInductionDestruct (true,false,ic)) }
+ { TacAtom (CAst.make ~loc @@ TacInductionDestruct (true,false,ic)) }
| IDENT "einduction"; ic = induction_clause_list ->
- { TacAtom (CAst.make ~loc @@ TacInductionDestruct(true,true,ic)) }
+ { TacAtom (CAst.make ~loc @@ TacInductionDestruct(true,true,ic)) }
| IDENT "destruct"; icl = induction_clause_list ->
- { TacAtom (CAst.make ~loc @@ TacInductionDestruct(false,false,icl)) }
+ { TacAtom (CAst.make ~loc @@ TacInductionDestruct(false,false,icl)) }
| IDENT "edestruct"; icl = induction_clause_list ->
- { TacAtom (CAst.make ~loc @@ TacInductionDestruct(false,true,icl)) }
+ { TacAtom (CAst.make ~loc @@ TacInductionDestruct(false,true,icl)) }
(* Equality and inversion *)
| IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
- cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (false,l,cl,t)) }
+ cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (false,l,cl,t)) }
| IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
- cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (true,l,cl,t)) }
+ cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (true,l,cl,t)) }
| IDENT "dependent"; k =
- [ IDENT "simple"; IDENT "inversion" -> { SimpleInversion }
- | IDENT "inversion" -> { FullInversion }
- | IDENT "inversion_clear" -> { FullInversionClear } ];
- hyp = quantified_hypothesis;
- ids = as_or_and_ipat; co = OPT ["with"; c = constr -> { c } ] ->
- { TacAtom (CAst.make ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) }
+ [ IDENT "simple"; IDENT "inversion" -> { SimpleInversion }
+ | IDENT "inversion" -> { FullInversion }
+ | IDENT "inversion_clear" -> { FullInversionClear } ];
+ hyp = quantified_hypothesis;
+ ids = as_or_and_ipat; co = OPT ["with"; c = constr -> { c } ] ->
+ { TacAtom (CAst.make ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) }
| IDENT "simple"; IDENT "inversion";
- hyp = quantified_hypothesis; ids = as_or_and_ipat;
- cl = in_hyp_list ->
- { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) }
+ hyp = quantified_hypothesis; ids = as_or_and_ipat;
+ cl = in_hyp_list ->
+ { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) }
| IDENT "inversion";
- hyp = quantified_hypothesis; ids = as_or_and_ipat;
- cl = in_hyp_list ->
- { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) }
+ hyp = quantified_hypothesis; ids = as_or_and_ipat;
+ cl = in_hyp_list ->
+ { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) }
| IDENT "inversion_clear";
- hyp = quantified_hypothesis; ids = as_or_and_ipat;
- cl = in_hyp_list ->
- { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) }
+ hyp = quantified_hypothesis; ids = as_or_and_ipat;
+ cl = in_hyp_list ->
+ { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) }
| IDENT "inversion"; hyp = quantified_hypothesis;
- "using"; c = constr; cl = in_hyp_list ->
- { TacAtom (CAst.make ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) }
+ "using"; c = constr; cl = in_hyp_list ->
+ { TacAtom (CAst.make ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) }
(* Conversion *)
| IDENT "red"; cl = clause_dft_concl ->
@@ -696,8 +696,8 @@ GRAMMAR EXTEND Gram
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
| IDENT "change"; c = conversion; cl = clause_dft_concl ->
- { let (oc, c) = c in
- let p,cl = merge_occurrences loc cl oc in
+ { let (oc, c) = c in
+ let p,cl = merge_occurrences loc cl oc in
TacAtom (CAst.make ~loc @@ TacChange (true,p,c,cl)) }
| IDENT "change_no_check"; c = conversion; cl = clause_dft_concl ->
{ let (oc, c) = c in
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index e3042dc3cb..0e21115474 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -34,7 +34,7 @@ let int_or_var = make_gen_entry utactic "int_or_var"
let simple_intropattern =
make_gen_entry utactic "simple_intropattern"
let in_clause = make_gen_entry utactic "in_clause"
-let clause_dft_concl =
+let clause_dft_concl =
make_gen_entry utactic "clause"
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1493092f2f..5618fd7bc3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -76,7 +76,7 @@ let find_global dir s =
let gr = lazy (find_reference dir s) in
fun (evd,cstrs) ->
let (evd, c) = Evarutil.new_global evd (Lazy.force gr) in
- (evd, cstrs), c
+ (evd, cstrs), c
(** Utility for dealing with polymorphic applications *)
@@ -122,7 +122,7 @@ let app_poly_nocheck env evars f args =
let app_poly_sort b =
if b then app_poly_nocheck
else app_poly_check
-
+
let find_class_proof proof_type proof_method env evars carrier relation =
try
let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in
@@ -130,7 +130,7 @@ let find_class_proof proof_type proof_method env evars carrier relation =
if extends_undefined (goalevars evars) evars' then raise Not_found
else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |]
with e when Logic.catchable_exception e -> raise Not_found
-
+
(** Utility functions *)
module GlobalBindings (M : sig
@@ -146,7 +146,7 @@ end) = struct
let reflexive_type = find_global relation_classes "Reflexive"
let reflexive_proof = find_global relation_classes "reflexivity"
-
+
let symmetric_type = find_global relation_classes "Symmetric"
let symmetric_proof = find_global relation_classes "symmetry"
@@ -201,53 +201,53 @@ end) = struct
let get_symmetric_proof env = find_class_proof symmetric_type symmetric_proof env
let get_transitive_proof env = find_class_proof transitive_type transitive_proof env
- let mk_relation env evd a =
+ let mk_relation env evd a =
app_poly env evd relation [| a |]
(** Build an inferred signature from constraints on the arguments and expected output
relation *)
-
+
let build_signature evars env m (cstrs : (types * types option) option list)
(finalcstr : (types * types option) option) =
let mk_relty evars newenv ty obj =
match obj with
| None | Some (_, None) ->
- let evars, relty = mk_relation env evars ty in
- if closed0 (goalevars evars) ty then
- let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
- new_cstr_evar evars env' relty
- else new_cstr_evar evars newenv relty
+ let evars, relty = mk_relation env evars ty in
+ if closed0 (goalevars evars) ty then
+ let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
+ new_cstr_evar evars env' relty
+ else new_cstr_evar evars newenv relty
| Some (x, Some rel) -> evars, rel
in
let rec aux env evars ty l =
let t = Reductionops.whd_all env (goalevars evars) ty in
- match EConstr.kind (goalevars evars) t, l with
+ match EConstr.kind (goalevars evars) t, l with
| Prod (na, ty, b), obj :: cstrs ->
let b = Reductionops.nf_betaiota env (goalevars evars) b in
if noccurn (goalevars evars) 1 b (* non-dependent product *) then
let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
- let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
- let evars, relty = mk_relty evars env ty obj in
- let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
+ let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
+ let evars, relty = mk_relty evars env ty obj in
+ let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
- else
- let (evars, b, arg, cstrs) =
+ else
+ let (evars, b, arg, cstrs) =
aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs
- in
+ in
let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
let pred = mkLambda (na, ty, b) in
let liftarg = mkLambda (na, ty, arg) in
let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
- else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
- | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.")
- | _, [] ->
- (match finalcstr with
- | None | Some (_, None) ->
+ else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
+ | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.")
+ | _, [] ->
+ (match finalcstr with
+ | None | Some (_, None) ->
let t = Reductionops.nf_betaiota env (fst evars) ty in
- let evars, rel = mk_relty evars env t None in
- evars, t, rel, [t, Some rel]
- | Some (t, Some rel) -> evars, t, rel, [t, Some rel])
+ let evars, rel = mk_relty evars env t None in
+ evars, t, rel, [t, Some rel]
+ | Some (t, Some rel) -> evars, t, rel, [t, Some rel])
in aux env evars m cstrs
(** Folding/unfolding of the tactic constants. *)
@@ -278,30 +278,30 @@ end) = struct
let ap = is_Prop (goalevars evd) ta and bp = is_Prop (goalevars evd) tb in
if ap && bp then app_poly env evd impl [| a; b |], unfold_impl
else if ap then (* Domain in Prop, CoDomain in Type *)
- (app_poly env evd arrow [| a; b |]), unfold_impl
- (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *)
+ (app_poly env evd arrow [| a; b |]), unfold_impl
+ (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *)
else if bp then (* Dummy forall *)
(app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall
else (* None in Prop, use arrow *)
- (app_poly env evd arrow [| a; b |]), unfold_impl
+ (app_poly env evd arrow [| a; b |]), unfold_impl
let rec decomp_pointwise sigma n c =
if Int.equal n 0 then c
else
match EConstr.kind sigma c with
| App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
- decomp_pointwise sigma (pred n) relb
+ decomp_pointwise sigma (pred n) relb
| App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
- decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1]))
+ decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1]))
| _ -> invalid_arg "decomp_pointwise"
let rec apply_pointwise sigma rel = function
| arg :: args ->
(match EConstr.kind sigma rel with
| App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
- apply_pointwise sigma relb args
+ apply_pointwise sigma relb args
| App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
- apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args
+ apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args
| _ -> invalid_arg "apply_pointwise")
| [] -> rel
@@ -316,36 +316,36 @@ end) = struct
let lift_cstr env evars (args : constr list) c ty cstr =
let start evars env car =
match cstr with
- | None | Some (_, None) ->
- let evars, rel = mk_relation env evars car in
- new_cstr_evar evars env rel
+ | None | Some (_, None) ->
+ let evars, rel = mk_relation env evars car in
+ new_cstr_evar evars env rel
| Some (ty, Some rel) -> evars, rel
in
- let rec aux evars env prod n =
+ let rec aux evars env prod n =
if Int.equal n 0 then start evars env prod
else
let sigma = goalevars evars in
- match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with
+ match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with
| Prod (na, ty, b) ->
- if noccurn sigma 1 b then
- let b' = lift (-1) b in
- let evars, rb = aux evars env b' (pred n) in
- app_poly env evars pointwise_relation [| ty; b'; rb |]
- else
+ if noccurn sigma 1 b then
+ let b' = lift (-1) b in
+ let evars, rb = aux evars env b' (pred n) in
+ app_poly env evars pointwise_relation [| ty; b'; rb |]
+ else
let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in
- app_poly env evars forall_relation
+ app_poly env evars forall_relation
[| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]
- | _ -> raise Not_found
- in
+ | _ -> raise Not_found
+ in
let rec find env c ty = function
| [] -> None
| arg :: args ->
- try let evars, found = aux evars env ty (succ (List.length args)) in
- Some (evars, found, c, ty, arg :: args)
- with Not_found ->
+ try let evars, found = aux evars env ty (succ (List.length args)) in
+ Some (evars, found, c, ty, arg :: args)
+ with Not_found ->
let sigma = goalevars evars in
- let ty = Reductionops.whd_all env sigma ty in
- find env (mkApp (c, [| arg |])) (prod_applist sigma ty [arg]) args
+ let ty = Reductionops.whd_all env sigma ty in
+ find env (mkApp (c, [| arg |])) (prod_applist sigma ty [arg]) args
in find env c ty args
let unlift_cstr env sigma = function
@@ -357,18 +357,18 @@ end) = struct
match EConstr.kind sigma t with
| App (c, args) when Array.length args >= 2 ->
let head = if isApp sigma c then fst (destApp sigma c) else c in
- if Termops.is_global sigma (coq_eq_ref ()) head then None
- else
- (try
- let params, args = Array.chop (Array.length args - 2) args in
- let env' = push_rel_context rels env in
- let (evars, (evar, _)) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
- let evars, inst =
- app_poly env (evars,Evar.Set.empty)
- rewrite_relation_class [| evar; mkApp (c, params) |] in
- let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
- Some (it_mkProd_or_LetIn t rels)
- with e when CErrors.noncritical e -> None)
+ if Termops.is_global sigma (coq_eq_ref ()) head then None
+ else
+ (try
+ let params, args = Array.chop (Array.length args - 2) args in
+ let env' = push_rel_context rels env in
+ let (evars, (evar, _)) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
+ let evars, inst =
+ app_poly env (evars,Evar.Set.empty)
+ rewrite_relation_class [| evar; mkApp (c, params) |] in
+ let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
+ Some (it_mkProd_or_LetIn t rels)
+ with e when CErrors.noncritical e -> None)
| _ -> None
@@ -386,7 +386,7 @@ let type_app_poly env env evd f args =
module PropGlobal = struct
module Consts =
- struct
+ struct
let relation_classes = ["Coq"; "Classes"; "RelationClasses"]
let morphisms = ["Coq"; "Classes"; "Morphisms"]
let relation = ["Coq"; "Relations";"Relation_Definitions"], "relation"
@@ -399,15 +399,15 @@ module PropGlobal = struct
include G
include Consts
- let inverse env evd car rel =
+ let inverse env evd car rel =
type_app_poly env env evd coq_inverse [| car ; car; mkProp; rel |]
(* app_poly env evd coq_inverse [| car ; car; mkProp; rel |] *)
end
module TypeGlobal = struct
- module Consts =
- struct
+ module Consts =
+ struct
let relation_classes = ["Coq"; "Classes"; "CRelationClasses"]
let morphisms = ["Coq"; "Classes"; "CMorphisms"]
let relation = relation_classes, "crelation"
@@ -421,7 +421,7 @@ module TypeGlobal = struct
include Consts
- let inverse env (evd,cstrs) car rel =
+ let inverse env (evd,cstrs) car rel =
let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible evd in
app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
@@ -471,12 +471,12 @@ type hypinfo = {
holes : Clenv.hole list;
}
-let get_symmetric_proof b =
+let get_symmetric_proof b =
if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof
let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")
-let rec decompose_app_rel env evd t =
+let rec decompose_app_rel env evd t =
(* Head normalize for compatibility with the old meta mechanism *)
let t = Reductionops.whd_betaiota evd t in
match EConstr.kind evd t with
@@ -525,10 +525,10 @@ let decompose_applied_relation env sigma (c,l) =
match find_rel ctype with
| Some c -> c
| None ->
- let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
+ let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
- | Some c -> c
- | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.")
+ | Some c -> c
+ | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.")
let rewrite_db = "rewrite"
@@ -644,13 +644,13 @@ let solve_remaining_by env sigma holes by =
in
List.fold_left solve sigma indep
-let no_constraints cstrs =
+let no_constraints cstrs =
fun ev _ -> not (Evar.Set.mem ev cstrs)
let poly_inverse sort =
if sort then PropGlobal.inverse else TypeGlobal.inverse
-type rewrite_proof =
+type rewrite_proof =
| RewPrf of constr * constr
(** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *)
@@ -675,13 +675,13 @@ type rewrite_result =
| Success of rewrite_result_info
type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *)
- env : Environ.env ;
- unfresh : Id.Set.t; (* Unfresh names *)
- term1 : constr ;
- ty1 : types ; (* first term and its type (convertible to rew_from) *)
- cstr : (bool (* prop *) * constr option) ;
- evars : evars }
-
+ env : Environ.env ;
+ unfresh : Id.Set.t; (* Unfresh names *)
+ term1 : constr ;
+ ty1 : types ; (* first term and its type (convertible to rew_from) *)
+ cstr : (bool (* prop *) * constr option) ;
+ evars : evars }
+
type 'a pure_strategy = { strategy :
'a strategy_input ->
'a * rewrite_result (* the updated state and the "result" *) }
@@ -723,7 +723,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs)
let rew = { rew_evars; rew_prf; rew_car; rew_from = c1; rew_to = c2; } in
let rew = if l2r then rew else symmetry env sort rew in
Some rew
- with
+ with
| e when Class_tactics.catchable e -> None
| Reduction.NotConvertible -> None
@@ -740,7 +740,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t =
let rew = { rew_car = car; rew_from = c1; rew_to = c2; rew_prf; rew_evars; } in
let rew = if l2r then rew else symmetry env sort rew in
Some rew
- with
+ with
| e when Class_tactics.catchable e -> None
| Reduction.NotConvertible -> None
@@ -766,9 +766,9 @@ let get_rew_prf evars r = match r.rew_prf with
let evars, eq_refl = make_eq_refl evars in
let rel = mkApp (eq, [| r.rew_car |]) in
evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]),
- c, mkApp (rel, [| r.rew_from; r.rew_to |])))
+ c, mkApp (rel, [| r.rew_from; r.rew_to |])))
-let poly_subrelation sort =
+let poly_subrelation sort =
if sort then PropGlobal.subrelation else TypeGlobal.subrelation
let resolve_subrelation env avoid car rel sort prf rel' res =
@@ -778,8 +778,8 @@ let resolve_subrelation env avoid car rel sort prf rel' res =
let evars, subrel = new_cstr_evar evars env app in
let appsub = mkApp (subrel, [| res.rew_from ; res.rew_to ; prf |]) in
{ res with
- rew_prf = RewPrf (rel', appsub);
- rew_evars = evars }
+ rew_prf = RewPrf (rel', appsub);
+ rew_evars = evars }
let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars =
let evars, morph_instance, proj, sigargs, m', args, args' =
@@ -790,12 +790,12 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let morphargs', morphobjs' = Array.chop first args' in
let appm = mkApp(m, morphargs) in
let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
- let cstrs = List.map
- (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
- (Array.to_list morphobjs')
+ let cstrs = List.map
+ (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
+ (Array.to_list morphobjs')
in
(* Desired signature *)
- let evars, appmtype', signature, sigargs =
+ let evars, appmtype', signature, sigargs =
if b then PropGlobal.build_signature evars env appmtype cstrs cstr
else TypeGlobal.build_signature evars env appmtype cstrs cstr
in
@@ -803,16 +803,16 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let cl_args = [| appmtype' ; signature ; appm |] in
let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type env else TypeGlobal.proper_type env)
cl_args in
- let env' =
- let dosub, appsub =
- if b then PropGlobal.do_subrelation, PropGlobal.apply_subrelation
- else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation
+ let env' =
+ let dosub, appsub =
+ if b then PropGlobal.do_subrelation, PropGlobal.apply_subrelation
+ else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation
in
- EConstr.push_named
+ EConstr.push_named
(LocalDef (make_annot (Id.of_string "do_subrelation") Sorts.Relevant,
- snd (app_poly_sort b env evars dosub [||]),
- snd (app_poly_nocheck env evars appsub [||])))
- env
+ snd (app_poly_sort b env evars dosub [||]),
+ snd (app_poly_nocheck env evars appsub [||])))
+ env
in
let evars, morph = new_cstr_evar evars env' app in
evars, morph, morph, sigargs, appm, morphobjs, morphobjs'
@@ -820,31 +820,31 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let projargs, subst, evars, respars, typeargs =
Array.fold_left2
(fun (acc, subst, evars, sigargs, typeargs') x y ->
- let (carrier, relation), sigargs = split_head sigargs in
- match relation with
- | Some relation ->
- let carrier = substl subst carrier
- and relation = substl subst relation in
- (match y with
- | None ->
- let evars, proof =
- (if b then PropGlobal.proper_proof else TypeGlobal.proper_proof)
- env evars carrier relation x in
- [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
- | Some r ->
+ let (carrier, relation), sigargs = split_head sigargs in
+ match relation with
+ | Some relation ->
+ let carrier = substl subst carrier
+ and relation = substl subst relation in
+ (match y with
+ | None ->
+ let evars, proof =
+ (if b then PropGlobal.proper_proof else TypeGlobal.proper_proof)
+ env evars carrier relation x in
+ [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
+ | Some r ->
let evars, proof = get_rew_prf evars r in
- [ snd proof; r.rew_to; x ] @ acc, subst, evars,
- sigargs, r.rew_to :: typeargs')
- | None ->
- if not (Option.is_empty y) then
- user_err Pp.(str "Cannot rewrite inside dependent arguments of a function");
- x :: acc, x :: subst, evars, sigargs, x :: typeargs')
+ [ snd proof; r.rew_to; x ] @ acc, subst, evars,
+ sigargs, r.rew_to :: typeargs')
+ | None ->
+ if not (Option.is_empty y) then
+ user_err Pp.(str "Cannot rewrite inside dependent arguments of a function");
+ x :: acc, x :: subst, evars, sigargs, x :: typeargs')
([], [], evars, sigargs, []) args args'
in
let proof = applist (proj, List.rev projargs) in
let newt = applist (m', List.rev typeargs) in
match respars with
- [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt
+ [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt
| _ -> assert(false)
let apply_constraint env avoid car rel prf cstr res =
@@ -852,7 +852,7 @@ let apply_constraint env avoid car rel prf cstr res =
| None -> res
| Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res
-let coerce env avoid cstr res =
+let coerce env avoid cstr res =
let evars, (rel, prf) = get_rew_prf res.rew_evars res in
let res = { res with rew_evars = evars } in
apply_constraint env avoid res.rew_car rel prf cstr res
@@ -860,22 +860,22 @@ let coerce env avoid cstr res =
let apply_rule unify loccs : int pure_strategy =
let (nowhere_except_in,occs) = convert_occs loccs in
let is_occ occ =
- if nowhere_except_in
- then List.mem occ occs
- else not (List.mem occ occs)
+ if nowhere_except_in
+ then List.mem occ occs
+ else not (List.mem occ occs)
in
{ strategy = fun { state = occ ; env ; unfresh ;
- term1 = t ; ty1 = ty ; cstr ; evars } ->
+ term1 = t ; ty1 = ty ; cstr ; evars } ->
let unif = if isEvar (goalevars evars) t then None else unify env evars t in
- match unif with
- | None -> (occ, Fail)
+ match unif with
+ | None -> (occ, Fail)
| Some rew ->
- let occ = succ occ in
- if not (is_occ occ) then (occ, Fail)
- else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
- else
- let res = { rew with rew_car = ty } in
- let res = Success (coerce env unfresh cstr res) in
+ let occ = succ occ in
+ if not (is_occ occ) then (occ, Fail)
+ else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
+ else
+ let res = { rew with rew_car = ty } in
+ let res = Success (coerce env unfresh cstr res) in
(occ, res)
}
@@ -893,10 +893,10 @@ let apply_lemma l2r flags oc by loccs : strategy = { strategy =
| Some rew -> Some rew
in
let _, res = (apply_rule unify loccs).strategy { input with
- state = 0 ;
- evars } in
+ state = 0 ;
+ evars } in
(), res
- }
+ }
let e_app_poly env evars f args =
let evars', c = app_poly_nocheck env !evars f args in
@@ -905,16 +905,16 @@ let e_app_poly env evars f args =
let make_leibniz_proof env c ty r =
let evars = ref r.rew_evars in
- let prf =
+ let prf =
match r.rew_prf with
- | RewPrf (rel, prf) ->
- let rel = e_app_poly env evars coq_eq [| ty |] in
- let prf =
- e_app_poly env evars coq_f_equal
- [| r.rew_car; ty;
+ | RewPrf (rel, prf) ->
+ let rel = e_app_poly env evars coq_eq [| ty |] in
+ let prf =
+ e_app_poly env evars coq_f_equal
+ [| r.rew_car; ty;
mkLambda (make_annot Anonymous Sorts.Relevant, r.rew_car, c);
- r.rew_from; r.rew_to; prf |]
- in RewPrf (rel, prf)
+ r.rew_from; r.rew_to; prf |]
+ in RewPrf (rel, prf)
| RewCast k -> r.rew_prf
in
{ rew_car = ty; rew_evars = !evars;
@@ -923,39 +923,39 @@ let make_leibniz_proof env c ty r =
let reset_env env =
let env' = Global.env_of_context (Environ.named_context_val env) in
Environ.push_rel_context (Environ.rel_context env) env'
-
+
let fold_match ?(force=false) env sigma c =
let (ci, p, c, brs) = destCase sigma c in
let cty = Retyping.get_type_of env sigma c in
- let dep, pred, exists, (sk,eff) =
+ let dep, pred, exists, (sk,eff) =
let env', ctx, body =
let ctx, pred = decompose_lam_assum sigma p in
let env' = push_rel_context ctx env in
- env', ctx, pred
+ env', ctx, pred
in
let sortp = Retyping.get_sort_family_of env' sigma body in
let sortc = Retyping.get_sort_family_of env sigma cty in
let dep = not (noccurn sigma 1 body) in
let pred = if dep then p else
- it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
+ it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
in
- let sk =
+ let sk =
if sortp == Sorts.InProp then
- if sortc == Sorts.InProp then
- if dep then case_dep_scheme_kind_from_prop
- else case_scheme_kind_from_prop
- else (
+ if sortc == Sorts.InProp then
+ if dep then case_dep_scheme_kind_from_prop
+ else case_scheme_kind_from_prop
+ else (
if dep
then case_dep_scheme_kind_from_type_in_prop
else case_scheme_kind_from_type)
else ((* sortc <> InProp by typing *)
- if dep
- then case_dep_scheme_kind_from_type
- else case_scheme_kind_from_type)
- in
+ if dep
+ then case_dep_scheme_kind_from_type
+ else case_scheme_kind_from_type)
+ in
let exists = Ind_tables.check_scheme sk ci.ci_ind in
if exists || force then
- dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind
+ dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind
else raise Not_found
in
let app =
@@ -963,7 +963,7 @@ let fold_match ?(force=false) env sigma c =
let pars, args = List.chop ci.ci_npar args in
let meths = List.map (fun br -> br) (Array.to_list brs) in
applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
- in
+ in
sk, (if exists then env else reset_env env), app, eff
let unfold_match env sigma sk app =
@@ -971,128 +971,128 @@ let unfold_match env sigma sk app =
| App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
let v = EConstr.of_constr v in
- Reductionops.whd_beta sigma (mkApp (v, args))
+ Reductionops.whd_beta sigma (mkApp (v, args))
| _ -> app
let is_rew_cast = function RewCast _ -> true | _ -> false
let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let rec aux { state ; env ; unfresh ;
- term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } =
+ term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } =
let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
match EConstr.kind (goalevars evars) t with
| App (m, args) ->
- let rewrite_args state success =
- let state, (args', evars', progress) =
- Array.fold_left
- (fun (state, (acc, evars, progress)) arg ->
- if not (Option.is_empty progress) && not all then
- state, (None :: acc, evars, progress)
- else
- let argty = Retyping.get_type_of env (goalevars evars) arg in
- let state, res = s.strategy { state ; env ;
- unfresh ;
- term1 = arg ; ty1 = argty ;
- cstr = (prop,None) ;
- evars } in
- let res' =
- match res with
- | Identity ->
- let progress = if Option.is_empty progress then Some false else progress in
- (None :: acc, evars, progress)
- | Success r ->
- (Some r :: acc, r.rew_evars, Some true)
- | Fail -> (None :: acc, evars, progress)
- in state, res')
- (state, ([], evars, success)) args
- in
- let res =
- match progress with
- | None -> Fail
- | Some false -> Identity
- | Some true ->
- let args' = Array.of_list (List.rev args') in
- if Array.exists
- (function
- | None -> false
- | Some r -> not (is_rew_cast r.rew_prf)) args'
- then
- let evars', prf, car, rel, c1, c2 =
- resolve_morphism env unfresh t m args args' (prop, cstr') evars'
- in
- let res = { rew_car = ty; rew_from = c1;
- rew_to = c2; rew_prf = RewPrf (rel, prf);
- rew_evars = evars' }
- in Success res
- else
- let args' = Array.map2
- (fun aorig anew ->
- match anew with None -> aorig
- | Some r -> r.rew_to) args args'
- in
- let res = { rew_car = ty; rew_from = t;
- rew_to = mkApp (m, args'); rew_prf = RewCast DEFAULTcast;
- rew_evars = evars' }
- in Success res
- in state, res
- in
- if flags.on_morphisms then
- let mty = Retyping.get_type_of env (goalevars evars) m in
- let evars, cstr', m, mty, argsl, args =
- let argsl = Array.to_list args in
- let lift = if prop then PropGlobal.lift_cstr else TypeGlobal.lift_cstr in
- match lift env evars argsl m mty None with
- | Some (evars, cstr', m, mty, args) ->
- evars, Some cstr', m, mty, args, Array.of_list args
- | None -> evars, None, m, mty, argsl, args
- in
- let state, m' = s.strategy { state ; env ; unfresh ;
- term1 = m ; ty1 = mty ;
- cstr = (prop, cstr') ; evars } in
- match m' with
- | Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
- | Identity -> rewrite_args state (Some false)
- | Success r ->
- (* We rewrote the function and get a proof of pointwise rel for the arguments.
- We just apply it. *)
- let prf = match r.rew_prf with
- | RewPrf (rel, prf) ->
- let app = if prop then PropGlobal.apply_pointwise
- else TypeGlobal.apply_pointwise
- in
- RewPrf (app (goalevars evars) rel argsl, mkApp (prf, args))
- | x -> x
- in
- let res =
- { rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args;
- rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
- rew_prf = prf; rew_evars = r.rew_evars }
- in
- let res =
- match prf with
- | RewPrf (rel, prf) ->
- Success (apply_constraint env unfresh res.rew_car
- rel prf (prop,cstr) res)
- | _ -> Success res
- in state, res
- else rewrite_args state None
-
+ let rewrite_args state success =
+ let state, (args', evars', progress) =
+ Array.fold_left
+ (fun (state, (acc, evars, progress)) arg ->
+ if not (Option.is_empty progress) && not all then
+ state, (None :: acc, evars, progress)
+ else
+ let argty = Retyping.get_type_of env (goalevars evars) arg in
+ let state, res = s.strategy { state ; env ;
+ unfresh ;
+ term1 = arg ; ty1 = argty ;
+ cstr = (prop,None) ;
+ evars } in
+ let res' =
+ match res with
+ | Identity ->
+ let progress = if Option.is_empty progress then Some false else progress in
+ (None :: acc, evars, progress)
+ | Success r ->
+ (Some r :: acc, r.rew_evars, Some true)
+ | Fail -> (None :: acc, evars, progress)
+ in state, res')
+ (state, ([], evars, success)) args
+ in
+ let res =
+ match progress with
+ | None -> Fail
+ | Some false -> Identity
+ | Some true ->
+ let args' = Array.of_list (List.rev args') in
+ if Array.exists
+ (function
+ | None -> false
+ | Some r -> not (is_rew_cast r.rew_prf)) args'
+ then
+ let evars', prf, car, rel, c1, c2 =
+ resolve_morphism env unfresh t m args args' (prop, cstr') evars'
+ in
+ let res = { rew_car = ty; rew_from = c1;
+ rew_to = c2; rew_prf = RewPrf (rel, prf);
+ rew_evars = evars' }
+ in Success res
+ else
+ let args' = Array.map2
+ (fun aorig anew ->
+ match anew with None -> aorig
+ | Some r -> r.rew_to) args args'
+ in
+ let res = { rew_car = ty; rew_from = t;
+ rew_to = mkApp (m, args'); rew_prf = RewCast DEFAULTcast;
+ rew_evars = evars' }
+ in Success res
+ in state, res
+ in
+ if flags.on_morphisms then
+ let mty = Retyping.get_type_of env (goalevars evars) m in
+ let evars, cstr', m, mty, argsl, args =
+ let argsl = Array.to_list args in
+ let lift = if prop then PropGlobal.lift_cstr else TypeGlobal.lift_cstr in
+ match lift env evars argsl m mty None with
+ | Some (evars, cstr', m, mty, args) ->
+ evars, Some cstr', m, mty, args, Array.of_list args
+ | None -> evars, None, m, mty, argsl, args
+ in
+ let state, m' = s.strategy { state ; env ; unfresh ;
+ term1 = m ; ty1 = mty ;
+ cstr = (prop, cstr') ; evars } in
+ match m' with
+ | Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
+ | Identity -> rewrite_args state (Some false)
+ | Success r ->
+ (* We rewrote the function and get a proof of pointwise rel for the arguments.
+ We just apply it. *)
+ let prf = match r.rew_prf with
+ | RewPrf (rel, prf) ->
+ let app = if prop then PropGlobal.apply_pointwise
+ else TypeGlobal.apply_pointwise
+ in
+ RewPrf (app (goalevars evars) rel argsl, mkApp (prf, args))
+ | x -> x
+ in
+ let res =
+ { rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args;
+ rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
+ rew_prf = prf; rew_evars = r.rew_evars }
+ in
+ let res =
+ match prf with
+ | RewPrf (rel, prf) ->
+ Success (apply_constraint env unfresh res.rew_car
+ rel prf (prop,cstr) res)
+ | _ -> Success res
+ in state, res
+ else rewrite_args state None
+
| Prod (n, x, b) when noccurn (goalevars evars) 1 b ->
- let b = subst1 mkProp b in
- let tx = Retyping.get_type_of env (goalevars evars) x
- and tb = Retyping.get_type_of env (goalevars evars) b in
- let arr = if prop then PropGlobal.arrow_morphism
- else TypeGlobal.arrow_morphism
- in
- let (evars', mor), unfold = arr env evars tx tb x b in
- let state, res = aux { state ; env ; unfresh ;
- term1 = mor ; ty1 = ty ;
- cstr = (prop,cstr) ; evars = evars' } in
- let res =
- match res with
- | Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
- | Fail | Identity -> res
- in state, res
+ let b = subst1 mkProp b in
+ let tx = Retyping.get_type_of env (goalevars evars) x
+ and tb = Retyping.get_type_of env (goalevars evars) b in
+ let arr = if prop then PropGlobal.arrow_morphism
+ else TypeGlobal.arrow_morphism
+ in
+ let (evars', mor), unfold = arr env evars tx tb x b in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = mor ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars = evars' } in
+ let res =
+ match res with
+ | Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
+ | Fail | Identity -> res
+ in state, res
(* if x' = None && flags.under_lambdas then *)
(* let lam = mkLambda (n, x, b) in *)
@@ -1110,23 +1110,23 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Prod (n, dom, codom) ->
let lam = mkLambda (n, dom, codom) in
- let (evars', app), unfold =
- if eq_constr (fst evars) ty mkProp then
- (app_poly_sort prop env evars coq_all [| dom; lam |]), TypeGlobal.unfold_all
- else
- let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
- (app_poly_sort prop env evars forall [| dom; lam |]), TypeGlobal.unfold_forall
- in
- let state, res = aux { state ; env ; unfresh ;
- term1 = app ; ty1 = ty ;
- cstr = (prop,cstr) ; evars = evars' } in
- let res =
- match res with
- | Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
- | Fail | Identity -> res
- in state, res
-
-(* TODO: real rewriting under binders: introduce x x' (H : R x x') and rewrite with
+ let (evars', app), unfold =
+ if eq_constr (fst evars) ty mkProp then
+ (app_poly_sort prop env evars coq_all [| dom; lam |]), TypeGlobal.unfold_all
+ else
+ let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
+ (app_poly_sort prop env evars forall [| dom; lam |]), TypeGlobal.unfold_forall
+ in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = app ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars = evars' } in
+ let res =
+ match res with
+ | Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
+ | Fail | Identity -> res
+ in state, res
+
+(* TODO: real rewriting under binders: introduce x x' (H : R x x') and rewrite with
H at any occurrence of x. Ask for (R ==> R') for the lambda. Formalize this.
B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing
dependent relations and using projections to get them out.
@@ -1158,88 +1158,88 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
let open Context.Rel.Declaration in
let env' = EConstr.push_rel (LocalAssum (n', t)) env in
- let bty = Retyping.get_type_of env' (goalevars evars) b in
- let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
- let state, b' = s.strategy { state ; env = env' ; unfresh ;
- term1 = b ; ty1 = bty ;
- cstr = (prop, unlift env evars cstr) ;
- evars } in
- let res =
- match b' with
- | Success r ->
- let r = match r.rew_prf with
- | RewPrf (rel, prf) ->
- let point = if prop then PropGlobal.pointwise_or_dep_relation else
- TypeGlobal.pointwise_or_dep_relation
- in
+ let bty = Retyping.get_type_of env' (goalevars evars) b in
+ let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
+ let state, b' = s.strategy { state ; env = env' ; unfresh ;
+ term1 = b ; ty1 = bty ;
+ cstr = (prop, unlift env evars cstr) ;
+ evars } in
+ let res =
+ match b' with
+ | Success r ->
+ let r = match r.rew_prf with
+ | RewPrf (rel, prf) ->
+ let point = if prop then PropGlobal.pointwise_or_dep_relation else
+ TypeGlobal.pointwise_or_dep_relation
+ in
let evars, rel = point env r.rew_evars n'.binder_name t r.rew_car rel in
let prf = mkLambda (n', t, prf) in
- { r with rew_prf = RewPrf (rel, prf); rew_evars = evars }
- | x -> r
- in
- Success { r with
+ { r with rew_prf = RewPrf (rel, prf); rew_evars = evars }
+ | x -> r
+ in
+ Success { r with
rew_car = mkProd (n, t, r.rew_car);
rew_from = mkLambda(n, t, r.rew_from);
rew_to = mkLambda (n, t, r.rew_to) }
- | Fail | Identity -> b'
- in state, res
-
+ | Fail | Identity -> b'
+ in state, res
+
| Case (ci, p, c, brs) ->
- let cty = Retyping.get_type_of env (goalevars evars) c in
- let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
- let cstr' = Some eqty in
- let state, c' = s.strategy { state ; env ; unfresh ;
- term1 = c ; ty1 = cty ;
- cstr = (prop, cstr') ; evars = evars' } in
- let state, res =
- match c' with
- | Success r ->
- let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in
- let res = make_leibniz_proof env case ty r in
- state, Success (coerce env unfresh (prop,cstr) res)
- | Fail | Identity ->
- if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
- let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
- let cstr = Some eqty in
- let state, found, brs' = Array.fold_left
- (fun (state, found, acc) br ->
- if not (Option.is_empty found) then
- (state, found, fun x -> lift 1 br :: acc x)
- else
- let state, res = s.strategy { state ; env ; unfresh ;
- term1 = br ; ty1 = ty ;
- cstr = (prop,cstr) ; evars } in
- match res with
- | Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
- | Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
- (state, None, fun x -> []) brs
- in
- match found with
- | Some r ->
- let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' c'))) in
- state, Success (make_leibniz_proof env ctxc ty r)
- | None -> state, c'
- else
- match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
- | None -> state, c'
- | Some (cst, _, t', eff (*FIXME*)) ->
- let state, res = aux { state ; env ; unfresh ;
- term1 = t' ; ty1 = ty ;
- cstr = (prop,cstr) ; evars } in
- let res =
- match res with
- | Success prf ->
- Success { prf with
- rew_from = t;
- rew_to = unfold_match env (goalevars evars) cst prf.rew_to }
- | x' -> c'
- in state, res
- in
- let res =
- match res with
- | Success r -> Success (coerce env unfresh (prop,cstr) r)
- | Fail | Identity -> res
- in state, res
+ let cty = Retyping.get_type_of env (goalevars evars) c in
+ let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
+ let cstr' = Some eqty in
+ let state, c' = s.strategy { state ; env ; unfresh ;
+ term1 = c ; ty1 = cty ;
+ cstr = (prop, cstr') ; evars = evars' } in
+ let state, res =
+ match c' with
+ | Success r ->
+ let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in
+ let res = make_leibniz_proof env case ty r in
+ state, Success (coerce env unfresh (prop,cstr) res)
+ | Fail | Identity ->
+ if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
+ let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
+ let cstr = Some eqty in
+ let state, found, brs' = Array.fold_left
+ (fun (state, found, acc) br ->
+ if not (Option.is_empty found) then
+ (state, found, fun x -> lift 1 br :: acc x)
+ else
+ let state, res = s.strategy { state ; env ; unfresh ;
+ term1 = br ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } in
+ match res with
+ | Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
+ | Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
+ (state, None, fun x -> []) brs
+ in
+ match found with
+ | Some r ->
+ let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' c'))) in
+ state, Success (make_leibniz_proof env ctxc ty r)
+ | None -> state, c'
+ else
+ match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
+ | None -> state, c'
+ | Some (cst, _, t', eff (*FIXME*)) ->
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = t' ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } in
+ let res =
+ match res with
+ | Success prf ->
+ Success { prf with
+ rew_from = t;
+ rew_to = unfold_match env (goalevars evars) cst prf.rew_to }
+ | x' -> c'
+ in state, res
+ in
+ let res =
+ match res with
+ | Success r -> Success (coerce env unfresh (prop,cstr) r)
+ | Fail | Identity -> res
+ in state, res
| _ -> state, Fail
in { strategy = aux }
@@ -1249,15 +1249,15 @@ let one_subterm = subterm false default_flags
(** Requires transitivity of the rewrite step, if not a reduction.
Not tail-recursive. *)
-let transitivity state env unfresh prop (res : rewrite_result_info) (next : 'a pure_strategy) :
+let transitivity state env unfresh prop (res : rewrite_result_info) (next : 'a pure_strategy) :
'a * rewrite_result =
let state, nextres =
next.strategy { state ; env ; unfresh ;
- term1 = res.rew_to ; ty1 = res.rew_car ;
- cstr = (prop, get_opt_rew_rel res.rew_prf) ;
- evars = res.rew_evars }
- in
- let res =
+ term1 = res.rew_to ; ty1 = res.rew_car ;
+ cstr = (prop, get_opt_rew_rel res.rew_prf) ;
+ evars = res.rew_evars }
+ in
+ let res =
match nextres with
| Fail -> Fail
| Identity -> Success res
@@ -1265,21 +1265,21 @@ let transitivity state env unfresh prop (res : rewrite_result_info) (next : 'a p
match res.rew_prf with
| RewCast c -> Success { res' with rew_from = res.rew_from }
| RewPrf (rew_rel, rew_prf) ->
- match res'.rew_prf with
- | RewCast _ -> Success { res with rew_to = res'.rew_to }
- | RewPrf (res'_rel, res'_prf) ->
- let trans =
- if prop then PropGlobal.transitive_type
- else TypeGlobal.transitive_type
- in
- let evars, prfty =
- app_poly_sort prop env res'.rew_evars trans [| res.rew_car; rew_rel |]
- in
- let evars, prf = new_cstr_evar evars env prfty in
- let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
- rew_prf; res'_prf |])
- in Success { res' with rew_from = res.rew_from;
- rew_evars = evars; rew_prf = RewPrf (res'_rel, prf) }
+ match res'.rew_prf with
+ | RewCast _ -> Success { res with rew_to = res'.rew_to }
+ | RewPrf (res'_rel, res'_prf) ->
+ let trans =
+ if prop then PropGlobal.transitive_type
+ else TypeGlobal.transitive_type
+ in
+ let evars, prfty =
+ app_poly_sort prop env res'.rew_evars trans [| res.rew_car; rew_rel |]
+ in
+ let evars, prf = new_cstr_evar evars env prfty in
+ let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
+ rew_prf; res'_prf |])
+ in Success { res' with rew_from = res.rew_from;
+ rew_evars = evars; rew_prf = RewPrf (res'_rel, prf) }
in state, res
(** Rewriting strategies.
@@ -1299,54 +1299,54 @@ module Strategies =
let refl : 'a pure_strategy =
{ strategy =
- fun { state ; env ;
- term1 = t ; ty1 = ty ;
- cstr = (prop,cstr) ; evars } ->
- let evars, rel = match cstr with
- | None ->
- let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in
- let evars, rty = mkr env evars ty in
- new_cstr_evar evars env rty
- | Some r -> evars, r
- in
- let evars, proof =
- let proxy =
+ fun { state ; env ;
+ term1 = t ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } ->
+ let evars, rel = match cstr with
+ | None ->
+ let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in
+ let evars, rty = mkr env evars ty in
+ new_cstr_evar evars env rty
+ | Some r -> evars, r
+ in
+ let evars, proof =
+ let proxy =
if prop then PropGlobal.proper_proxy_type env
else TypeGlobal.proper_proxy_type env
- in
- let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in
- new_cstr_evar evars env mty
- in
- let res = Success { rew_car = ty; rew_from = t; rew_to = t;
- rew_prf = RewPrf (rel, proof); rew_evars = evars }
- in state, res
+ in
+ let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in
+ new_cstr_evar evars env mty
+ in
+ let res = Success { rew_car = ty; rew_from = t; rew_to = t;
+ rew_prf = RewPrf (rel, proof); rew_evars = evars }
+ in state, res
}
let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy =
fun input ->
- let state, res = s.strategy input in
- match res with
- | Fail -> state, Fail
- | Identity -> state, Fail
- | Success r -> state, Success r
- }
-
+ let state, res = s.strategy input in
+ match res with
+ | Fail -> state, Fail
+ | Identity -> state, Fail
+ | Success r -> state, Success r
+ }
+
let seq first snd : 'a pure_strategy = { strategy =
fun ({ env ; unfresh ; cstr } as input) ->
- let state, res = first.strategy input in
- match res with
- | Fail -> state, Fail
- | Identity -> snd.strategy { input with state }
- | Success res -> transitivity state env unfresh (fst cstr) res snd
- }
-
+ let state, res = first.strategy input in
+ match res with
+ | Fail -> state, Fail
+ | Identity -> snd.strategy { input with state }
+ | Success res -> transitivity state env unfresh (fst cstr) res snd
+ }
+
let choice fst snd : 'a pure_strategy = { strategy =
fun input ->
- let state, res = fst.strategy input in
- match res with
- | Fail -> snd.strategy { input with state }
- | Identity | Success _ -> state, res
- }
+ let state, res = fst.strategy input in
+ match res with
+ | Fail -> snd.strategy { input with state }
+ | Identity | Success _ -> state, res
+ }
let try_ str : 'a pure_strategy = choice str id
@@ -1357,7 +1357,7 @@ module Strategies =
let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy =
let rec aux input = (f { strategy = fun input -> check_interrupt aux input }).strategy input in
{ strategy = aux }
-
+
let any (s : 'a pure_strategy) : 'a pure_strategy =
fix (fun any -> try_ (seq s any))
@@ -1378,8 +1378,8 @@ module Strategies =
let lemmas cs : 'a pure_strategy =
List.fold_left (fun tac (l,l2r,by) ->
- choice tac (apply_lemma l2r rewrite_unif_flags l by AllOccurrences))
- fail cs
+ choice tac (apply_lemma l2r rewrite_unif_flags l by AllOccurrences))
+ fail cs
let inj_open hint = (); fun sigma ->
let ctx = UState.of_context_set hint.Autorewrite.rew_ctx in
@@ -1388,51 +1388,51 @@ module Strategies =
let old_hints (db : string) : 'a pure_strategy =
let rules = Autorewrite.find_rewrites db in
- lemmas
- (List.map (fun hint -> (inj_open hint, hint.Autorewrite.rew_l2r,
- hint.Autorewrite.rew_tac)) rules)
+ lemmas
+ (List.map (fun hint -> (inj_open hint, hint.Autorewrite.rew_l2r,
+ hint.Autorewrite.rew_tac)) rules)
let hints (db : string) : 'a pure_strategy = { strategy =
fun ({ term1 = t } as input) ->
let t = EConstr.Unsafe.to_constr t in
let rules = Autorewrite.find_matches db t in
let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r,
- hint.Autorewrite.rew_tac) in
+ hint.Autorewrite.rew_tac) in
let lems = List.map lemma rules in
(lemmas lems).strategy input
- }
+ }
let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy =
- fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
+ fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
let rfn, ckind = Redexpr.reduction_of_red_expr env r in
let sigma = goalevars evars in
- let (sigma, t') = rfn env sigma t in
- if Termops.eq_constr sigma t' t then
- state, Identity
- else
- state, Success { rew_car = ty; rew_from = t; rew_to = t';
- rew_prf = RewCast ckind;
- rew_evars = sigma, cstrevars evars }
- }
-
+ let (sigma, t') = rfn env sigma t in
+ if Termops.eq_constr sigma t' t then
+ state, Identity
+ else
+ state, Success { rew_car = ty; rew_from = t; rew_to = t';
+ rew_prf = RewCast ckind;
+ rew_evars = sigma, cstrevars evars }
+ }
+
let fold_glob c : 'a pure_strategy = { strategy =
fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
- let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
- let unfolded =
- try Tacred.try_red_product env sigma c
- with e when CErrors.noncritical e ->
+ let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
+ let unfolded =
+ try Tacred.try_red_product env sigma c
+ with e when CErrors.noncritical e ->
user_err Pp.(str "fold: the term is not unfoldable!")
- in
- try
- let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
- let c' = Reductionops.nf_evar sigma c in
- state, Success { rew_car = ty; rew_from = t; rew_to = c';
- rew_prf = RewCast DEFAULTcast;
- rew_evars = (sigma, snd evars) }
- with e when CErrors.noncritical e -> state, Fail
- }
-
+ in
+ try
+ let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
+ let c' = Reductionops.nf_evar sigma c in
+ state, Success { rew_car = ty; rew_from = t; rew_to = c';
+ rew_prf = RewCast DEFAULTcast;
+ rew_evars = (sigma, snd evars) }
+ with e when CErrors.noncritical e -> state, Fail
+ }
+
end
@@ -1450,19 +1450,19 @@ let rewrite_with l2r flags c occs : strategy = { strategy =
unify_eqn rew l2r flags env (sigma, cstrs) None t
in
let app = apply_rule unify occs in
- let strat =
- Strategies.fix (fun aux ->
- Strategies.choice app (subterm true default_flags aux))
+ let strat =
+ Strategies.fix (fun aux ->
+ Strategies.choice app (subterm true default_flags aux))
in
let _, res = strat.strategy { input with state = 0 } in
((), res)
- }
+ }
let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars =
let ty = Retyping.get_type_of env (goalevars evars) concl in
let _, res = s.strategy { state = () ; env ; unfresh ;
- term1 = concl ; ty1 = ty ;
- cstr = (prop, Some cstr) ; evars } in
+ term1 = concl ; ty1 = ty ;
+ cstr = (prop, Some cstr) ; evars } in
res
let solve_constraints env (evars,cstrs) =
@@ -1483,14 +1483,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
let evdref = ref sigma in
let evars = (!evdref, Evar.Set.empty) in
let evars, cstr =
- let prop, (evars, arrow) =
+ let prop, (evars, arrow) =
if Sorts.is_prop sort then true, app_poly_sort true env evars impl [||]
else false, app_poly_sort false env evars TypeGlobal.arrow [||]
in
match is_hyp with
- | None ->
- let evars, t = poly_inverse prop env evars (mkSort sort) arrow in
- evars, (prop, t)
+ | None ->
+ let evars, t = poly_inverse prop env evars (mkSort sort) arrow in
+ evars, (prop, t)
| Some _ -> evars, (prop, arrow)
in
let eq = apply_strategy strat env avoid concl cstr evars in
@@ -1502,29 +1502,29 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
let evars' = solve_constraints env res.rew_evars in
let newt = Reductionops.nf_evar evars' res.rew_to in
let evars = (* Keep only original evars (potentially instantiated) and goal evars,
- the rest has been defined and substituted already. *)
- Evar.Set.fold
- (fun ev acc ->
- if not (Evd.is_defined acc ev) then
- user_err ~hdr:"rewrite"
- (str "Unsolved constraint remaining: " ++ spc () ++
+ the rest has been defined and substituted already. *)
+ Evar.Set.fold
+ (fun ev acc ->
+ if not (Evd.is_defined acc ev) then
+ user_err ~hdr:"rewrite"
+ (str "Unsolved constraint remaining: " ++ spc () ++
Termops.pr_evar_info env acc (Evd.find acc ev))
- else Evd.remove acc ev)
- cstrs evars'
+ else Evd.remove acc ev)
+ cstrs evars'
in
let res = match res.rew_prf with
- | RewCast c -> None
- | RewPrf (rel, p) ->
- let p = nf_zeta env evars' (Reductionops.nf_evar evars' p) in
- let term =
- match abs with
- | None -> p
- | Some (t, ty) ->
+ | RewCast c -> None
+ | RewPrf (rel, p) ->
+ let p = nf_zeta env evars' (Reductionops.nf_evar evars' p) in
+ let term =
+ match abs with
+ | None -> p
+ | Some (t, ty) ->
let t = Reductionops.nf_evar evars' t in
let ty = Reductionops.nf_evar evars' ty in
mkApp (mkLambda (make_annot (Name (Id.of_string "lemma")) Sorts.Relevant, ty, p), [| t |])
- in
- let proof = match is_hyp with
+ in
+ let proof = match is_hyp with
| None -> term
| Some id -> mkApp (term, [| mkVar id |])
in Some proof
@@ -1539,7 +1539,7 @@ let rec insert_dependent env sigma decl accu hyps = match hyps with
else
insert_dependent env sigma decl (ndecl :: accu) rem
-let assert_replacing id newt tac =
+let assert_replacing id newt tac =
let prf = Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
@@ -1565,7 +1565,7 @@ let assert_replacing id newt tac =
end in
Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
-let newfail n s =
+let newfail n s =
Proofview.tclZERO (Refiner.FailError (n, lazy s))
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
@@ -1573,29 +1573,29 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
(* For compatibility *)
let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in
- let treat sigma res =
+ let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
| Some None -> if progress then newfail 0 (str"Failed to progress")
- else Proofview.tclUNIT ()
+ else Proofview.tclUNIT ()
| Some (Some res) ->
let (undef, prf, newt) = res in
let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
let gls = List.rev (Evd.fold_undefined fold undef []) in
let gls = List.map Proofview.with_empty_state gls in
match clause, prf with
- | Some id, Some p ->
+ | Some id, Some p ->
let tac = tclTHENLIST [
Refine.refine ~typecheck:true (fun h -> (h,p));
Proofview.Unsafe.tclNEWGOALS gls;
] in
Proofview.Unsafe.tclEVARS undef <*>
- tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
- | Some id, None ->
+ tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
+ | Some id, None ->
Proofview.Unsafe.tclEVARS undef <*>
convert_hyp ~check:false ~reorder:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
beta_hyp id
- | None, Some p ->
+ | None, Some p ->
Proofview.Unsafe.tclEVARS undef <*>
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1605,7 +1605,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
end in
Refine.refine ~typecheck:true make <*> Proofview.Unsafe.tclNEWGOALS gls
end
- | None, None ->
+ | None, None ->
Proofview.Unsafe.tclEVARS undef <*>
convert_concl ~check:false newt DEFAULTcast
in
@@ -1639,7 +1639,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
end
-let tactic_init_setoid () =
+let tactic_init_setoid () =
try init_setoid (); Proofview.tclUNIT ()
with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded")
@@ -1650,9 +1650,9 @@ let cl_rewrite_clause_strat progress strat clause =
(cl_rewrite_clause_newtac ~progress strat clause)
(fun (e, info) -> match e with
| RewriteFailure e ->
- tclZEROMSG (str"setoid rewrite failed: " ++ e)
- | Refiner.FailError (n, pp) ->
- tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp)
+ tclZEROMSG (str"setoid rewrite failed: " ++ e)
+ | Refiner.FailError (n, pp) ->
+ tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp)
| e -> Proofview.tclZERO ~info e))
(** Setoid rewriting when called with "setoid_rewrite" *)
@@ -1663,7 +1663,7 @@ let cl_rewrite_clause l left2right occs clause =
(** Setoid rewriting when called with "rewrite_strat" *)
let cl_rewrite_clause_strat strat clause =
cl_rewrite_clause_strat false strat clause
-
+
let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
let c sigma =
let (sigma, c) = Pretyping.understand_tcc env sigma c in
@@ -1681,22 +1681,22 @@ let interp_glob_constr_list env =
(* Syntax for rewriting with strategies *)
-type unary_strategy =
+type unary_strategy =
Subterms | Subterm | Innermost | Outermost
| Bottomup | Topdown | Progress | Try | Any | Repeat
-type binary_strategy =
+type binary_strategy =
| Compose | Choice
-type ('constr,'redexpr) strategy_ast =
+type ('constr,'redexpr) strategy_ast =
| StratId | StratFail | StratRefl
| StratUnary of unary_strategy * ('constr,'redexpr) strategy_ast
- | StratBinary of binary_strategy
+ | StratBinary of binary_strategy
* ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
| StratConstr of 'constr * bool
| StratTerms of 'constr list
| StratHints of bool * string
- | StratEval of 'redexpr
+ | StratEval of 'redexpr
| StratFold of 'constr
let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> ('a2,'b2) strategy_ast = function
@@ -1747,7 +1747,7 @@ let rec strategy_of_ast = function
| StratId -> Strategies.id
| StratFail -> Strategies.fail
| StratRefl -> Strategies.refl
- | StratUnary (f, s) ->
+ | StratUnary (f, s) ->
let s' = strategy_of_ast s in
let f' = match f with
| Subterms -> all_subterms
@@ -1774,12 +1774,12 @@ let rec strategy_of_ast = function
(fun ({ state = () ; env } as input) ->
let l' = interp_glob_constr_list env (List.map fst l) in
(Strategies.lemmas l').strategy input)
- }
+ }
| StratEval r -> { strategy =
(fun ({ state = () ; env ; evars } as input) ->
let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
(Strategies.reduce r_interp).strategy { input with
- evars = (sigma,cstrevars evars) }) }
+ evars = (sigma,cstrevars evars) }) }
| StratFold c -> Strategies.fold_glob (fst c)
@@ -1862,7 +1862,7 @@ let proper_projection env sigma r ty =
let mor, args = destApp sigma inst in
let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
let app = mkApp (PropGlobal.proper_proj env sigma,
- Array.append args [| instarg |]) in
+ Array.append args [| instarg |]) in
it_mkLambda_or_LetIn app ctx
let declare_projection n instance_id r =
@@ -1877,17 +1877,17 @@ let declare_projection n instance_id r =
let typ =
let n =
let rec aux t =
- match EConstr.kind sigma t with
- | App (f, [| a ; a' ; rel; rel' |])
- when Termops.is_global sigma (PropGlobal.respectful_ref ()) f ->
- succ (aux rel')
- | _ -> 0
+ match EConstr.kind sigma t with
+ | App (f, [| a ; a' ; rel; rel' |])
+ when Termops.is_global sigma (PropGlobal.respectful_ref ()) f ->
+ succ (aux rel')
+ | _ -> 0
in
let init =
- match EConstr.kind sigma typ with
- App (f, args) when Termops.is_global sigma (PropGlobal.respectful_ref ()) f ->
- mkApp (f, fst (Array.chop (Array.length args - 2) args))
- | _ -> typ
+ match EConstr.kind sigma typ with
+ App (f, args) when Termops.is_global sigma (PropGlobal.respectful_ref ()) f ->
+ mkApp (f, fst (Array.chop (Array.length args - 2) args))
+ | _ -> typ
in aux init
in
let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ
@@ -1911,19 +1911,19 @@ let build_morphism_signature env sigma m =
let rec aux t =
match EConstr.kind sigma t with
| Prod (na, a, b) ->
- None :: aux b
- | _ -> []
+ None :: aux b
+ | _ -> []
in aux t
in
- let evars, t', sig_, cstrs =
+ let evars, t', sig_, cstrs =
PropGlobal.build_signature (sigma, Evar.Set.empty) env t cstrs None in
let evd = ref evars in
let _ = List.iter
(fun (ty, rel) ->
Option.iter (fun rel ->
- let default = e_app_poly env evd PropGlobal.default_relation [| ty; rel |] in
- ignore(e_new_cstr_evar env evd default))
- rel)
+ let default = e_app_poly env evd PropGlobal.default_relation [| ty; rel |] in
+ ignore(e_new_cstr_evar env evd default))
+ rel)
cstrs
in
let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in
@@ -2023,7 +2023,8 @@ let add_morphism atts binders m s n =
let _id, lemma = Classes.new_instance_interactive
~global:atts.global ~poly:atts.polymorphic
instance_name binders instance_t
- ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
+ ~generalize:false ~tac ~hook:(declare_projection n instance_id)
+ Hints.empty_hint_info None
in
lemma (* no instance body -> always open proof *)
@@ -2061,14 +2062,14 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env =
(* ~flags:(false,true) to allow to mark occurrences that must not be
rewritten simply by replacing them with let-defined definitions
in the context *)
- Unification.w_unify_to_subterm
+ Unification.w_unify_to_subterm
~flags:rewrite_unif_flags
env sigma ((if l2r then c1 else c2),but)
with
| ex when Pretype_errors.precatchable_exception ex ->
- (* ~flags:(true,true) to make Ring work (since it really
+ (* ~flags:(true,true) to make Ring work (since it really
exploits conversion) *)
- Unification.w_unify_to_subterm
+ Unification.w_unify_to_subterm
~flags:rewrite_conv_unif_flags
env sigma ((if l2r then c1 else c2),but)
in
@@ -2111,15 +2112,15 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
let strat = { strategy = fun ({ state = () } as input) ->
let _, res = substrat.strategy { input with state = 0 } in
(), res
- }
+ }
in
let origsigma = Tacmach.New.project gl in
tactic_init_setoid () <*>
Proofview.tclOR
(tclPROGRESS
- (tclTHEN
+ (tclTHEN
(Proofview.Unsafe.tclEVARS evd)
- (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
+ (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
(fun (e, info) -> match e with
| RewriteFailure e ->
tclFAIL 0 (str"setoid rewrite failed: " ++ e)
@@ -2146,7 +2147,7 @@ let setoid_proof ty fn fallback =
let rel, _, _ = decompose_app_rel env sigma concl in
let (sigma, t) = Typing.type_of env sigma rel in
let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
- (try init_relation_classes () with _ -> raise Not_found);
+ (try init_relation_classes () with _ -> raise Not_found);
fn env sigma car rel
with e -> Proofview.tclZERO e
end
@@ -2156,18 +2157,18 @@ let setoid_proof ty fn fallback =
fallback
begin function (e', info) -> match e' with
| Hipattern.NoEquationFound ->
- begin match e with
- | (Not_found, _) ->
- let rel, _, _ = decompose_app_rel env sigma concl in
- not_declared env sigma ty rel
- | (e, info) -> Proofview.tclZERO ~info e
+ begin match e with
+ | (Not_found, _) ->
+ let rel, _, _ = decompose_app_rel env sigma concl in
+ not_declared env sigma ty rel
+ | (e, info) -> Proofview.tclZERO ~info e
end
| e' -> Proofview.tclZERO ~info e'
end
end
end
-let tac_open ((evm,_), c) tac =
+let tac_open ((evm,_), c) tac =
(tclTHEN (Proofview.Unsafe.tclEVARS evm) (tac c))
let poly_proof getp gett env evm car rel =
@@ -2177,32 +2178,32 @@ let poly_proof getp gett env evm car rel =
let setoid_reflexivity =
setoid_proof "reflexive"
- (fun env evm car rel ->
+ (fun env evm car rel ->
tac_open (poly_proof PropGlobal.get_reflexive_proof
- TypeGlobal.get_reflexive_proof
- env evm car rel)
- (fun c -> tclCOMPLETE (apply c)))
+ TypeGlobal.get_reflexive_proof
+ env evm car rel)
+ (fun c -> tclCOMPLETE (apply c)))
(reflexivity_red true)
let setoid_symmetry =
setoid_proof "symmetric"
- (fun env evm car rel ->
+ (fun env evm car rel ->
tac_open
- (poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
- env evm car rel)
- (fun c -> apply c))
+ (poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
+ env evm car rel)
+ (fun c -> apply c))
(symmetry_red true)
-
+
let setoid_transitivity c =
setoid_proof "transitive"
(fun env evm car rel ->
tac_open (poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof
- env evm car rel)
- (fun proof -> match c with
- | None -> eapply proof
- | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])))
+ env evm car rel)
+ (fun proof -> match c with
+ | None -> eapply proof
+ | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])))
(transitivity_red true c)
-
+
let setoid_symmetry_in id =
let open Tacmach.New in
Proofview.Goal.enter begin fun gl ->
@@ -2229,16 +2230,16 @@ let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in
let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity
-let get_lemma_proof f env evm x y =
+let get_lemma_proof f env evm x y =
let (evm, _), c = f env (evm,Evar.Set.empty) x y in
evm, c
let get_reflexive_proof =
get_lemma_proof PropGlobal.get_reflexive_proof
-let get_symmetric_proof =
+let get_symmetric_proof =
get_lemma_proof PropGlobal.get_symmetric_proof
-let get_transitive_proof =
+let get_transitive_proof =
get_lemma_proof PropGlobal.get_transitive_proof
-
+
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 8e0b0a8003..576ed686d4 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -23,25 +23,25 @@ open Tacinterp
type rewrite_attributes
val rewrite_attributes : rewrite_attributes Attributes.attribute
-type unary_strategy =
+type unary_strategy =
Subterms | Subterm | Innermost | Outermost
| Bottomup | Topdown | Progress | Try | Any | Repeat
-type binary_strategy =
+type binary_strategy =
| Compose | Choice
-type ('constr,'redexpr) strategy_ast =
+type ('constr,'redexpr) strategy_ast =
| StratId | StratFail | StratRefl
| StratUnary of unary_strategy * ('constr,'redexpr) strategy_ast
- | StratBinary of binary_strategy
+ | StratBinary of binary_strategy
* ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
| StratConstr of 'constr * bool
| StratTerms of 'constr list
| StratHints of bool * string
- | StratEval of 'redexpr
+ | StratEval of 'redexpr
| StratFold of 'constr
-type rewrite_proof =
+type rewrite_proof =
| RewPrf of constr * constr
| RewCast of Constr.cast_kind
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index da89a027e2..a57cc76faa 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -191,7 +191,7 @@ let id_of_name = function
| None -> fail ()
| Some c ->
match EConstr.kind sigma c with
- | Var id -> id
+ | Var id -> id
| Meta m -> id_of_name (Evd.meta_name sigma m)
| Evar (kn,_) ->
begin match Evd.evar_ident kn sigma with
@@ -201,12 +201,12 @@ let id_of_name = function
| Const (cst,_) -> Label.to_id (Constant.label cst)
| Construct (cstr,_) ->
let ref = GlobRef.ConstructRef cstr in
- let basename = Nametab.basename_of_global ref in
- basename
+ let basename = Nametab.basename_of_global ref in
+ basename
| Ind (ind,_) ->
let ref = GlobRef.IndRef ind in
- let basename = Nametab.basename_of_global ref in
- basename
+ let basename = Nametab.basename_of_global ref in
+ basename
| Sort s ->
begin
match ESorts.kind sigma s with
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 6a5ab55604..8bafbb7ea3 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -107,7 +107,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
let () = if Array.length tacs <= i then raise Not_found in
tacs.(i)
with Not_found ->
- CErrors.user_err
+ CErrors.user_err
(str "The tactic " ++ pr_tacname s ++ str " is not installed.")
(***************************************************************************)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 63559cf488..4dc2ade7a1 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -279,11 +279,11 @@ let intern_destruction_arg ist = function
| clear,ElimOnAnonHyp n as x -> x
| clear,ElimOnIdent {loc;v=id} ->
if !strict_check then
- (* If in a defined tactic, no intros-until *)
+ (* If in a defined tactic, no intros-until *)
let c, p = intern_constr ist (make @@ CRef (qualid_of_ident id, None)) in
- match DAst.get c with
+ match DAst.get c with
| GVar id -> clear,ElimOnIdent (make ?loc:c.loc id)
- | _ -> clear,ElimOnConstr ((c, p), NoBindings)
+ | _ -> clear,ElimOnConstr ((c, p), NoBindings)
else
clear,ElimOnIdent (make ?loc id)
@@ -401,13 +401,13 @@ let dump_glob_red_expr = function
| Unfold occs -> List.iter (fun (_, r) ->
try
Dumpglob.add_glob ?loc:r.loc
- (Smartlocate.smart_global r)
+ (Smartlocate.smart_global r)
with e when CErrors.noncritical e -> ()) occs
| Cbv grf | Lazy grf ->
List.iter (fun r ->
try
Dumpglob.add_glob ?loc:r.loc
- (Smartlocate.smart_global r)
+ (Smartlocate.smart_global r)
with e when CErrors.noncritical e -> ()) grf.rConst
| _ -> ()
@@ -525,18 +525,18 @@ let rec intern_atomic lf ist x =
intern_constr_gen false (not (Option.is_empty otac)) ist c)
| TacGeneralize cl ->
TacGeneralize (List.map (fun (c,na) ->
- intern_constr_with_occurrences ist c,
+ intern_constr_with_occurrences ist c,
intern_name lf ist na) cl)
| TacLetTac (ev,na,c,cls,b,eqpat) ->
let na = intern_name lf ist na in
TacLetTac (ev,na,intern_constr ist c,
(clause_app (intern_hyp_location ist) cls),b,
- (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat))
+ (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat))
(* Derived basic tactics *)
| TacInductionDestruct (ev,isrec,(l,el)) ->
TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats),cls) ->
- (intern_destruction_arg ist c,
+ (intern_destruction_arg ist c,
(Option.map (intern_intro_pattern_naming_loc lf ist) ipato,
Option.map (intern_or_and_intro_pattern_loc lf ist) ipats),
Option.map (clause_app (intern_hyp_location ist)) cls)) l,
@@ -557,7 +557,7 @@ let rec intern_atomic lf ist x =
TacChange (check,None,
(if is_onhyps && is_onconcl
then intern_type ist c else intern_constr ist c),
- clause_app (intern_hyp_location ist) cl)
+ clause_app (intern_hyp_location ist) cl)
| TacChange (check,Some p,c,cl) ->
let { ltacvars } = ist in
let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in
@@ -565,15 +565,15 @@ let rec intern_atomic lf ist x =
let ltacvars = List.fold_left fold ltacvars metas in
let ist' = { ist with ltacvars } in
TacChange (check,Some pat,intern_constr ist' c,
- clause_app (intern_hyp_location ist) cl)
+ clause_app (intern_hyp_location ist) cl)
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
TacRewrite
- (ev,
- List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings_arg ist c)) l,
- clause_app (intern_hyp_location ist) cl,
- Option.map (intern_pure_tactic ist) by)
+ (ev,
+ List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings_arg ist c)) l,
+ clause_app (intern_hyp_location ist) cl,
+ Option.map (intern_pure_tactic ist) by)
| TacInversion (inv,hyp) ->
TacInversion (intern_inversion_strength lf ist inv,
intern_quantified_hypothesis ist hyp)
@@ -590,7 +590,7 @@ and intern_tactic_seq onlytac ist = function
let ltacvars = Id.Set.union (extract_let_names l) ist.ltacvars in
let ist' = { ist with ltacvars } in
let l = List.map (fun (n,b) ->
- (n,intern_tacarg !strict_check false (if isrec then ist' else ist) b)) l in
+ (n,intern_tacarg !strict_check false (if isrec then ist' else ist) b)) l in
ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
| TacMatchGoal (lz,lr,lmr) ->
@@ -615,13 +615,13 @@ and intern_tactic_seq onlytac ist = function
ist.ltacvars ,
TacExtendTac (Array.map (intern_pure_tactic ist) tf,
intern_pure_tactic ist t,
- Array.map (intern_pure_tactic ist) tl)
+ Array.map (intern_pure_tactic ist) tl)
| TacThens3parts (t1,tf,t2,tl) ->
let lfun', t1 = intern_tactic_seq onlytac ist t1 in
let ist' = { ist with ltacvars = lfun' } in
(* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
lfun', TacThens3parts (t1,Array.map (intern_pure_tactic ist') tf,intern_pure_tactic ist' t2,
- Array.map (intern_pure_tactic ist') tl)
+ Array.map (intern_pure_tactic ist') tl)
| TacThens (t,tl) ->
let lfun', t = intern_tactic_seq true ist t in
let ist' = { ist with ltacvars = lfun' } in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index c252372f21..9633c9bd77 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -240,7 +240,7 @@ let append_trace trace v =
(* Dynamically check that an argument is a tactic *)
let coerce_to_tactic loc id v =
- let fail () = user_err ?loc
+ let fail () = user_err ?loc
(str "Variable " ++ Id.print id ++ str " should be bound to a tactic.")
in
if has_type v (topwit wit_tacvalue) then
@@ -472,8 +472,8 @@ let interp_fresh_id ist env sigma l =
if List.is_empty l then default_fresh_id
else
let s =
- String.concat "" (List.map (function
- | ArgArg s -> s
+ String.concat "" (List.map (function
+ | ArgArg s -> s
| ArgVar {v=id} -> Id.to_string (extract_ident ist env sigma id)) l) in
let s = if CLexer.is_keyword s then s^"0" else s in
Id.of_string s in
@@ -694,7 +694,7 @@ let interp_red_expr ist env sigma = function
sigma , Pattern l_interp
| Simpl (f,o) ->
sigma , Simpl (interp_flag ist env sigma f,
- Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
+ Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
| CbvVm o ->
sigma , CbvVm (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
| CbvNative o ->
@@ -709,23 +709,23 @@ let interp_may_eval f ist env sigma = function
redfun env sigma c_interp
| ConstrContext ({loc;v=s},c) ->
(try
- let (sigma,ic) = f ist env sigma c in
+ let (sigma,ic) = f ist env sigma c in
let ctxt = try_interp_ltac_var coerce_to_constr_context ist (Some (env, sigma)) (make ?loc s) in
- let ctxt = EConstr.Unsafe.to_constr ctxt in
+ let ctxt = EConstr.Unsafe.to_constr ctxt in
let ic = EConstr.Unsafe.to_constr ic in
- let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
+ let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
Typing.solve_evars env sigma (EConstr.of_constr c)
with
- | Not_found ->
- user_err ?loc ~hdr:"interp_may_eval"
- (str "Unbound context identifier" ++ Id.print s ++ str"."))
+ | Not_found ->
+ user_err ?loc ~hdr:"interp_may_eval"
+ (str "Unbound context identifier" ++ Id.print s ++ str"."))
| ConstrTypeOf c ->
let (sigma,c_interp) = f ist env sigma c in
let (sigma, t) = Typing.type_of ~refresh:true env sigma c_interp in
(sigma, t)
| ConstrTerm c ->
try
- f ist env sigma c
+ f ist env sigma c
with reraise ->
let reraise = CErrors.push reraise in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
@@ -909,7 +909,7 @@ let interp_destruction_arg ist gl arg =
end
| keep,ElimOnAnonHyp n as x -> x
| keep,ElimOnIdent {loc;v=id} ->
- let error () = user_err ?loc
+ let error () = user_err ?loc
(strbrk "Cannot coerce " ++ Id.print id ++
strbrk " neither to a quantified hypothesis nor to a term.")
in
@@ -941,10 +941,10 @@ let interp_destruction_arg ist gl arg =
| None -> error ()
| Some c -> keep,ElimOnConstr (fun env sigma -> (sigma, (c,NoBindings)))
with Not_found ->
- (* We were in non strict (interactive) mode *)
- if Tactics.is_quantified_hypothesis id gl then
+ (* We were in non strict (interactive) mode *)
+ if Tactics.is_quantified_hypothesis id gl then
keep,ElimOnIdent (make ?loc id)
- else
+ else
let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (qualid_of_ident ?loc id,None))) in
let f env sigma =
let (sigma,c) = interp_open_constr ist env sigma c in
@@ -995,11 +995,11 @@ let rec read_match_goal_hyps lfun ist env sigma lidh = function
| (Hyp ({loc;v=na} as locna,mp))::tl ->
let lidh' = Name.fold_right cons_and_check_name na lidh in
Hyp (locna,read_pattern lfun ist env sigma mp)::
- (read_match_goal_hyps lfun ist env sigma lidh' tl)
+ (read_match_goal_hyps lfun ist env sigma lidh' tl)
| (Def ({loc;v=na} as locna,mv,mp))::tl ->
let lidh' = Name.fold_right cons_and_check_name na lidh in
Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp)::
- (read_match_goal_hyps lfun ist env sigma lidh' tl)
+ (read_match_goal_hyps lfun ist env sigma lidh' tl)
| [] -> []
(* Reads the rules of a Match Context or a Match *)
@@ -1060,7 +1060,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
let ist = { ist with extra = TacStore.set ist.extra f_debug v } in
value_interp ist >>= fun v -> return (name_vfun appl v)
in
- Tactic_debug.debug_prompt lev tac eval
+ Tactic_debug.debug_prompt lev tac eval
| _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
@@ -1117,7 +1117,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
| TacThens3parts (t1,tf,t,tl) ->
Tacticals.New.tclTHENS3PARTS (interp_tactic ist t1)
- (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
+ (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
| TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
| TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
| TacTime (s,tac) -> Tacticals.New.tclTIME s (interp_tactic ist tac)
@@ -1276,9 +1276,9 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
| (VFun(appl,trace,olfun,(_::_ as var),body)
|VFun(appl,trace,olfun,([] as var),
(TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) ->
- let (extfun,lvar,lval)=head_with_value (var,largs) in
+ let (extfun,lvar,lval)=head_with_value (var,largs) in
let fold accu (id, v) = Id.Map.add id v accu in
- let newlfun = List.fold_left fold olfun extfun in
+ let newlfun = List.fold_left fold olfun extfun in
if List.is_empty lvar then
begin wrap_error
begin
@@ -1291,9 +1291,9 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
(catch_error_tac trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
- begin fun (e, info) ->
+ begin fun (e, info) ->
Proofview.tclLIFT (debugging_exception_step ist false e (fun () -> str "evaluation")) <*>
- Proofview.tclZERO ~info e
+ Proofview.tclZERO ~info e
end
end >>= fun v ->
(* No errors happened, we propagate the trace *)
@@ -1604,10 +1604,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
- let l = List.map (fun (k,c) ->
+ let l = List.map (fun (k,c) ->
let loc, f = interp_open_constr_with_bindings_loc ist c in
(k,(make ?loc f))) cb
- in
+ in
let sigma,tac = match cl with
| None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
| Some cl ->
@@ -1619,7 +1619,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacElim (ev,(keep,cb),cbo) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = project gl in
+ let sigma = project gl in
let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
let sigma, cbo = Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma cbo in
let named_tac =
@@ -1646,7 +1646,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = pf_env gl in
let f sigma (id,n,c) =
let (sigma,c_interp) = interp_type ist env sigma c in
- sigma , (interp_ident ist env sigma id,n,c_interp) in
+ sigma , (interp_ident ist env sigma id,n,c_interp) in
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
in
@@ -1660,8 +1660,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,c) =
- let (sigma,c_interp) = interp_type ist env sigma c in
- sigma , (interp_ident ist env sigma id,c_interp) in
+ let (sigma,c_interp) = interp_type ist env sigma c in
+ sigma , (interp_ident ist env sigma id,c_interp) in
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
in
@@ -1728,7 +1728,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let (sigma',c) = interp_pure_open_constr ist env sigma c in
name_atomic ~env
(TacLetTac(ev,na,c,clp,b,eqpat))
- (Tacticals.New.tclWITHHOLES ev
+ (Tacticals.New.tclWITHHOLES ev
(let_pat_tac b (interp_name ist env sigma na)
(sigma,c) clp eqpat) sigma')
end
@@ -1782,11 +1782,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
| _ -> false
in
let c_interp patvars env sigma =
- let lfun' = Id.Map.fold (fun id c lfun ->
- Id.Map.add id (Value.of_constr c) lfun)
- patvars ist.lfun
- in
- let ist = { ist with lfun = lfun' } in
+ let lfun' = Id.Map.fold (fun id c lfun ->
+ Id.Map.add id (Value.of_constr c) lfun)
+ patvars ist.lfun
+ in
+ let ist = { ist with lfun = lfun' } in
if is_onhyps && is_onconcl
then interp_type ist env sigma c
else interp_constr ist env sigma c
@@ -1804,7 +1804,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
let c_interp patvars env sigma =
let lfun' = Id.Map.fold (fun id c lfun ->
- Id.Map.add id (Value.of_constr c) lfun)
+ Id.Map.add id (Value.of_constr c) lfun)
patvars ist.lfun
in
let env = ensure_freshness env in
@@ -1826,7 +1826,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let f env sigma =
interp_open_constr_with_bindings ist env sigma c
in
- (b,m,keep,f)) l in
+ (b,m,keep,f)) l in
let env = Proofview.Goal.env gl in
let sigma = project gl in
let cl = interp_clause ist env sigma cl in
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index bf5d49f678..e864d31da4 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -161,9 +161,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
TacRewrite (ev,
- List.map (fun (b,m,c) ->
- b,m,subst_glob_with_bindings_arg subst c) l,
- cl,Option.map (subst_tactic subst) by)
+ List.map (fun (b,m,c) ->
+ b,m,subst_glob_with_bindings_arg subst c) l,
+ cl,Option.map (subst_tactic subst) by)
| TacInversion (DepInversion (k,c,l),hyp) ->
TacInversion (DepInversion (k,Option.map (subst_glob_constr subst) c,l),hyp)
| TacInversion (NonDepInversion _,_) as x -> x
@@ -189,13 +189,13 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
| TacDispatch tl -> TacDispatch (List.map (subst_tactic subst) tl)
| TacExtendTac (tf,t,tl) ->
TacExtendTac (Array.map (subst_tactic subst) tf,
- subst_tactic subst t,
+ subst_tactic subst t,
Array.map (subst_tactic subst) tl)
| TacThens (t,tl) ->
TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
| TacThens3parts (t1,tf,t2,tl) ->
TacThens3parts (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
- subst_tactic subst t2,Array.map (subst_tactic subst) tl)
+ subst_tactic subst t2,Array.map (subst_tactic subst) tl)
| TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
| TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac)
| TacTime (s,tac) -> TacTime (s,subst_tactic subst tac)
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index d008f9da1f..eabfe2f540 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -85,7 +85,7 @@ let is_empty_subst (ln,lm) =
would ensure consistency. *)
let equal_instances env sigma (ctx',c') (ctx,c) =
(* How to compare instances? Do we want the terms to be convertible?
- unifiable? Do we want the universe levels to be relevant?
+ unifiable? Do we want the universe levels to be relevant?
(historically, conv_x is used) *)
CList.equal Id.equal ctx ctx' && Reductionops.is_conv env sigma c' c
@@ -230,11 +230,11 @@ module PatternMatching (E:StaticEnvironment) = struct
(** [pattern_match_term refresh pat term lhs] returns the possible
matchings of [term] with the pattern [pat => lhs]. If refresh is
true, refreshes the universes of [term]. *)
- let pattern_match_term refresh pat term lhs =
+ let pattern_match_term refresh pat term lhs =
(* let term = if refresh then Termops.refresh_universes_strict term else term in *)
match pat with
| Term p ->
- begin
+ begin
try
put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*>
return lhs
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index 21e02d4c04..da57f51ca3 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -34,19 +34,19 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
let input : bool * Tacexpr.glob_tactic_expr -> obj =
declare_object
{ (default_object name) with
- cache_function = cache;
- load_function = (fun _ -> load);
- open_function = (fun _ -> load);
- classify_function = (fun (local, tac) ->
- if local then Dispose else Substitute (local, tac));
- subst_function = subst}
+ cache_function = cache;
+ load_function = (fun _ -> load);
+ open_function = (fun _ -> load);
+ classify_function = (fun (local, tac) ->
+ if local then Dispose else Substitute (local, tac));
+ subst_function = subst}
in
let put local tac =
set_default_tactic local tac;
Lib.add_anonymous_leaf (input (local, tac))
in
let get () = !locality, Tacinterp.eval_tactic !default_tactic in
- let print () =
+ let print () =
Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++
(if !locality then str" (locally defined)" else str" (globally defined)")
in
diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli
index 637dd238fe..9705d225d4 100644
--- a/plugins/ltac/tactic_option.mli
+++ b/plugins/ltac/tactic_option.mli
@@ -11,7 +11,7 @@
open Tacexpr
open Vernacexpr
-val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string ->
+val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string ->
(* put *) (locality_flag -> glob_tactic_expr -> unit) *
(* get *) (unit -> locality_flag * unit Proofview.tactic) *
(* print *) (unit -> Pp.t)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:37:23 +0000