summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml16
-rw-r--r--interp/constrintern.ml10
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/notation.ml5
4 files changed, 22 insertions, 13 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b2b21925..fd230539 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: constrextern.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
(*i*)
open Pp
@@ -602,7 +602,7 @@ let rec extern inctx scopes vars r =
extern_symbol scopes vars r'' (uninterp_notations r'')
with No_match -> match r' with
| RRef (loc,ref) ->
- extern_global loc (implicits_of_global ref)
+ extern_global loc (select_stronger_impargs (implicits_of_global ref))
(extern_reference loc vars ref)
| RVar (loc,id) -> CRef (Ident (loc,id))
@@ -655,7 +655,8 @@ let rec extern inctx scopes vars r =
CRecord (loc, None, List.rev (ip projs locals args []))
with
| Not_found | No_match | Exit ->
- extern_app loc inctx (implicits_of_global ref)
+ extern_app loc inctx
+ (select_stronger_impargs (implicits_of_global ref))
(Some ref,extern_reference rloc vars ref) args
end
| _ ->
@@ -828,12 +829,17 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
let subscopes =
try list_skipn n (find_arguments_scope ref) with _ -> [] in
let impls =
- try list_skipn n (implicits_of_global ref) with _ -> [] in
+ let impls =
+ select_impargs_size
+ (List.length args) (implicits_of_global ref) in
+ try list_skipn n impls with _ -> [] in
(if n = 0 then f else RApp (dummy_loc,f,args1)),
args2, subscopes, impls
| RApp (_,(RRef (_,ref) as f),args), None ->
let subscopes = find_arguments_scope ref in
- let impls = implicits_of_global ref in
+ let impls =
+ select_impargs_size
+ (List.length args) (implicits_of_global ref) in
f, args, subscopes, impls
| RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], []
| _, None -> t, [], [], []
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3bf556f1..d918e94d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: constrintern.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
open Pp
open Util
@@ -41,7 +41,7 @@ type var_internalization_data =
in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
identifier list *
(* signature of impargs of the variable *)
- Impargs.implicits_list *
+ Impargs.implicit_status list *
(* subscopes of the args of the variable *)
scope_name option list
@@ -557,7 +557,7 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id
(fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
- RVar (loc,id), impls, argsc, expl_impls
+ RVar (loc,id), make_implicits_list impls, argsc, expl_impls
with Not_found ->
(* Is [id] bound in current term or is an ltac var bound to constr *)
if Idset.mem id ids or List.mem id ltacvars
@@ -598,7 +598,7 @@ let find_appl_head_data = function
| RApp (_,RRef (_,ref),l) as x
when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
let n = List.length l in
- x,list_skipn_at_least n (implicits_of_global ref),
+ x,List.map (drop_first_implicits n) (implicits_of_global ref),
list_skipn_at_least n (find_arguments_scope ref),[]
| x -> x,[],[],[]
@@ -815,6 +815,7 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
+ | AHole _ -> ([],[[], PatVar (loc,Anonymous)])
| t -> error_invalid_pattern_notation loc
in aux alias fullsubst a
@@ -1372,6 +1373,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
it_mkRLambda ibind body
and intern_impargs c env l subscopes args =
+ let l = select_impargs_size (List.length args) l in
let eargs, rargs = extract_explicit_arg l args in
let rec aux n impl subscopes eargs rargs =
let (enva,subscopes') = apply_scope_env env subscopes in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index acb13a8b..02a51e7e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrintern.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
+(*i $Id: constrintern.mli 13492 2010-10-04 21:20:01Z herbelin $ i*)
(*i*)
open Names
@@ -53,7 +53,7 @@ type var_internalization_data =
identifier list *
(* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
- Impargs.implicits_list * (* signature of impargs of the variable *)
+ Impargs.implicit_status list * (** signature of impargs of the variable *)
scope_name option list (* subscopes of the args of the variable *)
(* A map of free variables to their implicit arguments and scopes *)
diff --git a/interp/notation.ml b/interp/notation.ml
index fe9d8b6d..8bf7ba21 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: notation.ml 13463 2010-09-24 22:21:29Z herbelin $ *)
(*i*)
open Util
@@ -113,7 +113,7 @@ let subst_scope (subst,sc) = sc
open Libobject
-let discharge_scope (local,_,_ as o) =
+let discharge_scope (_,(local,_,_ as o)) =
if local then None else Some o
let classify_scope (local,_,_ as o) =
@@ -124,6 +124,7 @@ let (inScope,outScope) =
cache_function = cache_scope;
open_function = open_scope;
subst_function = subst_scope;
+ discharge_function = discharge_scope;
classify_function = classify_scope }
let open_close_scope (local,opening,sc) =