diff options
Diffstat (limited to 'tactics/evar_tactics.ml')
| -rw-r--r-- | tactics/evar_tactics.ml | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 2887fc2284..2e0996bf5a 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -14,6 +14,9 @@ open Tacexpr open Refiner open Evd open Locus +open Sigma.Notations +open Proofview.Notations +open Context.Named.Declaration (* The instantiate tactic *) @@ -41,14 +44,14 @@ let instantiate_tac n c ido = match hloc with InHyp -> (match decl with - (_,None,typ) -> evar_list typ + | LocalAssum (_,typ) -> evar_list typ | _ -> error "Please be more specific: in type or value?") | InHypTypeOnly -> - let (_, _, typ) = decl in evar_list typ + evar_list (get_type decl) | InHypValueOnly -> (match decl with - (_,Some body,_) -> evar_list body + | LocalDef (_,body,_) -> evar_list body | _ -> error "Not a defined hypothesis.") in if List.length evl < n then error "Not enough uninstantiated existential variables."; @@ -68,18 +71,21 @@ let instantiate_tac_by_name id c = let let_evar name typ = let src = (Loc.ghost,Evar_kinds.GoalEvar) in - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma = ref sigma in - let _ = Typing.sort_of env sigma typ in - let sigma = !sigma in + let _ = Typing.e_sort_of env sigma typ in + let sigma = Sigma.Unsafe.of_evar_map !sigma in let id = match name with | Names.Anonymous -> let id = Namegen.id_of_name_using_hdchar env typ name in Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) - | Names.Name id -> id in - let sigma',evar = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma')) + | Names.Name id -> id + in + let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in + let tac = (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere) - end + in + Sigma (tac, sigma, p) + end } |