diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 8d465384b..d57ae89dd 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -127,7 +127,7 @@ end module Store = Store.Make () -type evar = existential_key +type evar = Evar.t let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk) @@ -243,7 +243,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 (NamedDecl.get_id %> Term.isVarId) info args + evar_instance_array (NamedDecl.get_id %> isVarId) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -371,7 +371,7 @@ val key : Id.t -> t -> Evar.t end = struct -type t = Id.t EvMap.t * existential_key Id.Map.t +type t = Id.t EvMap.t * Evar.t Id.Map.t let empty = (EvMap.empty, Id.Map.empty) @@ -707,10 +707,10 @@ let extract_all_conv_pbs evd = extract_conv_pbs evd (fun _ -> true) let loc_of_conv_pb evd (pbty,env,t1,t2) = - match kind (fst (Term.decompose_app t1)) with + match kind (fst (decompose_app t1)) with | Evar (evk1,_) -> fst (evar_source evk1 evd) | _ -> - match kind (fst (Term.decompose_app t2)) with + match kind (fst (decompose_app t2)) with | Evar (evk2,_) -> fst (evar_source evk2 evd) | _ -> None @@ -756,10 +756,12 @@ let evar_universe_context d = d.universes let universe_context_set d = UState.context_set d.universes -let universe_context ~names ~extensible evd = - UState.universe_context ~names ~extensible evd.universes +let to_universe_context evd = UState.context evd.universes -let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl +let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes +let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes + +let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl let restrict_universe_context evd vars = { evd with universes = UState.restrict evd.universes vars } @@ -802,7 +804,7 @@ let make_evar_universe_context e l = | Some us -> List.fold_left (fun uctx (loc,id) -> - fst (UState.new_univ_variable ?loc univ_rigid (Some (Id.to_string id)) uctx)) + fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx)) uctx us (****************************************) @@ -933,8 +935,7 @@ let nf_constraints evd = let universe_of_name evd s = UState.universe_of_name evd.universes s -let add_universe_name evd s l = - { evd with universes = UState.add_universe_name evd.universes s l } +let universe_binders evd = UState.universe_binders evd.universes let universes evd = UState.ugraph evd.universes |