diff options
| author | Gaëtan Gilbert | 2019-11-21 16:46:11 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-21 16:46:11 +0100 |
| commit | c0f34539209842735ccb93f3c069632b7eee4d6c (patch) | |
| tree | 32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /proofs/refiner.ml | |
| parent | b680b06b31c27751a7d551d95839aea38f7fbea1 (diff) | |
| parent | d016f69818b30b75d186fb14f440b93b0518fc66 (diff) | |
Merge PR #11010: [coq] Untabify the whole ML codebase.
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index e1896d51e3..832a749ef2 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -89,7 +89,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) = let gll = (List.map_i (fun i -> apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac)) - 0 gs) in + 0 gs) in (sigr,List.flatten gll) (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) @@ -188,13 +188,13 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) (fun hypl -> List.subtract cmp hypl oldhyps) hyps in - let s = + let s = let frst = ref true in List.fold_left (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") ^ (List.fold_left - (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) - "" lh)) + (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) + "" lh)) "" newhyps in Feedback.msg_notice (str "<infoH>" @@ -273,5 +273,5 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} -let tclPUSHEVARUNIVCONTEXT ctx gl = +let tclPUSHEVARUNIVCONTEXT ctx gl = tclEVARS (Evd.merge_universe_context (project gl) ctx) gl |