diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 9 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 29 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 |
3 files changed, 18 insertions, 22 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index f9834f5229..8dcc8e06bb 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -567,7 +567,7 @@ let minimal_free_rels env sigma (c,cty) = let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let { intro = exist_term } = find_sigma_data sort_of_ty in - let isevars = ref (Evarutil.create_evar_defs sigma) in + let isevars = ref (Evd.create_evar_defs sigma) in let rec sigrec_clausal_form siglen p_i = if siglen = 0 then if Evarconv.e_conv env isevars p_i dFLTty then @@ -579,19 +579,18 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let (a,p_i_minus_1) = match whd_beta_stack p_i with | (_sigS,[a;p]) -> (a,p) | _ -> anomaly "sig_clausal_form: should be a sigma type" in - let ev = Evarutil.e_new_isevar isevars env (dummy_loc,InternalHole) - (Evarutil.new_Type ()) in + let ev = Evarutil.e_new_evar isevars env (new_Type ()) in let rty = beta_applist(p_i_minus_1,[ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in match - Evd.existential_opt_value (Evarutil.evars_of !isevars) + Evd.existential_opt_value (Evd.evars_of !isevars) (destEvar ev) with | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) | None -> anomaly "Not enough components to build the dependent tuple" in let scf = sigrec_clausal_form siglen ty in - Evarutil.nf_evar (Evarutil.evars_of !isevars) scf + Evarutil.nf_evar (Evd.evars_of !isevars) scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index d65b1f3eb0..a0be2149a3 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -20,7 +20,7 @@ open Termops (* The instantiate tactic *) -let evars_of evc c = +let evar_list evc c = let rec evrec acc c = match kind_of_term c with | Evar (n, _) when Evd.in_dom evc n -> c :: acc @@ -29,30 +29,30 @@ let evars_of evc c = evrec [] c let instantiate n rawc ido gl = - let wc = Refiner.project_with_focus gl in + let sigma = gl.sigma in let evl = match ido with - ConclLocation () -> evars_of wc.sigma gl.it.evar_concl + ConclLocation () -> evar_list sigma gl.it.evar_concl | HypLocation (id,hloc) -> let decl = lookup_named id gl.it.evar_hyps in match hloc with InHyp -> (match decl with - (_,None,typ) -> evars_of wc.sigma typ + (_,None,typ) -> evar_list sigma typ | _ -> error "please be more specific : in type or value ?") | InHypTypeOnly -> - let (_, _, typ) = decl in evars_of wc.sigma typ + let (_, _, typ) = decl in evar_list sigma typ | InHypValueOnly -> (match decl with - (_,Some body,_) -> evars_of wc.sigma body + (_,Some body,_) -> evar_list sigma body | _ -> error "not a let .. in hypothesis") in if List.length evl < n then error "not enough uninstantiated existential variables"; if n <= 0 then error "incorrect existential variable index"; let ev,_ = destEvar (List.nth evl (n-1)) in - let wc' = w_refine ev rawc wc in - Tacticals.tclIDTAC {gl with sigma = wc'.sigma} + let evd' = w_refine (pf_env gl) ev rawc (create_evar_defs sigma) in + Refiner.tclEVARS (evars_of evd') gl (* let pfic gls c = @@ -67,12 +67,9 @@ let instantiate_tac = function | _ -> invalid_arg "Instantiate called with bad arguments" *) -let let_evar nam typ gls = - let sp = Evarutil.new_evar () in - let evd = Evarutil.create_evar_defs gls.sigma in - let evd' = Unification.w_Declare (pf_env gls) sp typ evd in - let ngls = {gls with sigma = Evarutil.evars_of evd'} in - let args = Array.of_list - (List.map mkVar (ids_of_named_context (pf_hyps gls))) in - Tactics.forward true nam (mkEvar(sp,args)) ngls +let let_evar name typ gls = + let evd = Evd.create_evar_defs gls.sigma in + let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in + Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd')) + (Tactics.forward true name evar) gls diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 79aa71c0f4..3d91877d00 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -369,7 +369,7 @@ let general_elim_then_using match predicate with | None -> elimclause' | Some p -> - clenv_unify true Reductionops.CONV (mkMeta pmv) p elimclause' + clenv_unify true Evd.CONV (mkMeta pmv) p elimclause' in elim_res_pf_THEN_i elimclause' branchtacs gl |