diff options
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 540a8bb420..d812a8cad7 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -27,7 +27,7 @@ let extract_prefix env info = let typecheck_evar ev env sigma = let info = Evd.find sigma ev in - (** Typecheck the hypotheses. *) + (* Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = let t = NamedDecl.get_type decl in let sigma, _ = Typing.sort_of env sigma t in @@ -40,7 +40,7 @@ let typecheck_evar ev env sigma = let (common, changed) = extract_prefix env info in let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in - (** Typecheck the conclusion *) + (* Typecheck the conclusion *) let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in sigma @@ -60,39 +60,39 @@ let generic_refine ~typecheck f gl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let state = Proofview.Goal.state gl in - (** Save the [future_goals] state to restore them after the - refinement. *) + (* Save the [future_goals] state to restore them after the + refinement. *) let prev_future_goals = Evd.save_future_goals sigma in - (** Create the refinement term *) + (* Create the refinement term *) Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> f >>= fun (v, c) -> Proofview.tclEVARMAP >>= fun sigma -> Proofview.V82.wrap_exceptions begin fun () -> let evs = Evd.save_future_goals sigma in - (** Redo the effects in sigma in the monad's env *) + (* Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in let sideff = Safe_typing.side_effects_of_private_constants privates_csts in let env = add_side_effects env sideff in - (** Check that the introduced evars are well-typed *) + (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in - (** Check that the refined term is typesafe *) + (* Check that the refined term is typesafe *) let sigma = if typecheck then Typing.check env sigma c concl else sigma in - (** Check that the goal itself does not appear in the refined term *) + (* Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = if not (Evarutil.occur_evar_upto sigma self c) then () else Pretype_errors.error_occur_check env sigma self c in - (** Restore the [future goals] state. *) + (* Restore the [future goals] state. *) let sigma = Evd.restore_future_goals sigma prev_future_goals in - (** Select the goals *) + (* Select the goals *) let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in - (** Proceed to the refinement *) + (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with | None -> - (** Nothing to do, the goal has been solved by side-effect *) + (* Nothing to do, the goal has been solved by side-effect *) sigma | Some self -> match evkmain with @@ -104,7 +104,7 @@ let generic_refine ~typecheck f gl = | None -> sigma | Some id -> Evd.rename evk id sigma in - (** Mark goals *) + (* Mark goals *) let sigma = Proofview.Unsafe.mark_as_goals sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ |