diff options
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 |