diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 2 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 |
6 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6854a4a7c5..b2e9f0e6b4 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -654,7 +654,7 @@ let rec subst_rawconstr subst raw = | RSort _ -> raw - | RHole (loc,ImplicitArg (ref,i)) -> + | RHole (loc,ImplicitArg (ref,i,b)) -> let ref',_ = subst_global subst ref in if ref' == ref then raw else RHole (loc,InternalHole) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 6bc77abcb6..79bbbf10ee 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -410,7 +410,7 @@ let metamap_to_list m = type obligation_definition_status = Define of bool | Expand type hole_kind = - | ImplicitArg of global_reference * (int * identifier option) + | ImplicitArg of global_reference * (int * identifier option) * bool | BinderType of name | QuestionMark of obligation_definition_status | CasesType diff --git a/pretyping/evd.mli b/pretyping/evd.mli index ac708d1ec7..4069144404 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -169,7 +169,7 @@ type obligation_definition_status = Define of bool | Expand (* Evars *) type hole_kind = - | ImplicitArg of global_reference * (int * identifier option) + | ImplicitArg of global_reference * (int * identifier option) * bool (* Force inference *) | BinderType of name | QuestionMark of obligation_definition_status | CasesType diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 4d33484075..d8eae2d0d6 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -75,7 +75,7 @@ type rawconstr = and rawdecl = name * binding_kind * rawconstr option * rawconstr -and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr +and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option and fix_kind = | RFix of ((int option * fix_recursion_order) array * int) diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 3628e2a503..6bb4eceb37 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -79,7 +79,7 @@ type rawconstr = and rawdecl = name * binding_kind * rawconstr option * rawconstr -and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr +and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option and fix_kind = | RFix of ((int option * fix_recursion_order) array * int) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 38e4fb677c..56b78715ad 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -277,7 +277,7 @@ let is_instance = function let is_implicit_arg k = match k with - ImplicitArg (ref, (n, id)) -> true + ImplicitArg (ref, (n, id), b) -> true | InternalHole -> true | _ -> false |