aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
-rw-r--r--plugins/ltac/tacinterp.ml74
1 files changed, 37 insertions, 37 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:10:42 +0000