diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 55 |
1 files changed, 20 insertions, 35 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ee72d314..bf519fb7 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -230,20 +230,20 @@ let evar_instance_array test_id info args = else instance_mismatch () | false :: filter, _ :: ctxt -> instrec filter ctxt i - | true :: filter, (id, _, _) :: ctxt -> + | true :: filter, (id,_,_ as d) :: ctxt -> if i < len then let c = Array.unsafe_get args i in - if test_id id c then instrec filter ctxt (succ i) + if test_id d c then instrec filter ctxt (succ i) else (id, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in match Filter.repr (evar_filter info) with | None -> - let map i (id, _, _) = + let map i (id,_,_ as d) = if (i < len) then let c = Array.unsafe_get args i in - if test_id id c then None else Some (id,c) + if test_id d c then None else Some (id,c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -251,7 +251,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array isVarId info args + evar_instance_array (fun (id,_,_) -> isVarId id) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -568,14 +568,6 @@ type evar_map = { (*** Lifting primitive from Evar.Map. ***) -(* HH: The progress tactical now uses this function. *) -let progress_evar_map d1 d2 = - let is_new k v = - assert (v.evar_body == Evar_empty); - EvMap.mem k d2.defn_evars - in - not (d1 == d2) && EvMap.exists is_new d1.undf_evars - let add_name_newly_undefined naming evk evi (evtoid,idtoev) = let id = match naming with | Misctypes.IntroAnonymous -> @@ -779,7 +771,9 @@ let merge_universe_context evd uctx' = let set_universe_context evd uctx' = { evd with universes = uctx' } -let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} +let add_conv_pb ?(tail=false) pb d = + if tail then {d with conv_pbs = d.conv_pbs @ [pb]} + else {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (find d evk).evar_source @@ -1195,6 +1189,18 @@ let abstract_undefined_variables uctx = in { uctx with uctx_local = Univ.ContextSet.empty; uctx_univ_algebraic = vars' } +let fix_undefined_variables ({ universes = uctx } as evm) = + let algs', vars' = + Univ.LMap.fold (fun u v (algs, vars as acc) -> + if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars) + else acc) + uctx.uctx_univ_variables + (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) + in + {evm with universes = + { uctx with uctx_univ_variables = vars'; + uctx_univ_algebraic = algs' } } + let refresh_undefined_univ_variables uctx = let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in @@ -1301,27 +1307,6 @@ let e_eq_constr_univs evdref t u = let eq_constr_univs_test evd t u = snd (eq_constr_univs evd t u) -let eq_named_context_val d ctx1 ctx2 = - ctx1 == ctx2 || - let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in - let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 - && (eq_constr_univs_test d) t1 t2 - in List.equal eq_named_declaration c1 c2 - -let eq_evar_body d b1 b2 = match b1, b2 with -| Evar_empty, Evar_empty -> true -| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2 -| _ -> false - -let eq_evar_info d ei1 ei2 = - ei1 == ei2 || - eq_constr_univs_test d ei1.evar_concl ei2.evar_concl && - eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) && - eq_evar_body d ei1.evar_body ei2.evar_body - (** ppedrot: [eq_constr] may be a bit too permissive here *) - - (**********************************************************) (* Accessing metas *) |