diff options
| author | Pierre-Marie Pédrot | 2020-07-04 19:54:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-08 00:20:42 +0200 |
| commit | aba870c6b58b18bc1bd4711c379863a87bbf6d33 (patch) | |
| tree | 6509127f687752c26d6a4353e1487e98f36966fe /tactics | |
| parent | c6391a7edfd12a876f663bbac6d24386c021d148 (diff) | |
Remove Evarutil.new_evar_from_context from the API.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4804822c99..7269b5c02d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -436,6 +436,10 @@ let clear_hyps2 env sigma ids sign t cl = with Evarutil.ClearDependencyError (id,err,inglobal) -> error_replacing_dependency env sigma id err inglobal +let new_evar_from_context ?principal sign evd typ = + let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in + Evarutil.new_evar_instance sign evd typ instance + let internal_cut ?(check=true) replace id t = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -457,8 +461,8 @@ let internal_cut ?(check=true) replace id t = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun sigma -> - let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in - let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in + let (sigma, ev) = new_evar_from_context sign sigma nf_t in + let (sigma, ev') = new_evar_from_context sign' sigma ~principal:true concl in let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in (sigma, term) end) |