From 880fee8f80503fc8a40e2e07b565cfd2a99d24da Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 19 Apr 2018 10:30:08 +0200 Subject: Make "intro"/"intros" progress on existential variables. --- tactics/tactics.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3a20c3fc4..59c035e83 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -979,6 +979,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac + | Evar ev when force_flag -> + let sigma, t = Evardefine.define_evar_as_product sigma ev in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (intro_then_gen name_flag move_flag force_flag dep_flag tac) | _ -> begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) -- cgit v1.2.3