aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3ed8733df..e08d01669 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -484,7 +484,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
in
(push_name_env lvar (impls_term_list indef) env locna,
(BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl)
- | LocalPattern (loc,p,ty) ->
+ | LocalRawPattern (loc,p,ty) ->
let tyc =
match ty with
| Some ty -> ty