aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-11-21 15:38:39 +0100
committerEmilio Jesus Gallego Arias2019-11-21 15:38:39 +0100
commitd016f69818b30b75d186fb14f440b93b0518fc66 (patch)
tree32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /interp
parentb680b06b31c27751a7d551d95839aea38f7fbea1 (diff)
[coq] Untabify the whole ML codebase.
We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ```
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml8
-rw-r--r--interp/constrextern.ml332
-rw-r--r--interp/constrextern.mli2
-rw-r--r--interp/constrintern.ml426
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/dumpglob.ml24
-rw-r--r--interp/impargs.ml18
-rw-r--r--interp/impargs.mli16
-rw-r--r--interp/implicit_quantifiers.ml28
-rw-r--r--interp/notation.ml62
-rw-r--r--interp/notation.mli4
-rw-r--r--interp/notation_ops.ml152
-rw-r--r--interp/notation_ops.mli2
13 files changed, 539 insertions, 539 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 49b9149675..b96ef7c4e5 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -41,7 +41,7 @@ type binder_kind =
| Default of Glob_term.binding_kind
| Generalized of Glob_term.binding_kind * bool
(** (Inner binding always Implicit) Outer bindings, typeclass-specific flag
- for implicit generalization of superclasses *)
+ for implicit generalization of superclasses *)
type abstraction_kind = AbsLambda | AbsPi
@@ -80,8 +80,8 @@ type cases_pattern_expr_r =
| CPatOr of cases_pattern_expr list
| CPatNotation of notation * cases_pattern_notation_substitution
* cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
- (notation n applied with substitution l1)
- applied to arguments l2 *)
+ (notation n applied with substitution l1)
+ applied to arguments l2 *)
| CPatPrim of prim_token
| CPatRecord of (qualid * cases_pattern_expr) list
| CPatDelimiters of string * cases_pattern_expr
@@ -127,7 +127,7 @@ and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr (* expression that is being matched *)
* lname option (* as-clause *)
- * cases_pattern_expr option (* in-clause *)
+ * cases_pattern_expr option (* in-clause *)
and branch_expr =
(cases_pattern_expr list list * constr_expr) CAst.t
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0a1371413a..0c247e2660 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -303,8 +303,8 @@ let drop_implicits_in_patt cst nb_expl args =
in let rec aux = function
|[] -> None
|(_,imps)::t -> match impls_fit [] (imps,args) with
- |None -> aux t
- |x -> x
+ |None -> aux t
+ |x -> x
in
if Int.equal nb_expl 0 then aux impl_data
else
@@ -327,7 +327,7 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
assert (bl=[]);
mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
| _ ->
- match decompose_notation_key ntn, l with
+ match decompose_notation_key ntn, l with
| (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
begin match NumTok.of_string x with
| Some n -> mkprim (loc, Numeral (SMinus,n))
@@ -378,7 +378,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
match availability_of_prim_token p sc scopes with
| None -> raise No_match
| Some key ->
- let loc = cases_pattern_loc pat in
+ let loc = cases_pattern_loc pat in
insert_pat_coercion ?loc coercion
(insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
with No_match ->
@@ -398,40 +398,40 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
let pat = match pat with
| PatVar (Name id) -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
| PatVar (Anonymous) -> CAst.make ?loc (CPatAtom None)
- | PatCstr(cstrsp,args,na) ->
+ | PatCstr(cstrsp,args,na) ->
let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
- let p =
- try
+ let p =
+ try
if !Flags.raw_print then raise Exit;
- let projs = Recordops.lookup_projections (fst cstrsp) in
- let rec ip projs args acc =
- match projs, args with
- | [], [] -> acc
- | proj :: q, pat :: tail ->
+ let projs = Recordops.lookup_projections (fst cstrsp) in
+ let rec ip projs args acc =
+ match projs, args with
+ | [], [] -> acc
+ | proj :: q, pat :: tail ->
let acc =
match proj, pat with
- | _, { CAst.v = CPatAtom None } ->
- (* we don't want to have 'x := _' in our patterns *)
+ | _, { CAst.v = CPatAtom None } ->
+ (* we don't want to have 'x := _' in our patterns *)
acc
- | Some c, _ ->
+ | Some c, _ ->
((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc)
| _ -> raise No_match in
ip q tail acc
- | _ -> assert false
- in
- CPatRecord(List.rev (ip projs args []))
- with
- Not_found | No_match | Exit ->
+ | _ -> assert false
+ in
+ CPatRecord(List.rev (ip projs args []))
+ with
+ Not_found | No_match | Exit ->
let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in
if Constrintern.get_asymmetric_patterns () then
- if pattern_printable_in_both_syntax cstrsp
- then CPatCstr (c, None, args)
- else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
- else
- let full_args = add_patt_for_params (fst cstrsp) args in
+ if pattern_printable_in_both_syntax cstrsp
+ then CPatCstr (c, None, args)
+ else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
+ else
+ let full_args = add_patt_for_params (fst cstrsp) args in
match drop_implicits_in_patt (GlobRef.ConstructRef cstrsp) 0 full_args with
- | Some true_args -> CPatCstr (c, None, true_args)
- | None -> CPatCstr (c, Some full_args, [])
+ | Some true_args -> CPatCstr (c, None, true_args)
+ | None -> CPatCstr (c, Some full_args, [])
in
insert_pat_alias ?loc (CAst.make ?loc p) na
in
@@ -450,23 +450,23 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
| None -> raise No_match
(* Uninterpretation is allowed in current context *)
| Some (scopt,key) ->
- let scopes' = Option.List.cons scopt scopes in
- let l =
+ let scopes' = Option.List.cons scopt scopes in
+ let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars c)
- subst in
- let ll =
+ subst in
+ let ll =
List.map (fun (c,(subentry,(scopt,scl))) ->
let subscope = (subentry,(scopt,scl@scopes')) in
- List.map (extern_cases_pattern_in_scope subscope vars) c)
- substlist in
- let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+ List.map (extern_cases_pattern_in_scope subscope vars) c)
+ substlist in
+ let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
- else
- match drop_implicits_in_patt gr nb_to_drop l2 with
- |Some true_args -> true_args
- |None -> raise No_match
- in
+ else
+ match drop_implicits_in_patt gr nb_to_drop l2 with
+ |Some true_args -> true_args
+ |None -> raise No_match
+ in
insert_pat_coercion coercion
(insert_pat_delimiters ?loc
(make_pat_notation ?loc ntn (l,ll) l2') key)
@@ -482,10 +482,10 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
subst in
let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
let l2' = if Constrintern.get_asymmetric_patterns () then l2
- else
- match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
- |Some true_args -> true_args
- |None -> raise No_match
+ else
+ match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
+ |Some true_args -> true_args
+ |None -> raise No_match
in
assert (List.is_empty substlist);
insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
@@ -500,8 +500,8 @@ and extern_notation_pattern allscopes vars t = function
let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in
let p = apply_notation_to_pattern ?loc (GlobRef.ConstructRef cstr)
(match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
- insert_pat_alias ?loc p na
- | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
+ insert_pat_alias ?loc p na
+ | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
| PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
with
No_match -> extern_notation_pattern allscopes vars t rules
@@ -532,8 +532,8 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
let c = extern_reference vars (GlobRef.IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
match drop_implicits_in_patt (GlobRef.IndRef ind) 0 args with
- |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
- |None -> CAst.make @@ CPatCstr (c, Some args, [])
+ |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
+ |None -> CAst.make @@ CPatCstr (c, Some args, [])
let extern_cases_pattern vars p =
extern_cases_pattern_in_scope (InConstrEntrySomeLevel,(None,[])) vars p
@@ -554,8 +554,8 @@ let is_projection nargs = function
| Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
(try
let n = Recordops.find_projection_nparams r + 1 in
- if n <= nargs then Some n
- else None
+ if n <= nargs then Some n
+ else None
with Not_found -> None)
| _ -> None
@@ -581,23 +581,23 @@ let explicitize inctx impl (cf,f) args =
!Flags.raw_print ||
(!print_implicits && !print_implicits_explicit_args) ||
(is_needed_for_correct_partial_application tail imp) ||
- (!print_implicits_defensive &&
- (not (is_inferable_implicit inctx n imp) || !Flags.beautify) &&
- is_significant_implicit (Lazy.force a))
- in
+ (!print_implicits_defensive &&
+ (not (is_inferable_implicit inctx n imp) || !Flags.beautify) &&
+ is_significant_implicit (Lazy.force a))
+ in
if visible then
(Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail
- else
- tail
+ else
+ tail
| a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
| args, [] -> List.map (fun a -> (Lazy.force a,None)) args (*In case of polymorphism*)
- | [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp ->
+ | [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp ->
(* The non-explicit application cannot be parsed back with the same type *)
raise Expl
| [], _ -> []
in
let ip = is_projection (List.length args) cf in
- let expl () =
+ let expl () =
match ip with
| Some i ->
(* Careful: It is possible to have declared implicits ending
@@ -609,12 +609,12 @@ let explicitize inctx impl (cf,f) args =
if is_impl
then raise Expl
else
- let (args1,args2) = List.chop i args in
+ let (args1,args2) = List.chop i args in
let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in
- let args1 = exprec 1 (args1,impl1) in
- let args2 = exprec (i+1) (args2,impl2) in
- let ip = Some (List.length args1) in
- CApp ((ip,f),args1@args2)
+ let args1 = exprec 1 (args1,impl1) in
+ let args2 = exprec (i+1) (args2,impl2) in
+ let ip = Some (List.length args1) in
+ CApp ((ip,f),args1@args2)
| None ->
let args = exprec 1 (args,impl) in
if List.is_empty args then f.CAst.v else
@@ -625,10 +625,10 @@ let explicitize inctx impl (cf,f) args =
CApp (g,args'@args)
| _ -> CApp ((None, f), args) in
try expl ()
- with Expl ->
+ with Expl ->
let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in
let ip = if !print_projections then ip else None in
- CAppExpl ((ip, f', us), List.map Lazy.force args)
+ CAppExpl ((ip, f', us), List.map Lazy.force args)
let is_start_implicit = function
| imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
@@ -679,22 +679,22 @@ let rec remove_coercions inctx c =
| Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
let nargs = List.length args in
(try match Classops.hide_coercion r with
- | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
- (* We skip a coercion *)
- let l = List.skipn (n - pars) args in
- let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
+ | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
+ (* We skip a coercion *)
+ let l = List.skipn (n - pars) args in
+ let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
(* Recursively remove the head coercions *)
- let a' = remove_coercions true a in
- (* Don't flatten App's in case of funclass so that
- (atomic) notations on [a] work; should be compatible
- since printer does not care whether App's are
- collapsed or not and notations with an implicit
- coercion using funclass either would have already
- been confused with ordinary application or would have need
+ let a' = remove_coercions true a in
+ (* Don't flatten App's in case of funclass so that
+ (atomic) notations on [a] work; should be compatible
+ since printer does not care whether App's are
+ collapsed or not and notations with an implicit
+ coercion using funclass either would have already
+ been confused with ordinary application or would have need
a surrounding context and the coercion to funclass would
have been made explicit to match *)
- if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l)
- | _ -> c
+ if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l)
+ | _ -> c
with Not_found -> c)
| _ -> c
@@ -841,58 +841,58 @@ let rec extern inctx scopes vars r =
| GApp (f,args) ->
(match DAst.get f with
- | GRef (ref,us) ->
- let subscopes = find_arguments_scope ref in
+ | GRef (ref,us) ->
+ let subscopes = find_arguments_scope ref in
let args = fill_arg_scopes args subscopes scopes in
- begin
- try
+ begin
+ try
if !Flags.raw_print then raise Exit;
let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
- let struc = Recordops.lookup_structure (fst cstrsp) in
+ let struc = Recordops.lookup_structure (fst cstrsp) in
if PrintingRecord.active (fst cstrsp) then
()
else if PrintingConstructor.active (fst cstrsp) then
raise Exit
else if not (get_record_print ()) then
raise Exit;
- let projs = struc.Recordops.s_PROJ in
- let locals = struc.Recordops.s_PROJKIND in
- let rec cut args n =
- if Int.equal n 0 then args
- else
- match args with
- | [] -> raise No_match
- | _ :: t -> cut t (n - 1) in
- let args = cut args struc.Recordops.s_EXPECTEDPARAM in
- let rec ip projs locs args acc =
- match projs with
- | [] -> acc
- | None :: q -> raise No_match
- | Some c :: q ->
- match locs with
- | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
+ let projs = struc.Recordops.s_PROJ in
+ let locals = struc.Recordops.s_PROJKIND in
+ let rec cut args n =
+ if Int.equal n 0 then args
+ else
+ match args with
+ | [] -> raise No_match
+ | _ :: t -> cut t (n - 1) in
+ let args = cut args struc.Recordops.s_EXPECTEDPARAM in
+ let rec ip projs locs args acc =
+ match projs with
+ | [] -> acc
+ | None :: q -> raise No_match
+ | Some c :: q ->
+ match locs with
+ | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
| { Recordops.pk_true_proj = false } :: locs' ->
- (* we don't want to print locals *)
- ip q locs' args acc
+ (* we don't want to print locals *)
+ ip q locs' args acc
| { Recordops.pk_true_proj = true } :: locs' ->
- match args with
- | [] -> raise No_match
- (* we give up since the constructor is not complete *)
- | (arg, scopes) :: tail ->
+ match args with
+ | [] -> raise No_match
+ (* we give up since the constructor is not complete *)
+ | (arg, scopes) :: tail ->
let head = extern true scopes vars arg in
ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc)
- in
- CRecord (List.rev (ip projs locals args []))
- with
- | Not_found | No_match | Exit ->
+ in
+ CRecord (List.rev (ip projs locals args []))
+ with
+ | Not_found | No_match | Exit ->
let args = extern_args (extern true) vars args in
- extern_app inctx
- (select_stronger_impargs (implicits_of_global ref))
+ extern_app inctx
+ (select_stronger_impargs (implicits_of_global ref))
(Some ref,extern_reference ?loc vars ref) (extern_universes us) args
- end
+ end
- | _ ->
- explicitize inctx [] (None,sub_extern false scopes vars f)
+ | _ ->
+ explicitize inctx [] (None,sub_extern false scopes vars f)
(List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
| GLetIn (na,b,t,c) ->
@@ -911,7 +911,7 @@ let rec extern inctx scopes vars r =
| GCases (sty,rtntypopt,tml,eqns) ->
let vars' =
List.fold_right (Name.fold_right Id.Set.add)
- (cases_predicate_names tml) vars in
+ (cases_predicate_names tml) vars in
let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
let tml = List.map (fun (tm,(na,x)) ->
let na' = match na, DAst.get tm with
@@ -954,9 +954,9 @@ let rec extern inctx scopes vars r =
| GRec (fk,idv,blv,tyv,bv) ->
let vars' = Array.fold_right Id.Set.add idv vars in
(match fk with
- | GFix (nv,n) ->
- let listdecl =
- Array.mapi (fun i fi ->
+ | GFix (nv,n) ->
+ let listdecl =
+ Array.mapi (fun i fi ->
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in
let (assums,ids,bl) = extern_local_binder scopes vars bl in
@@ -969,10 +969,10 @@ let rec extern inctx scopes vars r =
in
((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
- in
+ in
CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
- | GCoFix n ->
- let listdecl =
+ | GCoFix n ->
+ let listdecl =
Array.mapi (fun i fi ->
let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in
let (_,ids,bl) = extern_local_binder scopes vars bl in
@@ -980,7 +980,7 @@ let rec extern inctx scopes vars r =
let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
sub_extern false scopes vars1 bv.(i))) idv
- in
+ in
CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
| GSort s -> CSort (extern_glob_sort s)
@@ -1102,44 +1102,44 @@ and extern_notation (custom,scopes as allscopes) vars t = function
let loc = Glob_ops.loc_of_glob_constr t in
try
if is_inactive_rule keyrule then raise No_match;
- (* Adjusts to the number of arguments expected by the notation *)
- let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with
- | GApp (f,args), Some n
- when List.length args >= n ->
- let args1, args2 = List.chop n args in
+ (* Adjusts to the number of arguments expected by the notation *)
+ let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with
+ | GApp (f,args), Some n
+ when List.length args >= n ->
+ let args1, args2 = List.chop n args in
let subscopes, impls =
match DAst.get f with
| GRef (ref,us) ->
- let subscopes =
- try List.skipn n (find_arguments_scope ref)
+ let subscopes =
+ try List.skipn n (find_arguments_scope ref)
with Failure _ -> [] in
- let impls =
- let impls =
- select_impargs_size
- (List.length args) (implicits_of_global ref) in
- try List.skipn n impls with Failure _ -> [] in
+ let impls =
+ let impls =
+ select_impargs_size
+ (List.length args) (implicits_of_global ref) in
+ try List.skipn n impls with Failure _ -> [] in
subscopes,impls
| _ ->
[], [] in
- (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
- args2, subscopes, impls
- | GApp (f, args), None ->
+ (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
+ args2, subscopes, impls
+ | GApp (f, args), None ->
begin match DAst.get f with
| GRef (ref,us) ->
- let subscopes = find_arguments_scope ref in
- let impls =
- select_impargs_size
- (List.length args) (implicits_of_global ref) in
- f, args, subscopes, impls
+ let subscopes = find_arguments_scope ref in
+ let impls =
+ select_impargs_size
+ (List.length args) (implicits_of_global ref) in
+ f, args, subscopes, impls
| _ -> t, [], [], []
end
- | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], []
+ | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], []
| _, None -> t, [], [], []
| _ -> raise No_match in
- (* Try matching ... *)
+ (* Try matching ... *)
let terms,termlists,binders,binderlists =
match_notation_constr !print_universes t pat in
- (* Try availability of interpretation ... *)
+ (* Try availability of interpretation ... *)
let e =
match keyrule with
| NotationRule (sc,ntn) ->
@@ -1152,12 +1152,12 @@ and extern_notation (custom,scopes as allscopes) vars t = function
(* Uninterpretation is allowed in current context *)
| Some (scopt,key) ->
let scopes' = Option.List.cons scopt (snd scopes) in
- let l =
+ let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
- extern (* assuming no overloading: *) true
+ extern (* assuming no overloading: *) true
(subentry,(scopt,scl@scopes')) vars c)
terms in
- let ll =
+ let ll =
List.map (fun (c,(subentry,(scopt,scl))) ->
List.map (extern true (subentry,(scopt,scl@scopes')) vars) c)
termlists in
@@ -1174,17 +1174,17 @@ and extern_notation (custom,scopes as allscopes) vars t = function
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
| Some coercion ->
- let l =
+ let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
- terms in
+ terms in
let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in
insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
- if List.is_empty args then e
- else
+ if List.is_empty args then e
+ else
let args = fill_arg_scopes args argsscopes allscopes in
- let args = extern_args (extern true) vars args in
- CAst.make ?loc @@ explicitize false argsimpls (None,e) args
+ let args = extern_args (extern true) vars args in
+ CAst.make ?loc @@ explicitize false argsimpls (None,e) args
with
No_match -> extern_notation allscopes vars t rules
@@ -1255,15 +1255,15 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l)
| PRel n ->
let id = try match lookup_name_of_rel n env with
- | Name id -> id
- | Anonymous ->
- anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.")
+ | Name id -> id
+ | Anonymous ->
+ anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.")
with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
GVar id
| PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None)
| PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
| PProj (p,c) -> GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p),None),
- [glob_of_pat avoid env sigma c])
+ [glob_of_pat avoid env sigma c])
| PApp (f,args) ->
GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args)
| PSoApp (n,args) ->
@@ -1290,19 +1290,19 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
| PCase (info,p,tm,bl) ->
let mat = match bl, info.cip_ind with
- | [], _ -> []
- | _, Some ind ->
- let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in
- simple_cases_matrix_of_branches ind bl'
- | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
+ | [], _ -> []
+ | _, Some ind ->
+ let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in
+ simple_cases_matrix_of_branches ind bl'
+ | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
in
let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
in
let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with
- | PMeta None, _, _ -> (Anonymous,None),None
- | _, Some ind, Some nargs ->
- return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
- | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
+ | PMeta None, _, _ -> (Anonymous,None),None
+ | _, Some ind, Some nargs ->
+ return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
+ | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
in
GCases (Constr.RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
| PFix ((ln,i),(lna,tl,bl)) ->
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 7b8b93377b..e22dd2be86 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -32,7 +32,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
(** If [b=true] in [extern_constr b env c] then the variables in the first
level of quantification clashing with the variables in [env] are renamed.
- ~lax is for debug printing, when the constr might not be well typed in
+ ~lax is for debug printing, when the constr might not be well typed in
env, sigma
*)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f2cb4ae5c7..57e2214293 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -279,7 +279,7 @@ let error_inconsistent_scope ?loc id scopes1 scopes2 =
pr_scope_stack scopes1)
let error_expect_binder_notation_type ?loc id =
- user_err ?loc
+ user_err ?loc
(Id.print id ++
str " is expected to occur in binding position in the right-hand side.")
@@ -299,7 +299,7 @@ let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars =
in
match typ with
| Notation_term.NtnInternTypeOnlyBinder ->
- if istermvar then error_expect_binder_notation_type ?loc id
+ if istermvar then error_expect_binder_notation_type ?loc id
| Notation_term.NtnInternTypeAny -> ()
with Not_found ->
(* Not in a notation *)
@@ -319,8 +319,8 @@ let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
(* Utilities for binders *)
let build_impls = function
|Implicit -> (function
- |Name id -> Some (id, Impargs.Manual, (true,true))
- |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true)))
+ |Name id -> Some (id, Impargs.Manual, (true,true))
+ |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true)))
|Explicit -> fun _ -> None
let impls_type_list ?(args = []) =
@@ -335,7 +335,7 @@ let impls_term_list ?(args = []) =
| GRec (fix_kind, nas, args, tys, bds) ->
let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in
- aux acc' bds.(nb)
+ aux acc' bds.(nb)
|_ -> (Variable,[],List.append args (List.rev acc),[])
in aux []
@@ -351,9 +351,9 @@ let rec check_capture ty = let open CAst in function
let locate_if_hole ?loc na c = match DAst.get c with
| GHole (_,naming,arg) ->
(try match na with
- | Name id -> glob_constr_of_notation_constr ?loc
- (Reserve.find_reserved_type id)
- | Anonymous -> raise Not_found
+ | Name id -> glob_constr_of_notation_constr ?loc
+ (Reserve.find_reserved_type id)
+ | Anonymous -> raise Not_found
with Not_found -> DAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
| _ -> c
@@ -416,13 +416,13 @@ let intern_generalized_binder intern_type ntnvars
let na = match na with
| Anonymous ->
let name =
- let id =
- match ty with
+ let id =
+ match ty with
| { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
qualid_basename qid
- | _ -> default_non_dependent_ident
- in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
- in Name name
+ | _ -> default_non_dependent_ident
+ in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
+ in Name name
| _ -> na
in (push_name_env ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl
@@ -437,7 +437,7 @@ let intern_assumption intern ntnvars env nal bk ty =
(fun (env, bl) ({loc;v=na} as locna) ->
(push_name_env ntnvars impls env locna,
(make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
- (env, []) nal
+ (env, []) nal
| Generalized (b',t) ->
let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b' t ty in
env, b
@@ -501,9 +501,9 @@ let intern_generalization intern env ntnvars loc bk ak c =
let env', c' =
let abs =
let pi = match ak with
- | Some AbsPi -> true
+ | Some AbsPi -> true
| Some _ -> false
- | None ->
+ | None ->
match Notation.current_type_scope_name () with
| Some type_scope ->
let is_type_scope = match env.tmp_scope with
@@ -514,18 +514,18 @@ let intern_generalization intern env ntnvars loc bk ak c =
String.List.mem type_scope env.scopes
| None -> false
in
- if pi then
+ if pi then
(fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
- else
+ else
(fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
in
List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in
- (env', abs lid acc)) fvs (env,c)
+ (env', abs lid acc)) fvs (env,c)
in c'
let rec expand_binders ?loc mk bl c =
@@ -708,7 +708,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
with Not_found ->
try
let (bl,(scopt,subscopes)) = Id.Map.find x binderlists in
- let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
+ let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
terms_of_binders (if revert then bl' else List.rev bl'),(None,[])
with Not_found ->
anomaly (Pp.str "Inconsistent substitution of recursive notation.") in
@@ -970,10 +970,10 @@ let find_appl_head_data c =
begin match DAst.get r with
| GRef (ref,_) when l != [] ->
let n = List.length l in
- let impls = implicits_of_global ref in
+ let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- c, List.map (drop_first_implicits n) impls,
- List.skipn_at_least n scopes,[]
+ c, List.map (drop_first_implicits n) impls,
+ List.skipn_at_least n scopes,[]
| _ -> c,[],[],[]
end
| _ -> c,[],[],[]
@@ -1084,8 +1084,8 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
try
let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
check_applied_projection isproj realref qid;
- let x, imp, scopes, l = find_appl_head_data r in
- (x,imp,scopes,l), args2
+ let x, imp, scopes, l = find_appl_head_data r in
+ (x,imp,scopes,l), args2
with Not_found ->
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
@@ -1169,9 +1169,9 @@ let loc_of_lhs lhs =
let check_linearity lhs ids =
match has_duplicate ids with
| Some id ->
- raise (InternalizationError (loc_of_lhs lhs,NonLinearPattern id))
+ raise (InternalizationError (loc_of_lhs lhs,NonLinearPattern id))
| None ->
- ()
+ ()
(* Match the number of pattern against the number of matched args *)
let check_number_of_pattern loc n l =
@@ -1247,9 +1247,9 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in
let rec aux i = function
|[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in
- ((if Int.equal args_len nargs then false
- else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
- ,l)
+ ((if Int.equal args_len nargs then false
+ else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
+ ,l)
|imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
then let (b,out) = aux i (q,[]) in (b,(DAst.make @@ RCPatAtom None)::out)
else fail (remaining_args (len_pl1+i) il)
@@ -1489,7 +1489,7 @@ let product_of_cases_patterns aliases idspl =
(* Cartesian prod of the or-pats for the nth arg and the tail args *)
List.flatten (
List.map (fun (subst,p) ->
- List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl)))
+ List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl)))
idspl (aliases.alias_ids,[aliases.alias_map,[]])
let rec subst_pat_iterator y t = DAst.(map (function
@@ -1497,7 +1497,7 @@ let rec subst_pat_iterator y t = DAst.(map (function
begin match id with Some ({v=x},_) when Id.equal x y -> DAst.get t | _ -> p end
| RCPatCstr (id,l1,l2) ->
RCPatCstr (id,List.map (subst_pat_iterator y t) l1,
- List.map (subst_pat_iterator y t) l2)
+ List.map (subst_pat_iterator y t) l2)
| RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
| RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
@@ -1550,34 +1550,34 @@ let drop_notations_pattern looked_for genv =
| SynDef sp ->
let filter (vars,a) =
try match a with
- | NRef g ->
+ | NRef g ->
(* Convention: do not deactivate implicit arguments and scopes for further arguments *)
- test_kind top g;
- let () = assert (List.is_empty vars) in
- let (_,argscs) = find_remaining_scopes [] pats g in
- Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
- | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
- test_kind top g;
+ test_kind top g;
+ let () = assert (List.is_empty vars) in
+ let (_,argscs) = find_remaining_scopes [] pats g in
+ Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
+ | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
+ test_kind top g;
let () = assert (List.is_empty vars) in
- Some (g, List.map (in_pat false scopes) pats, [])
- | NApp (NRef g,args) ->
+ Some (g, List.map (in_pat false scopes) pats, [])
+ | NApp (NRef g,args) ->
(* Convention: do not deactivate implicit arguments and scopes for further arguments *)
- test_kind top g;
- let nvars = List.length vars in
+ test_kind top g;
+ let nvars = List.length vars in
if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
- let pats1,pats2 = List.chop nvars pats in
- let subst = make_subst vars pats1 in
+ let pats1,pats2 = List.chop nvars pats in
+ let subst = make_subst vars pats1 in
let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in
- let (_,argscs) = find_remaining_scopes pats1 pats2 g in
- Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
+ let (_,argscs) = find_remaining_scopes pats1 pats2 g in
+ Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
| _ -> raise Not_found
with Not_found -> None in
Syntax_def.search_filtered_syntactic_definition filter sp
| TrueGlobal g ->
- test_kind top g;
+ test_kind top g;
Dumpglob.add_glob ?loc:qid.loc g;
- let (_,argscs) = find_remaining_scopes [] pats g in
- Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
+ let (_,argscs) = find_remaining_scopes [] pats g in
+ Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
with Not_found -> None
and in_pat top scopes pt =
let open CAst in
@@ -1588,25 +1588,25 @@ let drop_notations_pattern looked_for genv =
let sorted_fields =
sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in
begin match sorted_fields with
- | None -> DAst.make ?loc @@ RCPatAtom None
- | Some (n, head, pl) ->
+ | None -> DAst.make ?loc @@ RCPatAtom None
+ | Some (n, head, pl) ->
let pl =
if get_asymmetric_patterns () then pl else
let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
List.rev_append pars pl in
- match drop_syndef top scopes head pl with
- | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
- | None -> raise (InternalizationError (loc,NotAConstructor head))
+ match drop_syndef top scopes head pl with
+ | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
+ | None -> raise (InternalizationError (loc,NotAConstructor head))
end
| CPatCstr (head, None, pl) ->
begin
- match drop_syndef top scopes head pl with
- | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
- | None -> raise (InternalizationError (loc,NotAConstructor head))
+ match drop_syndef top scopes head pl with
+ | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
+ | None -> raise (InternalizationError (loc,NotAConstructor head))
end
| CPatCstr (qid, Some expl_pl, pl) ->
let g = try Nametab.locate qid
- with Not_found ->
+ with Not_found ->
raise (InternalizationError (loc,NotAConstructor qid)) in
if expl_pl == [] then
(* Convention: (@r) deactivates all further implicit arguments and scopes *)
@@ -1635,8 +1635,8 @@ let drop_notations_pattern looked_for genv =
rcp_of_glob scopes pat
| CPatAtom (Some id) ->
begin
- match drop_syndef top scopes id [] with
- | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c)
+ match drop_syndef top scopes id [] with
+ | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c)
| None -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes))
end
| CPatAtom None -> DAst.make ?loc @@ RCPatAtom None
@@ -1659,14 +1659,14 @@ let drop_notations_pattern looked_for genv =
| NVar id ->
let () = assert (List.is_empty args) in
begin
- (* subst remembers the delimiters stack in the interpretation *)
- (* of the notations *)
- try
- let (a,(scopt,subscopes)) = Id.Map.find id subst in
- in_pat top (scopt,subscopes@snd scopes) a
- with Not_found ->
+ (* subst remembers the delimiters stack in the interpretation *)
+ (* of the notations *)
+ try
+ let (a,(scopt,subscopes)) = Id.Map.find id subst in
+ in_pat top (scopt,subscopes@snd scopes) a
+ with Not_found ->
if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((make ?loc id),scopes)) else
- anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
+ anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
end
| NRef g ->
ensure_kind top loc g;
@@ -1679,13 +1679,13 @@ let drop_notations_pattern looked_for genv =
let pl = add_local_defs_and_check_length loc genv g pl args in
DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, [])
| NList (x,y,iter,terminator,revert) ->
- if not (List.is_empty args) then user_err ?loc
+ if not (List.is_empty args) then user_err ?loc
(strbrk "Application of arguments to a recursive notation not supported in patterns.");
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
- let (l,(scopt,subscopes)) = Id.Map.find x substlist in
+ let (l,(scopt,subscopes)) = Id.Map.find x substlist in
let termin = in_not top loc scopes fullsubst [] terminator in
- List.fold_right (fun a t ->
+ List.fold_right (fun a t ->
let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in
let u = in_not false loc scopes (nsubst, substlist) [] iter in
subst_pat_iterator ldots_var t u)
@@ -1713,15 +1713,15 @@ let rec intern_pat genv ntnvars aliases pat =
| RCPatCstr (head, expl_pl, pl) ->
if get_asymmetric_patterns () then
let len = if List.is_empty expl_pl then Some (List.length pl) else None in
- let c,idslpl1 = find_constructor loc len head in
- let with_letin =
- check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
- intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl)
+ let c,idslpl1 = find_constructor loc len head in
+ let with_letin =
+ check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
+ intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl)
else
- let c,idslpl1 = find_constructor loc None head in
- let with_letin, pl2 =
- add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
- intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
+ let c,idslpl1 = find_constructor loc None head in
+ let with_letin, pl2 =
+ add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
+ intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
| RCPatAtom (Some ({loc;v=id},scopes)) ->
let aliases = merge_aliases aliases (make ?loc @@ Name id) in
set_var_scope ?loc id false scopes ntnvars;
@@ -1756,7 +1756,7 @@ let intern_ind_pattern genv ntnvars scopes pat =
| RCPatCstr (head, expl_pl, pl) ->
let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
let with_letin, pl2 = add_implicits_check_ind_length genv loc c
- (List.length expl_pl) pl in
+ (List.length expl_pl) pl in
let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
(with_letin,
match product_of_cases_patterns empty_alias idslpl with
@@ -1775,7 +1775,7 @@ let merge_impargs l args =
List.fold_right (fun a l ->
match a with
| (_, Some {v=ExplByName id as x}) when
- List.exists (test x) args -> l
+ List.exists (test x) args -> l
| _ -> a::l)
l args
@@ -1807,30 +1807,30 @@ let extract_explicit_arg imps args =
match e with
| None -> (eargs,a::rargs)
| Some {loc;v=pos} ->
- let id = match pos with
- | ExplByName id ->
- if not (exists_implicit_name id imps) then
- user_err ?loc
- (str "Wrong argument name: " ++ Id.print id ++ str ".");
- if Id.Map.mem id eargs then
- user_err ?loc (str "Argument name " ++ Id.print id
- ++ str " occurs more than once.");
- id
- | ExplByPos (p,_id) ->
- let id =
- try
- let imp = List.nth imps (p-1) in
- if not (is_status_implicit imp) then failwith "imp";
- name_of_implicit imp
- with Failure _ (* "nth" | "imp" *) ->
- user_err ?loc
- (str"Wrong argument position: " ++ int p ++ str ".")
- in
- if Id.Map.mem id eargs then
- user_err ?loc (str"Argument at position " ++ int p ++
- str " is mentioned more than once.");
- id in
- (Id.Map.add id (loc, a) eargs, rargs)
+ let id = match pos with
+ | ExplByName id ->
+ if not (exists_implicit_name id imps) then
+ user_err ?loc
+ (str "Wrong argument name: " ++ Id.print id ++ str ".");
+ if Id.Map.mem id eargs then
+ user_err ?loc (str "Argument name " ++ Id.print id
+ ++ str " occurs more than once.");
+ id
+ | ExplByPos (p,_id) ->
+ let id =
+ try
+ let imp = List.nth imps (p-1) in
+ if not (is_status_implicit imp) then failwith "imp";
+ name_of_implicit imp
+ with Failure _ (* "nth" | "imp" *) ->
+ user_err ?loc
+ (str"Wrong argument position: " ++ int p ++ str ".")
+ in
+ if Id.Map.mem id eargs then
+ user_err ?loc (str"Argument at position " ++ int p ++
+ str " is mentioned more than once.");
+ id in
+ (Id.Map.add id (loc, a) eargs, rargs)
in aux args
(**********************************************************************)
@@ -1839,11 +1839,11 @@ let extract_explicit_arg imps args =
let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let rec intern env = CAst.with_loc_val (fun ?loc -> function
| CRef (ref,us) ->
- let (c,imp,subscopes,l),_ =
+ let (c,imp,subscopes,l),_ =
intern_applied_reference ~isproj:None intern env (Environ.named_context_val globalenv)
lvar us [] ref
- in
- apply_impargs c env imp subscopes l loc
+ in
+ apply_impargs c env imp subscopes l loc
| CFix ({ CAst.loc = locid; v = iddef}, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
@@ -1890,11 +1890,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CCoFix ({ CAst.loc = locid; v = iddef }, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in
let dl = Array.of_list dl in
- let n =
+ let n =
try List.index0 Id.equal iddef lf
with Not_found ->
- raise (InternalizationError (locid,UnboundFixName (true,iddef)))
- in
+ raise (InternalizationError (locid,UnboundFixName (true,iddef)))
+ in
let idl_tmp = Array.map
(fun ({ CAst.loc; v = id },bl,ty,_) ->
let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
@@ -1910,8 +1910,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* We add the binders common to body and type to the environment *)
let env_body = restore_binders_impargs env_rec bl_impls in
(b,c,intern {env_body with tmp_scope = None} bd)) dl idl_tmp in
- DAst.make ?loc @@
- GRec (GCoFix n,
+ DAst.make ?loc @@
+ GRec (GCoFix n,
Array.of_list lf,
Array.map (fun (bl,_,_) -> bl) idl,
Array.map (fun (_,ty,_) -> ty) idl,
@@ -1925,9 +1925,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in
expand_binders ?loc mkGLambda bl (intern env' c2)
| CLetIn (na,c1,t,c2) ->
- let inc1 = intern (reset_tmp_scope env) c1 in
- let int = Option.map (intern_type env) t in
- DAst.make ?loc @@
+ let inc1 = intern (reset_tmp_scope env) c1 in
+ let int = Option.map (intern_type env) t in
+ DAst.make ?loc @@
GLetIn (na.CAst.v, inc1, int,
intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
| CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
@@ -1939,16 +1939,16 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CGeneralization (b,a,c) ->
intern_generalization intern env ntnvars loc b a c
| CPrim p ->
- fst (Notation.interp_prim_token ?loc p (env.tmp_scope,env.scopes))
+ fst (Notation.interp_prim_token ?loc p (env.tmp_scope,env.scopes))
| CDelimiters (key, e) ->
- intern {env with tmp_scope = None;
- scopes = find_delimiters_scope ?loc key :: env.scopes} e
+ intern {env with tmp_scope = None;
+ scopes = find_delimiters_scope ?loc key :: env.scopes} e
| CAppExpl ((isproj,ref,us), args) ->
let (f,_,args_scopes,_),args =
- let args = List.map (fun a -> (a,None)) args in
+ let args = List.map (fun a -> (a,None)) args in
intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
lvar us args ref
- in
+ in
(* Rem: GApp(_,f,[]) stands for @f *)
if args = [] then DAst.make ?loc @@ GApp (f,[]) else
smart_gapp f loc (intern_args env args_scopes (List.map fst args))
@@ -1960,24 +1960,24 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
isproj',f,args'@args
(* Don't compact "(f args') args" to resolve implicits separately *)
| _ -> isproj,f,args in
- let (c,impargs,args_scopes,l),args =
+ let (c,impargs,args_scopes,l),args =
match f.CAst.v with
- | CRef (ref,us) ->
+ | CRef (ref,us) ->
intern_applied_reference ~isproj intern env
(Environ.named_context_val globalenv) lvar us args ref
| CNotation (ntn,([],[],[],[])) ->
assert (Option.is_empty isproj);
let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
let x, impl, scopes, l = find_appl_head_data c in
- (x,impl,scopes,l), args
+ (x,impl,scopes,l), args
| _ -> assert (Option.is_empty isproj); (intern env f,[],[],[]), args in
apply_impargs c env impargs args_scopes
- (merge_impargs l args) loc
+ (merge_impargs l args) loc
| CRecord fs ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
let fields =
- sort_fields ~complete:true loc fs
+ sort_fields ~complete:true loc fs
(fun _idx fieldname constructorname ->
let open Evar_kinds in
let fieldinfo : Evar_kinds.record_field =
@@ -1990,13 +1990,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
}) , IntroAnonymous, None))
in
begin
- match fields with
- | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
- | Some (n, constrname, args) ->
+ match fields with
+ | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
+ | Some (n, constrname, args) ->
let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in
let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
- intern env app
- end
+ intern env app
+ end
| CCases (sty, rtnpo, tms, eqns) ->
let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
(Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na))
@@ -2014,25 +2014,25 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
tms ([],Id.Set.empty,Id.Map.empty,[]) in
let env' = Id.Set.fold
(fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var))
- (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
+ (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
(* PatVars before a real pattern do not need to be matched *)
let stripped_match_from_in =
let rec aux = function
- | [] -> []
- | (_, c) :: q when is_patvar c -> aux q
- | l -> l
- in aux match_from_in in
+ | [] -> []
+ | (_, c) :: q when is_patvar c -> aux q
+ | l -> l
+ in aux match_from_in in
let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in
let rtnpo = match stripped_match_from_in with
- | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
- | l ->
+ | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
+ | l ->
(* Build a return predicate by expansion of the patterns of the "in" clause *)
let thevars, thepats = List.split l in
let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in
let sub_tms = List.map (fun id -> (DAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
let main_sub_eqn = CAst.make @@
([],thepats, (* "|p1,..,pn" *)
- Option.cata (intern_type env')
+ Option.cata (intern_type env')
(DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None))
rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
let catch_all_sub_eqn =
@@ -2040,19 +2040,19 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
[CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
DAst.make @@ GHole(Evar_kinds.ImpossibleCase,IntroAnonymous,None))] (* "=> _" *) in
Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
- in
+ in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
- DAst.make ?loc @@
- GCases (sty, rtnpo, tms, List.flatten eqns')
+ DAst.make ?loc @@
+ GCases (sty, rtnpo, tms, List.flatten eqns')
| CLetTuple (nal, (na,po), b, c) ->
- let env' = reset_tmp_scope env in
- (* "in" is None so no match to add *)
+ let env' = reset_tmp_scope env in
+ (* "in" is None so no match to add *)
let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
let p' = Option.map (fun u ->
- let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
+ let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
(CAst.make na') in
- intern_type env'' u) po in
- DAst.make ?loc @@
+ intern_type env'' u) po in
+ DAst.make ?loc @@
GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b',
intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
| CIf (c, (na,po), b1, b2) ->
@@ -2061,8 +2061,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let p' = Option.map (fun p ->
let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
(CAst.make na') in
- intern_type env'' p) po in
- DAst.make ?loc @@
+ intern_type env'' p) po in
+ DAst.make ?loc @@
GIf (c', (na', p'), intern env b1, intern env b2)
| CHole (k, naming, solve) ->
let k = match k with
@@ -2099,28 +2099,28 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let (_, glb) = Genintern.generic_intern ist gen in
Some glb
in
- DAst.make ?loc @@
- GHole (k, naming, solve)
+ DAst.make ?loc @@
+ GHole (k, naming, solve)
(* Parsing pattern variables *)
| CPatVar n when pattern_mode ->
- DAst.make ?loc @@
- GPatVar (Evar_kinds.SecondOrderPatVar n)
+ DAst.make ?loc @@
+ GPatVar (Evar_kinds.SecondOrderPatVar n)
| CEvar (n, []) when pattern_mode ->
- DAst.make ?loc @@
- GPatVar (Evar_kinds.FirstOrderPatVar n)
+ DAst.make ?loc @@
+ GPatVar (Evar_kinds.FirstOrderPatVar n)
(* end *)
(* Parsing existential variables *)
| CEvar (n, l) ->
- DAst.make ?loc @@
- GEvar (n, List.map (on_snd (intern env)) l)
+ DAst.make ?loc @@
+ GEvar (n, List.map (on_snd (intern env)) l)
| CPatVar _ ->
raise (InternalizationError (loc,IllegalMetavariable))
(* end *)
| CSort s ->
- DAst.make ?loc @@
- GSort s
+ DAst.make ?loc @@
+ GSort s
| CCast (c1, c2) ->
- DAst.make ?loc @@
+ DAst.make ?loc @@
GCast (intern env c1, map_cast_type (intern_type env) c2)
)
and intern_type env = intern (set_type_scope env)
@@ -2172,26 +2172,26 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| Some t ->
let with_letin,(ind,ind_ids,alias_subst,l) =
intern_ind_pattern globalenv ntnvars (None,env.scopes) t in
- let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
- let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
- (* for "in Vect n", we answer (["n","n"],[(loc,"n")])
-
- for "in Vect (S n)", we answer ((match over "m", relevant branch is "S
- n"), abstract over "m") = ([("m","S n")],[(loc,"m")]) where "m" is
- generated from the canonical name of the inductive and outside of
- {forbidden_names_for_gen} *)
- let (match_to_do,nal) =
- let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
- let add_name l = function
+ let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
+ let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
+ (* for "in Vect n", we answer (["n","n"],[(loc,"n")])
+
+ for "in Vect (S n)", we answer ((match over "m", relevant branch is "S
+ n"), abstract over "m") = ([("m","S n")],[(loc,"m")]) where "m" is
+ generated from the canonical name of the inductive and outside of
+ {forbidden_names_for_gen} *)
+ let (match_to_do,nal) =
+ let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
+ let add_name l = function
| { CAst.v = Anonymous } -> l
| { CAst.loc; v = (Name y as x) } -> (y, DAst.make ?loc @@ PatVar x) :: l in
- match case_rel_ctxt,arg_pats with
- (* LetIn in the rel_context *)
- | LocalDef _ :: t, l when not with_letin ->
+ match case_rel_ctxt,arg_pats with
+ (* LetIn in the rel_context *)
+ | LocalDef _ :: t, l when not with_letin ->
canonize_args t l forbidden_names match_acc ((CAst.make Anonymous)::var_acc)
- | [],[] ->
- (add_name match_acc na, var_acc)
- | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
+ | [],[] ->
+ (add_name match_acc na, var_acc)
+ | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
begin match DAst.get c with
| PatVar x ->
let loc = c.CAst.loc in
@@ -2203,10 +2203,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
canonize_args t tt (Id.Set.add fresh forbidden_names)
((fresh,c)::match_acc) ((CAst.make ?loc:(cases_pattern_loc c) @@ Name fresh)::var_acc)
end
- | _ -> assert false in
- let _,args_rel =
- List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
- canonize_args args_rel l forbidden_names_for_gen [] [] in
+ | _ -> assert false in
+ let _,args_rel =
+ List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
+ canonize_args args_rel l forbidden_names_for_gen [] [] in
(Id.Set.of_list (List.map (fun id -> id.CAst.v) ind_ids),alias_subst,match_to_do),
Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal))
| None ->
@@ -2223,33 +2223,33 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let (enva,subscopes') = apply_scope_env env subscopes in
match (impl,rargs) with
| (imp::impl', rargs) when is_status_implicit imp ->
- begin try
- let id = name_of_implicit imp in
- let (_,a) = Id.Map.find id eargs in
- let eargs' = Id.Map.remove id eargs in
- intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
- with Not_found ->
- if List.is_empty rargs && Id.Map.is_empty eargs && not (maximal_insertion_of imp) then
+ begin try
+ let id = name_of_implicit imp in
+ let (_,a) = Id.Map.find id eargs in
+ let eargs' = Id.Map.remove id eargs in
+ intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
+ with Not_found ->
+ if List.is_empty rargs && Id.Map.is_empty eargs && not (maximal_insertion_of imp) then
(* Less regular arguments than expected: complete *)
(* with implicit arguments if maximal insertion is set *)
- []
- else
+ []
+ else
(DAst.map_from_loc (fun ?loc (a,b,c) -> GHole(a,b,c))
(set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c)
) :: aux (n+1) impl' subscopes' eargs rargs
- end
+ end
| (imp::impl', a::rargs') ->
- intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
+ intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
| (imp::impl', []) ->
- if not (Id.Map.is_empty eargs) then
- (let (id,(loc,_)) = Id.Map.choose eargs in
+ if not (Id.Map.is_empty eargs) then
+ (let (id,(loc,_)) = Id.Map.choose eargs in
user_err ?loc (str "Not enough non implicit \
- arguments to accept the argument bound to " ++
- Id.print id ++ str"."));
- []
+ arguments to accept the argument bound to " ++
+ Id.print id ++ str"."));
+ []
| ([], rargs) ->
- assert (Id.Map.is_empty eargs);
- intern_args env subscopes rargs
+ assert (Id.Map.is_empty eargs);
+ intern_args env subscopes rargs
in aux 1 l subscopes eargs rargs
and apply_impargs c env imp subscopes l loc =
@@ -2276,8 +2276,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
intern env c
with
InternalizationError (loc,e) ->
- user_err ?loc ~hdr:"internalize"
- (explain_internalization_error e)
+ user_err ?loc ~hdr:"internalize"
+ (explain_internalization_error e)
(**************************************************************************)
(* Functions to translate constr_expr into glob_constr *)
@@ -2304,8 +2304,8 @@ let intern_gen kind env sigma
c =
let tmp_scope = scope_of_type_kind sigma kind in
internalize env {ids = extract_ids env; unb = false;
- tmp_scope = tmp_scope; scopes = [];
- impls = impls}
+ tmp_scope = tmp_scope; scopes = [];
+ impls = impls}
pattern_mode (ltacvars, Id.Map.empty) c
let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
@@ -2315,7 +2315,7 @@ let intern_pattern globalenv patt =
intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
with
InternalizationError (loc,e) ->
- user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
+ user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
(*********************************************************************)
@@ -2427,11 +2427,11 @@ let intern_context env impl_env binders =
try
let lvar = (empty_ltac_sign, Id.Map.empty) in
let lenv, bl = List.fold_left
- (fun (lenv, bl) b ->
+ (fun (lenv, bl) b ->
let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
- (env, bl))
- ({ids = extract_ids env; unb = false;
- tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
+ (env, bl))
+ ({ids = extract_ids env; unb = false;
+ tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
(lenv.impls, List.map glob_local_binder_of_extended bl)
with InternalizationError (loc,e) ->
user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
@@ -2443,20 +2443,20 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
List.fold_left
(fun (env,sigma,params,n,impls) (na, k, b, t) ->
let t' =
- if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
- else t
+ if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
+ else t
in
let sigma, t = understand_tcc ~flags env sigma ~expected_type:IsType t' in
- match b with
+ match b with
None ->
let r = Retyping.relevance_of_type env sigma t in
let d = LocalAssum (make_annot na r,t) in
let impls =
if k == Implicit then CAst.make (Some (na,true)) :: impls
else CAst.make None :: impls
- in
+ in
(push_rel d env, sigma, d::params, succ n, impls)
- | Some b ->
+ | Some b ->
let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in
let r = Retyping.relevance_of_type env sigma t in
let d = LocalDef (make_annot na r, c, t) in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2e7b832e55..8cce7cd9af 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -150,7 +150,7 @@ val interp_reference : ltac_sign -> qualid -> glob_constr
(** Interpret binders *)
-val interp_binder : env -> evar_map -> Name.t -> constr_expr ->
+val interp_binder : env -> evar_map -> Name.t -> constr_expr ->
types Evd.in_evar_universe_context
val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map * types
@@ -162,7 +162,7 @@ val interp_context_evars :
env -> evar_map -> local_binder_expr list ->
evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))
-(** Locating references of constructions, possibly via a syntactic definition
+(** Locating references of constructions, possibly via a syntactic definition
(these functions do not modify the glob file) *)
val locate_reference : Libnames.qualid -> GlobRef.t
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 41d1da9694..25a87d5f94 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -112,18 +112,18 @@ let type_of_global_ref gr =
| VarRef v ->
"var" ^ type_of_logical_kind (Decls.variable_kind v)
| IndRef ind ->
- let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
+ let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
if mib.Declarations.mind_record <> Declarations.NotRecord then
begin match mib.Declarations.mind_finite with
| Finite -> "indrec"
| BiFinite -> "rec"
- | CoFinite -> "corec"
+ | CoFinite -> "corec"
end
- else
+ else
begin match mib.Declarations.mind_finite with
| Finite -> "ind"
| BiFinite -> "variant"
- | CoFinite -> "coind"
+ | CoFinite -> "coind"
end
| ConstructRef _ -> "constr"
@@ -150,7 +150,7 @@ let dump_ref ?loc filepath modpath ident ty =
| _ -> Option.iter (fun loc ->
let bl,el = interval loc in
dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
- bl el filepath modpath ident ty)
+ bl el filepath modpath ident ty)
) loc
let dump_reference ?loc modpath ident ty =
@@ -193,13 +193,13 @@ let cook_notation (from,df) sc =
(* Next token is a terminal *)
set ntn !j '\''; incr j;
while !i <= l && df.[!i] != ' ' do
- if df.[!i] < ' ' then
- let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in
- (String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i)
- else begin
- if df.[!i] == '\'' then (set ntn !j '\''; incr j);
- set ntn !j df.[!i]; incr j; incr i
- end
+ if df.[!i] < ' ' then
+ let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in
+ (String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i)
+ else begin
+ if df.[!i] == '\'' then (set ntn !j '\''; incr j);
+ set ntn !j df.[!i]; incr j; incr i
+ end
done;
set ntn !j '\''; incr j
end;
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 0de4eb5fa1..2aa002ead1 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -163,7 +163,7 @@ let is_flexible_reference env sigma bound depth f =
| Rel n -> (* since local definitions have been expanded *) false
| Const (kn,_) ->
let cb = Environ.lookup_constant kn env in
- (match cb.const_body with Def _ -> true | _ -> false)
+ (match cb.const_body with Def _ -> true | _ -> false)
| Var id ->
env |> Environ.lookup_named id |> NamedDecl.is_local_def
| Ind _ | Construct _ -> false
@@ -183,19 +183,19 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
let c = if strongly_strict then hd else c in
match kind sigma hd with
| Rel n when (n < bound+depth) && (n >= depth) ->
- let i = bound + depth - n - 1 in
+ let i = bound + depth - n - 1 in
acc.(i) <- update pos rig acc.(i)
| App (f,l) when revpat && is_reversible_pattern sigma bound depth f l ->
let i = bound + depth - EConstr.destRel sigma f - 1 in
- acc.(i) <- update pos rig acc.(i)
+ acc.(i) <- update pos rig acc.(i)
| App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
- if strict then () else
+ if strict then () else
iter_with_full_binders sigma push_lift (frec false) ed c
| Proj (p, _) when rig ->
if strict then () else
iter_with_full_binders sigma push_lift (frec false) ed c
| Case _ when rig ->
- if strict then () else
+ if strict then () else
iter_with_full_binders sigma push_lift (frec false) ed c
| Evar _ -> ()
| _ ->
@@ -611,9 +611,9 @@ let check_inclusion l =
(* Check strict inclusion *)
let rec aux = function
| n1::(n2::_ as nl) ->
- if n1 <= n2 then
- user_err Pp.(str "Sequences of implicit arguments must be of different lengths.");
- aux nl
+ if n1 <= n2 then
+ user_err Pp.(str "Sequences of implicit arguments must be of different lengths.");
+ aux nl
| _ -> () in
aux (List.map snd l)
@@ -621,7 +621,7 @@ let check_rigidity isrigid =
if not isrigid then
user_err (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
-let projection_implicits env p impls =
+let projection_implicits env p impls =
let npars = Projection.npars p in
CList.skipn_at_least npars impls
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 2751b9d40b..8fa69e818a 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -46,18 +46,18 @@ type argument_position =
type implicit_explanation =
| DepRigid of argument_position
(** means that the implicit argument can be found by
- unification along a rigid path (we do not print the arguments of
- this kind if there is enough arguments to infer them) *)
+ unification along a rigid path (we do not print the arguments of
+ this kind if there is enough arguments to infer them) *)
| DepFlex of argument_position
(** means that the implicit argument can be found by unification
along a collapsible path only (e.g. as x in (P x) where P is another
- argument) (we do (defensively) print the arguments of this kind) *)
+ argument) (we do (defensively) print the arguments of this kind) *)
| DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
(** means that the least argument from which the
implicit argument can be inferred is following a collapsible path
- but there is a greater argument from where the implicit argument is
- inferable following a rigid path (useful to know how to print a
- partial application) *)
+ but there is a greater argument from where the implicit argument is
+ inferable following a rigid path (useful to know how to print a
+ partial application) *)
| Manual
(** means the argument has been explicitly set as implicit. *)
@@ -68,8 +68,8 @@ type maximal_insertion = bool (** true = maximal contextual insertion *)
type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
-type implicit_status = (Id.t * implicit_explanation *
- (maximal_insertion * force_inference)) option
+type implicit_status = (Id.t * implicit_explanation *
+ (maximal_insertion * force_inference)) option
(** [None] = Not implicit *)
type implicit_side_condition
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 455471a472..77a2c1c8e6 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -34,7 +34,7 @@ let declare_generalizable_ident table {CAst.loc;v=id} =
" is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
if Id.Pred.mem id table then
user_err ?loc ~hdr:"declare_generalizable_ident"
- ((Id.print id++str" is already declared as a generalizable identifier"))
+ ((Id.print id++str" is already declared as a generalizable identifier"))
else Id.Pred.add id table
let add_generalizable gen table =
@@ -78,7 +78,7 @@ let is_freevar ids env x =
let ungeneralizable loc id =
user_err ?loc ~hdr:"Generalization"
- (str "Unbound and ungeneralizable variable " ++ Id.print id)
+ (str "Unbound and ungeneralizable variable " ++ Id.print id)
let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
let found loc id bdvars l =
@@ -102,16 +102,16 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
let rec vars bound vs c = match DAst.get c with
| GVar id ->
let loc = c.CAst.loc in
- if is_freevar bound (Global.env ()) id then
+ if is_freevar bound (Global.env ()) id then
if List.exists (fun {CAst.v} -> Id.equal v id) vs then vs
else CAst.(make ?loc id) :: vs
- else vs
+ else vs
| _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
- in fun rt ->
+ in fun rt ->
let vars = List.rev (vars bound [] rt) in
List.iter (fun {CAst.loc;v=id} ->
- if not (Id.Set.mem id allowed || find_generalizable_ident id) then
- ungeneralizable loc id) vars;
+ if not (Id.Set.mem id allowed || find_generalizable_ident id) then
+ ungeneralizable loc id) vars;
vars
let rec make_fresh ids env x =
@@ -131,10 +131,10 @@ let combine_params avoid applied needed =
| Name id' -> Id.equal id id'
| Anonymous -> false
in
- if not (List.exists is_id needed) then
- user_err ?loc (str "Wrong argument name: " ++ Id.print id);
- true
- | _ -> false) applied
+ if not (List.exists is_id needed) then
+ user_err ?loc (str "Wrong argument name: " ++ Id.print id);
+ true
+ | _ -> false) applied
in
let named = List.map
(fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false)
@@ -148,10 +148,10 @@ let combine_params avoid applied needed =
| [], [] -> List.rev ids, avoid
| app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named ->
- aux (Id.List.assoc id named :: ids) avoid app need
+ aux (Id.List.assoc id named :: ids) avoid app need
| (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need ->
- aux (x :: ids) avoid app need
+ aux (x :: ids) avoid app need
| x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
@@ -161,7 +161,7 @@ let combine_params avoid applied needed =
aux (t' :: ids) (Id.Set.add id' avoid) app need
| (x,_) :: _, [] ->
- user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
+ user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
in
aux [] avoid applied needed
diff --git a/interp/notation.ml b/interp/notation.ml
index c157cf43fb..efb826a76e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -219,9 +219,9 @@ let declare_delimiters scope key =
| Some oldkey when String.equal oldkey key -> ()
| Some oldkey ->
(* FIXME: implement multikey scopes? *)
- Flags.if_verbose Feedback.msg_info
- (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
- scope_map := String.Map.add scope newsc !scope_map
+ Flags.if_verbose Feedback.msg_info
+ (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
+ scope_map := String.Map.add scope newsc !scope_map
end;
try
let oldscope = String.Map.find key !delimiters_map in
@@ -1077,11 +1077,11 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
| Some scope' when String.equal scope scope' ->
Some (None,None)
| _ ->
- (* If the most recently open scope has a notation/numeral printer
- but not the expected one then we need delimiters *)
- if find scope then
+ (* If the most recently open scope has a notation/numeral printer
+ but not the expected one then we need delimiters *)
+ if find scope then
find_with_delimiters ntn_scope
- else
+ else
find_without_delimiters find (ntn_scope,ntn) scopes
end
| SingleNotation ntn' :: scopes ->
@@ -1646,7 +1646,7 @@ let decompose_notation_key (from,s) =
if n>=len then List.rev dirs else
let pos =
try
- String.index_from s n ' '
+ String.index_from s n ' '
with Not_found -> len
in
let tok =
@@ -1693,7 +1693,7 @@ let pr_named_scope prglob scope sc =
++ pr_scope_classes scope
++ NotationMap.fold
(fun ntn { not_interp = (_, r); not_location = (_, df) } strm ->
- pr_notation_info prglob df r ++ fnl () ++ strm)
+ pr_notation_info prglob df r ++ fnl () ++ strm)
sc.notations (mt ())
let pr_scope prglob scope = pr_named_scope prglob scope (find_scope scope)
@@ -1717,10 +1717,10 @@ let factorize_entries = function
| [] -> []
| (ntn,c)::l ->
let (ntn,l_of_ntn,rest) =
- List.fold_left
+ List.fold_left
(fun (a',l,rest) (a,c) ->
if notation_eq a a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
- (ntn,[c],[]) l in
+ (ntn,[c],[]) l in
(ntn,l_of_ntn)::rest
type symbol_token = WhiteSpace of int | String of string
@@ -1807,7 +1807,7 @@ let error_ambiguous_notation ?loc _ntn =
user_err ?loc (str "Ambiguous notation.")
let error_notation_not_reference ?loc ntn =
- user_err ?loc
+ user_err ?loc
(str "Unable to interpret " ++ quote (str ntn) ++
str " as a reference.")
@@ -1844,14 +1844,14 @@ let locate_notation prglob ntn scope =
prlist_with_sep fnl (fun (ntn,l) ->
let scope = find_default ntn scopes in
prlist_with_sep fnl
- (fun (sc,r,(_,df)) ->
- hov 0 (
- pr_notation_info prglob df r ++
- (if String.equal sc default_scope then mt ()
+ (fun (sc,r,(_,df)) ->
+ hov 0 (
+ pr_notation_info prglob df r ++
+ (if String.equal sc default_scope then mt ()
else (spc () ++ str ": " ++ str sc)) ++
- (if Option.equal String.equal (Some sc) scope
+ (if Option.equal String.equal (Some sc) scope
then spc () ++ str "(default interpretation)" else mt ())))
- l) ntns
+ l) ntns
let collect_notation_in_scope scope sc known =
assert (not (String.equal scope default_scope));
@@ -1864,22 +1864,22 @@ let collect_notations stack =
fst (List.fold_left
(fun (all,knownntn as acc) -> function
| Scope scope ->
- if String.List.mem_assoc scope all then acc
- else
- let (l,knownntn) =
- collect_notation_in_scope scope (find_scope scope) knownntn in
- ((scope,l)::all,knownntn)
+ if String.List.mem_assoc scope all then acc
+ else
+ let (l,knownntn) =
+ collect_notation_in_scope scope (find_scope scope) knownntn in
+ ((scope,l)::all,knownntn)
| SingleNotation ntn ->
if List.mem_f notation_eq ntn knownntn then (all,knownntn)
- else
- let { not_interp = (_, r); not_location = (_, df) } =
+ else
+ let { not_interp = (_, r); not_location = (_, df) } =
NotationMap.find ntn (find_scope default_scope).notations in
- let all' = match all with
- | (s,lonelyntn)::rest when String.equal s default_scope ->
- (s,(df,r)::lonelyntn)::rest
- | _ ->
- (default_scope,[df,r])::all in
- (all',ntn::knownntn))
+ let all' = match all with
+ | (s,lonelyntn)::rest when String.equal s default_scope ->
+ (s,(df,r)::lonelyntn)::rest
+ | _ ->
+ (default_scope,[df,r])::all in
+ (all',ntn::knownntn))
([],[]) stack)
let pr_visible_in_scope prglob (scope,ntns) =
diff --git a/interp/notation.mli b/interp/notation.mli
index bd9b50977b..864e500d56 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -233,8 +233,8 @@ val uninterp_notations : 'a glob_constr_g -> notation_rule list
val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list
val uninterp_ind_pattern_notations : inductive -> notation_rule list
-(** Test if a notation is available in the scopes
- context [scopes]; if available, the result is not None; the first
+(** Test if a notation is available in the scopes
+ context [scopes]; if available, the result is not None; the first
argument is itself not None if a delimiters is needed *)
val availability_of_notation : scope_name option * notation -> subscopes ->
(scope_name option * delimiters option) option
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7e146754b2..ff2498386d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -137,13 +137,13 @@ let rec subst_glob_vars l gc = DAst.map (function
| GVar id as r -> (try DAst.get (Id.List.assoc id l) with Not_found -> r)
| GProd (Name id,bk,t,c) ->
let id =
- try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id
- with Not_found -> id in
+ try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id
+ with Not_found -> id in
GProd (Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
| GLambda (Name id,bk,t,c) ->
let id =
- try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id
- with Not_found -> id in
+ try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id
+ with Not_found -> id in
GLambda (Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
| GHole (x,naming,arg) -> GHole (subst_binder_type_vars l x,naming,arg)
| _ -> DAst.get (map_glob_constr (subst_glob_vars l) gc) (* assume: id is not binding *)
@@ -190,10 +190,10 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
| NCases (sty,rtntypopt,tml,eqnl) ->
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
- let e',t' = match t with
- | None -> e',None
- | Some (ind,nal) ->
- let e',nal' = List.fold_right (fun na (e',nal) ->
+ let e',t' = match t with
+ | None -> e',None
+ | Some (ind,nal) ->
+ let e',nal' = List.fold_right (fun na (e',nal) ->
let e',na' = protect g e' na in
e',na'::nal) nal (e',[]) in
e',Some (CAst.make ?loc (ind,nal')) in
@@ -216,7 +216,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NRec (fk,idl,dll,tl,bl) ->
let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
let e,na = protect g e na in
- (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
+ (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
| NCast (c,k) -> GCast (f e c,map_cast_type (f e) k)
@@ -362,8 +362,8 @@ let compare_recursive_parts recvars found f f' (iterator,subc) =
if aux iterator subc then
match !diff with
| None ->
- let loc1 = loc_of_glob_constr iterator in
- let loc2 = loc_of_glob_constr (Option.get !terminator) in
+ let loc1 = loc_of_glob_constr iterator in
+ let loc2 = loc_of_glob_constr (Option.get !terminator) in
(* Here, we would need a loc made of several parts ... *)
user_err ?loc:(subtract_loc loc1 loc2)
(str "Both ends of the recursive pattern are the same.")
@@ -400,15 +400,15 @@ let notation_constr_and_vars_of_glob_constr recvars a =
| GApp (t, [_]) ->
begin match DAst.get t with
| GVar f when Id.equal f ldots_var ->
- (* Fall on the second part of the recursive pattern w/o having
- found the first part *)
+ (* Fall on the second part of the recursive pattern w/o having
+ found the first part *)
let loc = t.CAst.loc in
- user_err ?loc
- (str "Cannot find where the recursive pattern starts.")
+ user_err ?loc
+ (str "Cannot find where the recursive pattern starts.")
| _ -> aux' c
end
| _c ->
- aux' c
+ aux' c
and aux' x = DAst.with_val (function
| GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id
| GApp (g,args) -> NApp (aux g, List.map aux args)
@@ -419,8 +419,8 @@ let notation_constr_and_vars_of_glob_constr recvars a =
let f {CAst.v=(idl,pat,rhs)} = List.iter (add_id found) idl; (pat,aux rhs) in
NCases (sty,Option.map aux rtntypopt,
List.map (fun (tm,(na,x)) ->
- add_name found na;
- Option.iter
+ add_name found na;
+ Option.iter
(fun {CAst.v=(_,nl)} -> List.iter (add_name found) nl) x;
(aux tm,(na,Option.map (fun {CAst.v=(ind,nal)} -> (ind,nal)) x))) tml,
List.map f eqnl)
@@ -434,9 +434,9 @@ let notation_constr_and_vars_of_glob_constr recvars a =
| GRec (fk,idl,dll,tl,bl) ->
Array.iter (add_id found) idl;
let dll = Array.map (List.map (fun (na,bk,oc,b) ->
- if bk != Explicit then
- user_err Pp.(str "Binders marked as implicit not allowed in notations.");
- add_name found na; (na,Option.map aux oc,aux b))) dll in
+ if bk != Explicit then
+ user_err Pp.(str "Binders marked as implicit not allowed in notations.");
+ add_name found na; (na,Option.map aux oc,aux b))) dll in
NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
| GCast (c,k) -> NCast (aux c,map_cast_type aux k)
| GSort s -> NSort s
@@ -465,7 +465,7 @@ let check_variables_and_reversibility nenv
let check_recvar x =
if Id.List.mem x found then
user_err (Id.print x ++
- strbrk " should only be used in the recursive part of a pattern.") in
+ strbrk " should only be used in the recursive part of a pattern.") in
let check (x, y) = check_recvar x; check_recvar y in
let () = List.iter check foundrec in
let () = List.iter check foundrecbinding in
@@ -476,7 +476,7 @@ let check_variables_and_reversibility nenv
Id.List.mem_assoc_sym x foundrec ||
Id.List.mem_assoc_sym x foundrecbinding
then
- user_err Pp.(str
+ user_err Pp.(str
(Id.to_string x ^
" should not be bound in a recursive pattern of the right-hand side."))
else injective := x :: !injective
@@ -484,19 +484,19 @@ let check_variables_and_reversibility nenv
let check_pair s x y where =
if not (mem_recursive_pair (x,y) where) then
user_err (strbrk "in the right-hand side, " ++ Id.print x ++
- str " and " ++ Id.print y ++ strbrk " should appear in " ++ str s ++
- str " position as part of a recursive pattern.") in
+ str " and " ++ Id.print y ++ strbrk " should appear in " ++ str s ++
+ str " position as part of a recursive pattern.") in
let check_type x typ =
match typ with
| NtnInternTypeAny ->
- begin
- try check_pair "term" x (Id.Map.find x recvars) foundrec
- with Not_found -> check_bound x
- end
+ begin
+ try check_pair "term" x (Id.Map.find x recvars) foundrec
+ with Not_found -> check_bound x
+ end
| NtnInternTypeOnlyBinder ->
- begin
- try check_pair "binding" x (Id.Map.find x recvars) foundrecbinding
- with Not_found -> check_bound x
+ begin
+ try check_pair "binding" x (Id.Map.find x recvars) foundrecbinding
+ with Not_found -> check_bound x
end in
Id.Map.iter check_type vars;
List.rev !injective
@@ -547,49 +547,49 @@ let rec subst_notation_constr subst bound raw =
| NApp (r,rl) ->
let r' = subst_notation_constr subst bound r
and rl' = List.Smart.map (subst_notation_constr subst bound) rl in
- if r' == r && rl' == rl then raw else
- NApp(r',rl')
+ if r' == r && rl' == rl then raw else
+ NApp(r',rl')
| NList (id1,id2,r1,r2,b) ->
let r1' = subst_notation_constr subst bound r1
and r2' = subst_notation_constr subst bound r2 in
- if r1' == r1 && r2' == r2 then raw else
- NList (id1,id2,r1',r2',b)
+ if r1' == r1 && r2' == r2 then raw else
+ NList (id1,id2,r1',r2',b)
| NLambda (n,r1,r2) ->
let r1' = subst_notation_constr subst bound r1
and r2' = subst_notation_constr subst bound r2 in
- if r1' == r1 && r2' == r2 then raw else
- NLambda (n,r1',r2')
+ if r1' == r1 && r2' == r2 then raw else
+ NLambda (n,r1',r2')
| NProd (n,r1,r2) ->
let r1' = subst_notation_constr subst bound r1
and r2' = subst_notation_constr subst bound r2 in
- if r1' == r1 && r2' == r2 then raw else
- NProd (n,r1',r2')
+ if r1' == r1 && r2' == r2 then raw else
+ NProd (n,r1',r2')
| NBinderList (id1,id2,r1,r2,b) ->
let r1' = subst_notation_constr subst bound r1
and r2' = subst_notation_constr subst bound r2 in
- if r1' == r1 && r2' == r2 then raw else
+ if r1' == r1 && r2' == r2 then raw else
NBinderList (id1,id2,r1',r2',b)
| NLetIn (n,r1,t,r2) ->
let r1' = subst_notation_constr subst bound r1 in
let t' = Option.Smart.map (subst_notation_constr subst bound) t in
let r2' = subst_notation_constr subst bound r2 in
- if r1' == r1 && t == t' && r2' == r2 then raw else
- NLetIn (n,r1',t',r2')
+ if r1' == r1 && t == t' && r2' == r2 then raw else
+ NLetIn (n,r1',t',r2')
| NCases (sty,rtntypopt,rl,branches) ->
let rtntypopt' = Option.Smart.map (subst_notation_constr subst bound) rtntypopt
and rl' = List.Smart.map
(fun (a,(n,signopt) as x) ->
- let a' = subst_notation_constr subst bound a in
- let signopt' = Option.map (fun ((indkn,i),nal as z) ->
- let indkn' = subst_mind subst indkn in
- if indkn == indkn' then z else ((indkn',i),nal)) signopt in
- if a' == a && signopt' == signopt then x else (a',(n,signopt')))
+ let a' = subst_notation_constr subst bound a in
+ let signopt' = Option.map (fun ((indkn,i),nal as z) ->
+ let indkn' = subst_mind subst indkn in
+ if indkn == indkn' then z else ((indkn',i),nal)) signopt in
+ if a' == a && signopt' == signopt then x else (a',(n,signopt')))
rl
and branches' = List.Smart.map
(fun (cpl,r as branch) ->
@@ -607,27 +607,27 @@ let rec subst_notation_constr subst bound raw =
let po' = Option.Smart.map (subst_notation_constr subst bound) po
and b' = subst_notation_constr subst bound b
and c' = subst_notation_constr subst bound c in
- if po' == po && b' == b && c' == c then raw else
- NLetTuple (nal,(na,po'),b',c')
+ if po' == po && b' == b && c' == c then raw else
+ NLetTuple (nal,(na,po'),b',c')
| NIf (c,(na,po),b1,b2) ->
let po' = Option.Smart.map (subst_notation_constr subst bound) po
and b1' = subst_notation_constr subst bound b1
and b2' = subst_notation_constr subst bound b2
and c' = subst_notation_constr subst bound c in
- if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
- NIf (c',(na,po'),b1',b2')
+ if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
+ NIf (c',(na,po'),b1',b2')
| NRec (fk,idl,dll,tl,bl) ->
let dll' =
Array.Smart.map (List.Smart.map (fun (na,oc,b as x) ->
let oc' = Option.Smart.map (subst_notation_constr subst bound) oc in
- let b' = subst_notation_constr subst bound b in
- if oc' == oc && b' == b then x else (na,oc',b'))) dll in
+ let b' = subst_notation_constr subst bound b in
+ if oc' == oc && b' == b then x else (na,oc',b'))) dll in
let tl' = Array.Smart.map (subst_notation_constr subst bound) tl in
let bl' = Array.Smart.map (subst_notation_constr subst bound) bl in
if dll' == dll && tl' == tl && bl' == bl then raw else
- NRec (fk,idl,dll',tl',bl')
+ NRec (fk,idl,dll',tl',bl')
| NSort _ -> raw
| NInt _ -> raw
@@ -660,7 +660,7 @@ let abstract_return_type_context pi mklam tml rtno =
Option.map (fun rtn ->
let nal =
List.flatten (List.map (fun (_,(na,t)) ->
- match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
+ match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
List.fold_right mklam nal rtn)
rtno
@@ -1131,11 +1131,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GApp (f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
- if n1 < n2 then
- let l21,l22 = List.chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
- else if n1 > n2 then
- let l11,l12 = List.chop (n1-n2) l1 in DAst.make ?loc @@ GApp (f1,l11),l12, f2,l2
- else f1,l1, f2, l2 in
+ if n1 < n2 then
+ let l21,l22 = List.chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
+ else if n1 > n2 then
+ let l11,l12 = List.chop (n1-n2) l1 in DAst.make ?loc @@ GApp (f1,l11),l12, f2,l2
+ else f1,l1, f2, l2 in
let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
List.fold_left2 (match_ may_use_eta u alp metas)
(match_hd u alp metas sigma f1 f2) l1 l2
@@ -1154,8 +1154,8 @@ let rec match_ inner u alp metas sigma a1 a2 =
let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in
let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in
let sigma =
- try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2'
- with Option.Heterogeneous -> raise No_match
+ try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2'
+ with Option.Heterogeneous -> raise No_match
in
let sigma = List.fold_left2
(fun s (tm1,_) (tm2,_) ->
@@ -1173,24 +1173,24 @@ let rec match_ inner u alp metas sigma a1 a2 =
let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
let sigma = match_in u alp metas sigma b1 b2 in
let (alp,sigma) =
- List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
+ List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
match_in u alp metas sigma c1 c2
| GIf (a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) ->
let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2]
| GRec (fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2)
when match_fix_kind fk1 fk2 && Int.equal (Array.length idl1) (Array.length idl2) &&
- Array.for_all2 (fun l1 l2 -> Int.equal (List.length l1) (List.length l2)) dll1 dll2
- ->
+ Array.for_all2 (fun l1 l2 -> Int.equal (List.length l1) (List.length l2)) dll1 dll2
+ ->
let alp,sigma = Array.fold_left2
- (List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) ->
- let sigma =
- match_in u alp metas
+ (List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) ->
+ let sigma =
+ match_in u alp metas
(match_opt (match_in u alp metas) sigma oc1 oc2) b1 b2
- in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in
+ in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in
let sigma = Array.fold_left2 (match_in u alp metas) sigma tl1 tl2 in
let alp,sigma = Array.fold_right2 (fun id1 id2 alsig ->
- match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
+ match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
| GCast(t1, c1), NCast(t2, c2) ->
match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
@@ -1351,9 +1351,9 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
let le2 = List.length l2 in
if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
then
- raise No_match
+ raise No_match
else
- let l1',more_args = Util.List.chop le2 l1 in
+ let l1',more_args = Util.List.chop le2 l1 in
(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
| r1, NList (x,y,iter,termin,revert) ->
(match_cases_pattern_list (match_cases_pattern_no_more_args)
@@ -1374,10 +1374,10 @@ let match_ind_pattern metas sigma ind pats a2 =
let le2 = List.length l2 in
if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
then
- raise No_match
+ raise No_match
else
- let l1',more_args = Util.List.chop le2 pats in
- (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+ let l1',more_args = Util.List.chop le2 pats in
+ (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
|_ -> raise No_match
let reorder_canonically_substitution terms termlists metas =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 7919d0061f..f9de6b7d6b 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -20,7 +20,7 @@ val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_co
val subst_interpretation :
Mod_subst.substitution -> interpretation -> interpretation
-
+
(** Name of the special identifier used to encode recursive notations *)
val ldots_var : Id.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:29:18 +0000