From 6211fd6e067e781a160db8765dd87067428048f2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 1 Nov 2018 23:26:06 +0100 Subject: Moving Evd.evars_of_term from constr to econstr + consequences. This impacts a lot of code, apparently in the good, removing several conversions back and forth constr. --- engine/evarutil.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'engine/evarutil.ml') 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 -- cgit v1.2.3 From 6608f64f001f8f1a50b2dc41fefdf63c0b84b270 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 2 Nov 2018 00:17:47 +0100 Subject: Passing evar_map to evars_of_term rather than expecting the term to be evar-nf. --- engine/evarutil.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'engine/evarutil.ml') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 6888526f5b..0a5bba39b9 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -656,26 +656,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids = (* spiwack: a few functions to gather evars on which goals depend. *) 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 c) +let queue_term evm q is_dependent c = + queue_set q is_dependent (evars_of_term evm c) let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in (* Queues evars appearing in the types of the goal (conclusion, then hypotheses), they are all dependent. *) - queue_term q true evi.evar_concl; + queue_term evm q true evi.evar_concl; List.iter begin fun decl -> let open NamedDecl in - queue_term q true (NamedDecl.get_type decl); + queue_term evm q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () - | LocalDef (_,b,_) -> queue_term q true b + | LocalDef (_,b,_) -> queue_term evm q true b end (EConstr.named_context_of_val evi.evar_hyps); match evi.evar_body with | Evar_empty -> if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> - let subevars = evars_of_term b in + let subevars = evars_of_term evm 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 b + | Evar_defined b -> evars_of_term sigma 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 -- cgit v1.2.3