diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-19 10:30:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-02 19:25:22 +0200 |
| commit | 880fee8f80503fc8a40e2e07b565cfd2a99d24da (patch) | |
| tree | 67222b783e941aa265a425e1d9162a8c81d8538c /tactics/tactics.ml | |
| parent | fd146ca38202c9843b4240cbdac0ae75f57e4d67 (diff) | |
Make "intro"/"intros" progress on existential variables.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files changed, 5 insertions, 0 deletions
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 *) |