diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 6 | ||||
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index be0318fbde..6888526f5b 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -657,7 +657,7 @@ let clear_hyps2_in_evi env sigma hyps t concl ids = let queue_set q is_dependent set = Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set let queue_term q is_dependent c = - queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c)) + queue_set q is_dependent (evars_of_term c) let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in @@ -675,7 +675,7 @@ let process_dependent_evar q acc evm is_dependent e = | Evar_empty -> if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> - let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in + let subevars = evars_of_term b in (* evars appearing in the definition of an evar [e] are marked as dependent when [e] is dependent itself: if [e] is a non-dependent goal, then, unless they are reach from another @@ -795,7 +795,7 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi = in let accu = match evi.evar_body with | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b) + | Evar_defined b -> evars_of_term b in let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in diff --git a/engine/evd.mli b/engine/evd.mli index 29235050b0..3cb4031f11 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -495,7 +495,7 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option contained in the object; need the term to be evar-normal otherwise defined evars are returned too. *) -val evars_of_term : constr -> Evar.Set.t +val evars_of_term : econstr -> Evar.Set.t (** including evars in instances of evars *) val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t diff --git a/engine/proofview.ml b/engine/proofview.ml index ecea637947..b77839c28e 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1253,7 +1253,7 @@ module V82 = struct let top_evars initial = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c)) + Evar.Set.elements (Evd.evars_of_term c) in CList.flatten (CList.map evars_of_initial initial) diff --git a/engine/termops.ml b/engine/termops.ml index 8a6bd17948..67fc8edf6e 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -187,7 +187,7 @@ let compute_evar_dependency_graph sigma = in match evar_body evi with | Evar_empty -> acc - | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc + | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc in Evd.fold fold sigma EvMap.empty |