diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-29 18:41:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-29 19:09:13 +0200 |
| commit | ae0f6455129a66c243b7e0fe858aa779f8b956c2 (patch) | |
| tree | 6ba5ed428c4eddfc1b8d2cce1000cb9fc46019e0 /tactics | |
| parent | 5e5523f9e3211052f537cc90841fc295c67fc07f (diff) | |
Merging some functions from evarutil.ml/evd.ml.
- Removed collect_evars which does not consider instance
(use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
evars_of_filterered_evar_info instead). This is consistent with
printing goal contexts in the filtered way.
Anyway, as of today, afaics goals filters are trivial
because (if I interpret evarutil.ml correctly), evars with
non-trivial filter necessarily occur in a conv pb. Conversely,
conv pbs being solved when tactics are called, there should not be
an evar used as a goal with a non-trivial filter.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
4 files changed, 7 insertions, 7 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 35889462b..d9f90b02e 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -157,7 +157,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl = try let cl = Typeclasses.class_info (fst hdc) in if cl.cl_strict then - Evarutil.evars_of_term concl + Evd.evars_of_term concl else Evar.Set.empty with _ -> Evar.Set.empty in diff --git a/tactics/equality.ml b/tactics/equality.ml index c524e67ce..79e852815 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -127,7 +127,7 @@ let freeze_initial_evars sigma flags clause = (* We take evars of the type: this may include old evars! For excluding *) (* all old evars, including the ones occurring in the rewriting lemma, *) (* we would have to take the clenv_value *) - let newevars = Evd.collect_evars (clenv_type clause) in + let newevars = Evd.evars_of_term (clenv_type clause) in let evars = fold_undefined (fun evk _ evars -> if Evar.Set.mem evk newevars then evars diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 7c4c9c965..b569ef97f 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -35,20 +35,20 @@ let instantiate_tac n c ido = let sigma = gl.sigma in let evl = match ido with - ConclLocation () -> evar_list sigma (pf_concl gl) + ConclLocation () -> evar_list (pf_concl gl) | HypLocation (id,hloc) -> let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in match hloc with InHyp -> (match decl with - (_,None,typ) -> evar_list sigma typ + (_,None,typ) -> evar_list typ | _ -> error "Please be more specific: in type or value?") | InHypTypeOnly -> - let (_, _, typ) = decl in evar_list sigma typ + let (_, _, typ) = decl in evar_list typ | InHypValueOnly -> (match decl with - (_,Some body,_) -> evar_list sigma body + (_,Some body,_) -> evar_list body | _ -> error "Not a defined hypothesis.") in if List.length evl < n then error "Not enough uninstantiated existential variables."; diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index ffd164d16..34f5b52eb 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -665,7 +665,7 @@ END let hget_evar n gl = let sigma = project gl in - let evl = evar_list sigma (pf_concl gl) in + let evl = evar_list (pf_concl gl) in if List.length evl < n then error "Not enough uninstantiated existential variables."; if n <= 0 then error "Incorrect existential variable index."; |