diff options
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 69830960a9..4e1636e321 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -405,12 +405,13 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let new_pure_evar_full evd evi = - let (evd, evk) = Evd.new_evar evd evi in +let new_pure_evar_full evd ?typeclass_candidate evi = + let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?(principal=false) sign evd typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate + ?(principal=false) sign evd typ = let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -429,21 +430,22 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ? evar_source = src; evar_candidates = candidates } in - let (evd, newevk) = Evd.new_evar evd ?name evi in + let typeclass_candidate = if principal then Some false else typeclass_candidate in + let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in let evd = if principal then Evd.declare_principal_goal newevk evd else Evd.declare_future_goal newevk evd in (evd, newevk) -let new_evar_instance ?src ?filter ?candidates ?naming ?principal sign evd typ instance = +let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance = let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?principal typ in + let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in evd, mkEvar (newevk,Array.of_list instance) -let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd typ = +let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ = let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in let instance = match filter with @@ -453,7 +455,7 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd t (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ = +let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ = let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in @@ -461,11 +463,11 @@ let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?principal instance + new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in - let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in + let (evd', e) = new_evar env evd' ?src ?filter ?naming ~typeclass_candidate:false ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) let new_Type ?(rigid=Evd.univ_flexible) evd = |