aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /interp
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml92
-rw-r--r--interp/constrextern.mli4
-rw-r--r--interp/constrintern.ml252
-rw-r--r--interp/constrintern.mli24
-rw-r--r--interp/coqlib.ml12
-rw-r--r--interp/dumpglob.ml36
-rw-r--r--interp/genarg.ml2
-rw-r--r--interp/genarg.mli22
-rw-r--r--interp/implicit_quantifiers.ml136
-rw-r--r--interp/interp.mllib6
-rw-r--r--interp/modintern.ml32
-rw-r--r--interp/modintern.mli2
-rw-r--r--interp/notation.ml68
-rw-r--r--interp/notation.mli20
-rw-r--r--interp/ppextend.ml2
-rw-r--r--interp/ppextend.mli2
-rw-r--r--interp/reserve.ml12
-rw-r--r--interp/smartlocate.ml4
-rw-r--r--interp/syntax_def.mli2
-rw-r--r--interp/topconstr.ml146
-rw-r--r--interp/topconstr.mli24
21 files changed, 450 insertions, 450 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0d2fecfa2..0e61905c7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -266,8 +266,8 @@ let rec same_raw c d =
| r1, RCast(_,c2,_) -> same_raw r1 c2
| RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic"
| _ -> failwith "same_raw"
-
-let same_rawconstr c d =
+
+let same_rawconstr c d =
try same_raw c d; true
with Failure _ | Invalid_argument _ -> false
@@ -292,12 +292,12 @@ let expand_curly_brackets loc mknot ntn (l,ll) =
function
| [] -> []
| a::l ->
- let a' =
+ let a' =
let p = List.nth (wildcards !ntn' 0) i - 2 in
if p>=0 & p+5 <= String.length !ntn' & String.sub !ntn' p 5 = "{ _ }"
then begin
- ntn' :=
- String.sub !ntn' 0 p ^ "_" ^
+ ntn' :=
+ String.sub !ntn' 0 p ^ "_" ^
String.sub !ntn' (p+5) (String.length !ntn' -p-5);
mknot (loc,"{ _ }",([a],[])) end
else a in
@@ -316,7 +316,7 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
(* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
| "- _", [Some (Numeral p)],[] when Bigint.is_strictly_pos p ->
mknot (loc,ntn,([mknot (loc,"( _ )",l)],[]))
- | _ ->
+ | _ ->
match decompose_notation_key ntn, l with
| [Terminal "-"; Terminal x], ([],[]) ->
(try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
@@ -374,14 +374,14 @@ let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
let subst,substlist = match_cases_pattern vars ([],[]) c pat in
(* Reorder canonically the substitution *)
let find x subst =
- try List.assoc x subst
+ try List.assoc x subst
with Not_found -> anomaly "match_aconstr_cases_pattern" in
List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
(* Better to use extern_rawconstr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
- try
+ try
if !Flags.raw_print or !print_no_symbol then raise No_match;
let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
match availability_of_prim_token sc scopes with
@@ -390,20 +390,20 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
let loc = cases_pattern_loc pat in
insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
with No_match ->
- try
+ try
if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_symbol_pattern scopes vars pat
(uninterp_cases_pattern_notations pat)
with No_match ->
match pat with
| PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
- | PatVar (loc,Anonymous) -> CPatAtom (loc, None)
+ | PatVar (loc,Anonymous) -> CPatAtom (loc, None)
| PatCstr(loc,cstrsp,args,na) ->
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
let p = CPatCstr
(loc,extern_reference loc vars (ConstructRef cstrsp),args) in
insert_pat_alias loc p na
-
+
and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
@@ -434,7 +434,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
let subscope = (scopt,scl@scopes') in
List.map (extern_cases_pattern_in_scope subscope vars) c)
substlist in
- insert_pat_delimiters loc
+ insert_pat_delimiters loc
(make_pat_notation loc ntn (l,ll)) key)
| SynDefRule kn ->
let qid = shortest_qualid_of_syndef vars kn in
@@ -443,7 +443,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
with
No_match -> extern_symbol_pattern allscopes vars t rules
-let extern_cases_pattern vars p =
+let extern_cases_pattern vars p =
extern_cases_pattern_in_scope (None,[]) vars p
(**********************************************************************)
@@ -456,7 +456,7 @@ let occur_name na aty =
let is_projection nargs = function
| Some r when not !Flags.raw_print & !print_projections ->
- (try
+ (try
let n = Recordops.find_projection_nparams r + 1 in
if n <= nargs then Some n else None
with Not_found -> None)
@@ -476,13 +476,13 @@ let explicitize loc inctx impl (cf,f) args =
let tail = exprec (q+1) (args,impl) in
let visible =
!Flags.raw_print or
- (!print_implicits & !print_implicits_explicit_args) or
+ (!print_implicits & !print_implicits_explicit_args) or
(!print_implicits_defensive &
is_significant_implicit a impl tail &
not (is_inferable_implicit inctx n imp))
in
- if visible then
- (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail
+ if visible then
+ (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail
else
tail
| a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
@@ -499,7 +499,7 @@ let explicitize loc inctx impl (cf,f) args =
let args1 = exprec 1 (args1,impl1) in
let args2 = exprec (i+1) (args2,impl2) in
CApp (loc,(Some (List.length args1),f),args1@args2)
- | None ->
+ | None ->
let args = exprec 1 (args,impl) in
if args = [] then f else CApp (loc, (None, f), args)
@@ -513,11 +513,11 @@ let extern_app loc inctx impl (cf,f) args =
if args = [] (* maybe caused by a hidden coercion *) then
extern_global loc impl f
else
- if
+ if
((!Flags.raw_print or
(!print_implicits & not !print_implicits_explicit_args)) &
List.exists is_status_implicit impl)
- then
+ then
CAppExpl (loc, (is_projection (List.length args) cf, f), args)
else
explicitize loc inctx impl (cf,CRef f) args
@@ -538,7 +538,7 @@ let rec remove_coercions inctx = function
let nargs = List.length args in
(try match Classops.hide_coercion r with
| Some n when n < nargs && (inctx or n+1 < nargs) ->
- (* We skip a coercion *)
+ (* We skip a coercion *)
let l = list_skipn n args in
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
(* Recursively remove the head coercions *)
@@ -591,11 +591,11 @@ let extern_rawsort = function
let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
- try
+ try
if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_optimal_prim_token scopes r r'
with No_match ->
- try
+ try
if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_symbol scopes vars r' (uninterp_notations r')
with No_match -> match r' with
@@ -622,7 +622,7 @@ let rec extern inctx scopes vars r =
extern_app loc inctx (implicits_of_global ref)
(Some ref,extern_reference rloc vars ref)
args
- | _ ->
+ | _ ->
explicitize loc inctx [] (None,sub_extern false scopes vars f)
(List.map (sub_extern true scopes vars) args))
@@ -643,15 +643,15 @@ let rec extern inctx scopes vars r =
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
-
+
| RCases (loc,sty,rtntypopt,tml,eqns) ->
- let vars' =
+ let vars' =
List.fold_right (name_fold Idset.add)
(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,tm with
- Anonymous, RVar (_,id) when
+ Anonymous, RVar (_,id) when
rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
-> Some Anonymous
| Anonymous, _ -> None
@@ -662,11 +662,11 @@ let rec extern inctx scopes vars r =
let params = list_tabulate
(fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
let args = List.map (function
- | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
+ | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
| Name id -> RVar (dummy_loc,id)) nal in
let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
(extern_typ scopes vars t)) x))) tml in
- let eqns = List.map (extern_eqn inctx scopes vars) eqns in
+ let eqns = List.map (extern_eqn inctx scopes vars) eqns in
CCases (loc,sty,rtntypopt',tml,eqns)
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
@@ -686,23 +686,23 @@ let rec extern inctx scopes vars r =
let vars' = Array.fold_right Idset.add idv vars in
(match fk with
| RFix (nv,n) ->
- let listdecl =
+ let listdecl =
Array.mapi (fun i fi ->
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
let (ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Idset.add) ids vars in
let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
- let n =
+ let n =
match fst nv.(i) with
| None -> None
| Some x -> Some (dummy_loc, out_name (List.nth ids x))
- in
+ in
let ro = extern_recursion_order scopes vars (snd nv.(i)) in
((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
- in
+ in
CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
- | RCoFix n ->
+ | RCoFix n ->
let listdecl =
Array.mapi (fun i fi ->
let (ids,bl) = extern_local_binder scopes vars blv.(i) in
@@ -724,13 +724,13 @@ let rec extern inctx scopes vars r =
| RDynamic (loc,d) -> CDynamic (loc,d)
-and extern_typ (_,scopes) =
+and extern_typ (_,scopes) =
extern true (Some Notation.type_scope,scopes)
and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
and factorize_prod scopes vars aty c =
- try
+ try
if !Flags.raw_print or !print_no_symbol then raise No_match;
([],extern_symbol scopes vars c (uninterp_notations c))
with No_match -> match c with
@@ -742,7 +742,7 @@ and factorize_prod scopes vars aty c =
| c -> ([],extern_typ scopes vars c)
and factorize_lambda inctx scopes vars aty c =
- try
+ try
if !Flags.raw_print or !print_no_symbol then raise No_match;
([],extern_symbol scopes vars c (uninterp_notations c))
with No_match -> match c with
@@ -761,7 +761,7 @@ and extern_local_binder scopes vars = function
extern_local_binder scopes (name_fold Idset.add na vars) l in
(na::ids,
LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
-
+
| (na,bk,None,ty)::l ->
let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
(match extern_local_binder scopes (name_fold Idset.add na vars) l with
@@ -822,7 +822,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
subst in
let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
if l = [] then a else CApp (loc,(None,a),l) in
- if args = [] then e
+ if args = [] then e
else
(* TODO: compute scopt for the extra args, in case, head is a ref *)
explicitize loc false [] (None,e)
@@ -833,7 +833,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
and extern_recursion_order scopes vars = function
RStructRec -> CStructRec
| RWfRec c -> CWfRec (extern true scopes vars c)
- | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
+ | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
Option.map (extern true scopes vars) r)
@@ -895,7 +895,7 @@ let rec raw_of_pat env = function
| PLambda (na,t,c) ->
RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c)
| PIf (c,b1,b2) ->
- RIf (loc, raw_of_pat env c, (Anonymous,None),
+ RIf (loc, raw_of_pat env c, (Anonymous,None),
raw_of_pat env b1, raw_of_pat env b2)
| PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
@@ -910,7 +910,7 @@ let rec raw_of_pat env = function
let mat = simple_cases_matrix_of_branches ind brns brs in
let indnames,rtn =
if p = PMeta None then (Anonymous,None),None
- else
+ else
let nparams,n = Option.get ind_nargs in
return_type_of_predicate ind nparams n (raw_of_pat env p) in
RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat)
@@ -926,22 +926,22 @@ and raw_of_eqn env constr construct_nargs branch =
in
let rec buildrec ids patlist env n b =
if n=0 then
- (dummy_loc, ids,
+ (dummy_loc, ids,
[PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
raw_of_pat env b)
else
match b with
- | PLambda (x,_,b) ->
+ | PLambda (x,_,b) ->
let pat,new_env,new_ids = make_pat x env b ids in
buildrec new_ids (pat::patlist) new_env (n-1) b
- | PLetIn (x,_,b) ->
+ | PLetIn (x,_,b) ->
let pat,new_env,new_ids = make_pat x env b ids in
buildrec new_ids (pat::patlist) new_env (n-1) b
| _ ->
error "Unsupported branch in case-analysis while printing pattern."
- in
+ in
buildrec [] [] env construct_nargs branch
let extern_constr_pattern env pat =
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index a56923fe5..08a74e614 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -34,7 +34,7 @@ val extern_rawconstr : Idset.t -> rawconstr -> constr_expr
val extern_rawtype : Idset.t -> rawconstr -> constr_expr
val extern_constr_pattern : names_context -> constr_pattern -> constr_expr
-(* If [b=true] in [extern_constr b env c] then the variables in the first
+(* 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 *)
val extern_constr : bool -> env -> constr -> constr_expr
@@ -42,7 +42,7 @@ val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
val extern_reference : loc -> Idset.t -> global_reference -> reference
val extern_type : bool -> env -> types -> constr_expr
val extern_sort : sorts -> rawsort
-val extern_rel_context : constr option -> env ->
+val extern_rel_context : constr option -> env ->
rel_context -> local_binder list
(* Printing options *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e4e625205..e49f219af 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -75,7 +75,7 @@ let explain_not_a_constructor ref =
str "Unknown constructor: " ++ pr_reference ref
let explain_unbound_fix_name is_cofix id =
- str "The name" ++ spc () ++ pr_id id ++
+ str "The name" ++ spc () ++ pr_id id ++
spc () ++ str "is not bound in the corresponding" ++ spc () ++
str (if is_cofix then "co" else "") ++ str "fixpoint definition"
@@ -92,13 +92,13 @@ let explain_bad_explicitation_number n po =
let s = match po with
| None -> str "a regular argument"
| Some p -> int p in
- str "Bad explicitation number: found " ++ int n ++
+ str "Bad explicitation number: found " ++ int n ++
str" but was expecting " ++ s
| ExplByName id ->
let s = match po with
| None -> str "a regular argument"
| Some p -> (*pr_id (name_of_position p) in*) failwith "" in
- str "Bad explicitation name: found " ++ pr_id id ++
+ str "Bad explicitation name: found " ++ pr_id id ++
str" but was expecting " ++ s
let explain_internalisation_error e =
@@ -114,7 +114,7 @@ let explain_internalisation_error e =
pp ++ str "."
let error_bad_inductive_type loc =
- user_err_loc (loc,"",str
+ user_err_loc (loc,"",str
"This should be an inductive type applied to names or \"_\".")
let error_inductive_parameter_not_implicit loc =
@@ -135,8 +135,8 @@ and spaces ntn n =
let expand_notation_string ntn n =
let pos = List.nth (wildcards ntn 0) n in
let hd = if pos = 0 then "" else String.sub ntn 0 pos in
- let tl =
- if pos = String.length ntn then ""
+ let tl =
+ if pos = String.length ntn then ""
else String.sub ntn (pos+1) (String.length ntn - pos -1) in
hd ^ "{ _ }" ^ tl
@@ -146,7 +146,7 @@ let contract_notation ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CNotation (_,"{ _ }",([a],[])) :: l ->
+ | CNotation (_,"{ _ }",([a],[])) :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -159,7 +159,7 @@ let contract_pat_notation ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CPatNotation (_,"{ _ }",([a],[])) :: l ->
+ | CPatNotation (_,"{ _ }",([a],[])) :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -175,7 +175,7 @@ let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes
let set_var_scope loc id (_,_,scopt,scopes) varscopes =
let idscopes = List.assoc id varscopes in
- if !idscopes <> None &
+ if !idscopes <> None &
make_current_scope (Option.get !idscopes)
<> make_current_scope (scopt,scopes) then
user_err_loc (loc,"set_var_scope",
@@ -217,28 +217,28 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
begin
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
- try
+ try
let (a,(scopt,subscopes)) = List.assoc id subst in
interp (ids,unb,scopt,subscopes@scopes) a
- with Not_found ->
- try
+ with Not_found ->
+ try
RVar (loc,List.assoc id renaming)
- with Not_found ->
+ with Not_found ->
(* Happens for local notation joint with inductive/fixpoint defs *)
RVar (loc,id)
end
| AList (x,_,iter,terminator,lassoc) ->
- (try
+ (try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (l,(scopt,subscopes)) = List.assoc x substlist in
- let termin =
+ let termin =
subst_aconstr_in_rawconstr loc interp sub subinfos terminator in
- List.fold_right (fun a t ->
+ List.fold_right (fun a t ->
subst_iterator ldots_var t
- (subst_aconstr_in_rawconstr loc interp
+ (subst_aconstr_in_rawconstr loc interp
((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter))
(if lassoc then List.rev l else l) termin
- with Not_found ->
+ with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
| t ->
rawconstr_of_aconstr_with_binders loc (traverse_binder sub)
@@ -285,7 +285,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
(* Is [id] an inductive type potentially with implicit *)
try
let ty,l,impl,argsc = List.assoc id impls in
- let l = List.map
+ let l = List.map
(fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
let tys = string_of_ty ty in
Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
@@ -319,7 +319,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
with _ ->
(* [id] a goal variable *)
RVar (loc,id), [], [], []
-
+
let find_appl_head_data (_,_,_,(_,impls)) = function
| RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
| x -> x,[],[],[]
@@ -364,7 +364,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
find_appl_head_data lvar r, args2
| Ident (loc, id) ->
try intern_var env lvar loc id, args
- with Not_found ->
+ with Not_found ->
let qid = qualid_of_ident id in
try
let r,args2 = intern_non_secvar_qualid loc qid intern env args in
@@ -374,7 +374,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
if !interning_grammar || unb then
(RVar (loc,id), [], [], []),args
else raise e
-
+
let interp_reference vars r =
let (r,_,_,_),_ =
intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
@@ -415,11 +415,11 @@ let simple_product_of_cases_patterns pl =
pl [[],[]]
(* Check linearity of pattern-matching *)
-let rec has_duplicate = function
+let rec has_duplicate = function
| [] -> None
| x::l -> if List.mem x l then (Some x) else has_duplicate l
-let loc_of_lhs lhs =
+let loc_of_lhs lhs =
join_loc (fst (List.hd lhs)) (fst (list_last lhs))
let check_linearity lhs ids =
@@ -436,7 +436,7 @@ let check_number_of_pattern loc n l =
let check_or_pat_variables loc ids idsl =
if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then
- user_err_loc (loc, "", str
+ user_err_loc (loc, "", str
"The components of this disjunctive pattern must bind the same variables.")
let check_constructor_length env loc cstr pl pl0 =
@@ -458,7 +458,7 @@ let alias_of = function
| (id::_,_) -> Name id
let message_redundant_alias (id1,id2) =
- if_verbose warning
+ if_verbose warning
("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2))
(* Expanding notations *)
@@ -487,10 +487,10 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
begin
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
- try
+ try
let (a,(scopt,subscopes)) = List.assoc id subst in
intern (subscopes@scopes) ([],[]) scopt a
- with Not_found ->
+ with Not_found ->
if id = ldots_var then [], [[], PatVar (loc,Name id)] else
anomaly ("Unbound pattern notation variable: "^(string_of_id id))
(*
@@ -506,30 +506,30 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
let args = chop_aconstr_constructor loc cstr args in
let idslpll = List.map (aux Anonymous fullsubst) args in
let ids',pll = product_of_cases_patterns [] idslpll in
- let pl' = List.map (fun (asubst,pl) ->
+ let pl' = List.map (fun (asubst,pl) ->
asubst,PatCstr (loc,cstr,pl,alias)) pll in
ids', pl'
| AList (x,_,iter,terminator,lassoc) ->
- (try
+ (try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (l,(scopt,subscopes)) = List.assoc x substlist in
let termin = aux Anonymous fullsubst terminator in
let idsl,v =
- List.fold_right (fun a (tids,t) ->
+ List.fold_right (fun a (tids,t) ->
let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst,substlist) iter in
let pll = List.map (subst_pat_iterator ldots_var t) u in
tids@uids, List.flatten pll)
(if lassoc then List.rev l else l) termin in
idsl, List.map (fun ((asubst, pl) as x) ->
match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
- with Not_found ->
+ with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
| t -> error_invalid_pattern_notation loc
in aux alias fullsubst a
(* Differentiating between constructors and matching variables *)
type pattern_qualid_kind =
- | ConstrPat of constructor * (identifier list *
+ | ConstrPat of constructor * (identifier list *
((identifier * identifier) list * cases_pattern) list) list
| VarPat of identifier
@@ -554,14 +554,14 @@ let find_constructor ref f aliases pats scopes =
let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) scopes) args in
cstr, idspl1, pats2
| _ -> raise Not_found)
-
+
| TrueGlobal r ->
let rec unf = function
| ConstRef cst ->
let v = Environ.constant_value (Global.env()) cst in
unf (global_of_constr v)
- | ConstructRef cstr ->
- Dumpglob.add_glob loc r;
+ | ConstructRef cstr ->
+ Dumpglob.add_glob loc r;
cstr, [], pats
| _ -> raise Not_found
in unf r
@@ -584,13 +584,13 @@ let maybe_constructor ref f aliases scopes =
str " is understood as a pattern variable");
VarPat (find_pattern_variable ref)
-let mustbe_constructor loc ref f aliases patl scopes =
+let mustbe_constructor loc ref f aliases patl scopes =
try find_constructor ref f aliases patl scopes
with (Environ.NotEvaluableConst _ | Not_found) ->
raise (InternalisationError (loc,NotAConstructor ref))
let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
- let intern_pat = intern_cases_pattern genv in
+ let intern_pat = intern_cases_pattern genv in
match pat with
| CPatAlias (loc, p, id) ->
let aliases' = merge_aliases aliases id in
@@ -604,7 +604,7 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
let pl' = List.map (fun (asubst,pl) ->
(asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in
ids',pl'
- | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]))
+ | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]))
when Bigint.is_strictly_pos p ->
intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
| CPatNotation (_,"( _ )",([a],[])) ->
@@ -621,7 +621,7 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
in ids@ids'', pl
| CPatPrim (loc, p) ->
let a = alias_of aliases in
- let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
+ let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
(tmp_scope,scopes) in
Dumpglob.dump_notation_location (fst (unloc loc)) df;
(ids,[asubst,c])
@@ -660,10 +660,10 @@ let check_capture loc ty = function
()
let locate_if_isevar loc na = function
- | RHole _ ->
+ | RHole _ ->
(try match na with
| Name id -> Reserve.find_reserved_type id
- | Anonymous -> raise Not_found
+ | Anonymous -> raise Not_found
with Not_found -> RHole (loc, Evd.BinderType na))
| x -> x
@@ -674,25 +674,25 @@ let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
of its constructor.")
let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
- | Anonymous ->
+ | Anonymous ->
if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed");
env
- | Name id ->
+ | Name id ->
check_hidden_implicit_parameters id lvar;
(Idset.add id ids, unb,tmpsc,scopes)
let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function
- | Anonymous ->
+ | Anonymous ->
if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed");
env
- | Name id ->
+ | Name id ->
check_hidden_implicit_parameters id lvar;
Dumpglob.dump_binding loc id;
(Idset.add id ids,unb,tmpsc,scopes)
let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
(ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
- let ty =
+ let ty =
if t then ty else
Implicit_quantifiers.implicit_application ids
Implicit_quantifiers.combine_params_freevar ty
@@ -702,11 +702,11 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in
let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
let na = match na with
- | Anonymous ->
- if fail_anonymous then na
+ | Anonymous ->
+ if fail_anonymous then na
else
- let name =
- let id =
+ let name =
+ let id =
match ty with
| CApp (_, (_, CRef (Ident (loc,id))), _) -> id
| _ -> id_of_string "H"
@@ -736,25 +736,25 @@ let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((id
let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
let c = intern (ids,true,tmp_scope,scopes) c in
let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids c in
- let env', c' =
- let abs =
- let pi =
+ let env', c' =
+ let abs =
+ let pi =
match ak with
| Some AbsPi -> true
- | None when tmp_scope = Some Notation.type_scope
+ | None when tmp_scope = Some Notation.type_scope
|| List.mem Notation.type_scope scopes -> true
| _ -> false
- in
+ in
if pi then
(fun (id, loc') acc ->
RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
else
- (fun (id, loc') acc ->
+ (fun (id, loc') acc ->
RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
in
- List.fold_right (fun (id, loc as lid) (env, acc) ->
+ List.fold_right (fun (id, loc as lid) (env, acc) ->
let env' = push_loc_name_env lvar env loc (Name id) in
- (env', abs lid acc)) fvs (env,c)
+ (env', abs lid acc)) fvs (env,c)
in c'
(**********************************************************************)
@@ -762,20 +762,20 @@ let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk a
let merge_impargs l args =
List.fold_right (fun a l ->
- match a with
- | (_,Some (_,(ExplByName id as x))) when
+ match a with
+ | (_,Some (_,(ExplByName id as x))) when
List.exists (function (_,Some (_,y)) -> x=y | _ -> false) args -> l
| _ -> a::l)
- l args
+ l args
-let check_projection isproj nargs r =
+let check_projection isproj nargs r =
match (r,isproj) with
| RRef (loc, ref), Some _ ->
(try
let n = Recordops.find_projection_nparams ref + 1 in
if nargs <> n then
user_err_loc (loc,"",str "Projection has not the right number of explicit parameters.");
- with Not_found ->
+ with Not_found ->
user_err_loc
(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection."))
| _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.")
@@ -811,7 +811,7 @@ let extract_explicit_arg imps args =
id
| ExplByPos (p,_id) ->
let id =
- try
+ try
let imp = List.nth imps (p-1) in
if not (is_status_implicit imp) then failwith "imp";
name_of_implicit imp
@@ -848,7 +848,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let idl = Array.map
(fun (id,(n,order),bl,ty,bd) ->
let intern_ro_arg f =
- let idx =
+ let idx =
match n with
Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
| None -> 0
@@ -856,13 +856,13 @@ let internalise sigma globalenv env allow_patvar lvar c =
let before, after = list_chop idx bl in
let ((ids',_,_,_) as env',rbefore) =
List.fold_left intern_local_binder (env,[]) before in
- let ro = f (intern (ids', unb, tmp_scope, scopes)) in
+ let ro = f (intern (ids', unb, tmp_scope, scopes)) in
let n' = Option.map (fun _ -> List.length before) n in
n', ro, List.fold_left intern_local_binder (env',rbefore) after
in
let n, ro, ((ids',_,_,_),rbl) =
match order with
- | CStructRec ->
+ | CStructRec ->
intern_ro_arg (fun _ -> RStructRec)
| CWfRec c ->
intern_ro_arg (fun f -> RWfRec (f c))
@@ -870,10 +870,10 @@ let internalise sigma globalenv env allow_patvar lvar c =
intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r))
in
let ids'' = List.fold_right Idset.add lf ids' in
- ((n, ro), List.rev rbl,
+ ((n, ro), List.rev rbl,
intern_type (ids',unb,tmp_scope,scopes) ty,
intern (ids'',unb,None,scopes) bd)) dl in
- RRec (loc,RFix
+ RRec (loc,RFix
(Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
Array.map (fun (_,bl,_,_) -> bl) idl,
@@ -914,7 +914,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
RLetIn (loc, na, intern (reset_tmp_scope env) c1,
intern (push_loc_name_env lvar env loc1 na) c2)
| CNotation (loc,"- _",([CPrim (_,Numeral p)],[]))
- when Bigint.is_strictly_pos p ->
+ when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
| CNotation (_,"( _ )",([a],[])) -> intern env a
| CNotation (loc,ntn,args) ->
@@ -946,42 +946,42 @@ let internalise sigma globalenv env allow_patvar lvar c =
let c = intern_notation intern env loc ntn ([],[]) in
find_appl_head_data lvar c, args
| x -> (intern env f,[],[],[]), args in
- let args =
+ let args =
intern_impargs c env impargs args_scopes (merge_impargs l args) in
check_projection isproj (List.length args) c;
- (match c with
+ (match c with
(* Now compact "(f args') args" *)
| RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
| _ -> RApp (loc, c, args))
| CRecord (loc, w, fs) ->
let id, _ = List.hd fs in
- let record =
+ let record =
let (id,_,_,_),_ = intern_applied_reference intern env lvar [] (Ident id) in
match id with
- | RRef (loc, ref) ->
+ | RRef (loc, ref) ->
(try Recordops.find_projection ref
with Not_found -> user_err_loc (loc, "intern", str"Not a projection"))
| c -> user_err_loc (loc_of_rawconstr id, "intern", str"Not a projection")
in
let args =
- let pars = list_make record.Recordops.s_EXPECTEDPARAM (CHole (loc, None)) in
- let fields, rest =
+ let pars = list_make record.Recordops.s_EXPECTEDPARAM (CHole (loc, None)) in
+ let fields, rest =
List.fold_left (fun (args, rest as acc) (na, b) ->
- if b then
- try
+ if b then
+ try
let id = out_name na in
let _, t = List.assoc id rest in
t :: args, List.remove_assoc id rest
with _ -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: args, rest
else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) fs) record.Recordops.s_PROJKIND
- in
- if rest <> [] then
+ in
+ if rest <> [] then
let id, (loc, t) = List.hd rest in
user_err_loc (loc,"intern",(str "Unknown field name " ++ pr_id id))
else pars @ List.rev fields
in
- let constrname =
- Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef record.Recordops.s_CONST))
+ let constrname =
+ Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef record.Recordops.s_CONST))
in
let app = CAppExpl (loc, (None, constrname), args) in
intern env app
@@ -1008,7 +1008,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let env'' = List.fold_left (push_name_env lvar) env ids in
let p' = Option.map (intern_type env'') po in
RIf (loc, c', (na', p'), intern env b1, intern env b2)
- | CHole (loc, k) ->
+ | CHole (loc, k) ->
RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
| CPatVar (loc, n) when allow_patvar ->
RPatVar (loc, n)
@@ -1027,12 +1027,12 @@ let internalise sigma globalenv env allow_patvar lvar c =
and intern_type env = intern (set_type_scope env)
- and intern_local_binder env bind =
+ and intern_local_binder env bind =
intern_local_binder_aux intern intern_type lvar env bind
(* Expands a multiple pattern into a disjunction of multiple patterns *)
and intern_multiple_pattern scopes n (loc,pl) =
- let idsl_pll =
+ let idsl_pll =
List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
check_number_of_pattern loc n pl;
product_of_cases_patterns [] idsl_pll
@@ -1061,7 +1061,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
and intern_case_item (vars,unb,_,scopes as env) (tm,(na,t)) =
let tm' = intern env tm in
let ids,typ = match t with
- | Some t ->
+ | Some t ->
let tids = ids_of_cases_indtype t in
let tids = List.fold_right Idset.add tids Idset.empty in
let t = intern_type (tids,unb,None,scopes) t in
@@ -1081,14 +1081,14 @@ let internalise sigma globalenv env allow_patvar lvar c =
if List.exists ((<>) Anonymous) parnal then
error_inductive_parameter_not_implicit loc;
realnal, Some (loc,ind,nparams,realnal)
- | None ->
+ | None ->
[], None in
let na = match tm', na with
| RVar (_,id), None when Idset.mem id vars -> Name id
| _, None -> Anonymous
| _, Some na -> na in
(tm',(na,typ)), na::ids
-
+
and iterate_prod loc2 env bk ty body nal =
let rec default env bk = function
| (loc1,na)::nal ->
@@ -1100,14 +1100,14 @@ let internalise sigma globalenv env allow_patvar lvar c =
in
match bk with
| Default b -> default env b nal
- | Generalized (b,b',t) ->
+ | Generalized (b,b',t) ->
let env, ibind = intern_generalized_binder intern_type lvar
env [] (List.hd nal) b b' t ty in
let body = intern_type env body in
it_mkRProd ibind body
-
- and iterate_lam loc2 env bk ty body nal =
- let rec default env bk = function
+
+ and iterate_lam loc2 env bk ty body nal =
+ let rec default env bk = function
| (loc1,na)::nal ->
if nal <> [] then check_capture loc1 ty na;
let body = default (push_loc_name_env lvar env loc1 na) bk nal in
@@ -1116,19 +1116,19 @@ let internalise sigma globalenv env allow_patvar lvar c =
| [] -> intern env body
in match bk with
| Default b -> default env b nal
- | Generalized (b, b', t) ->
+ | Generalized (b, b', t) ->
let env, ibind = intern_generalized_binder intern_type lvar
env [] (List.hd nal) b b' t ty in
let body = intern env body in
it_mkRLambda ibind body
-
+
and intern_impargs c env l subscopes args =
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
match (impl,rargs) with
| (imp::impl', rargs) when is_status_implicit imp ->
- begin try
+ begin try
let id = name_of_implicit imp in
let (_,a) = List.assoc id eargs in
let eargs' = List.remove_assoc id eargs in
@@ -1139,16 +1139,16 @@ let internalise sigma globalenv env allow_patvar lvar c =
(* with implicit arguments if maximal insertion is set *)
[]
else
- RHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
+ RHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
aux (n+1) impl' subscopes' eargs rargs
end
| (imp::impl', a::rargs') ->
intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
- | (imp::impl', []) ->
- if eargs <> [] then
+ | (imp::impl', []) ->
+ if eargs <> [] then
(let (id,(loc,_)) = List.hd eargs in
user_err_loc (loc,"",str "Not enough non implicit
- arguments to accept the argument bound to " ++
+ arguments to accept the argument bound to " ++
pr_id id ++ str"."));
[]
| ([], rargs) ->
@@ -1162,8 +1162,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
let (enva,subscopes) = apply_scope_env env subscopes in
(intern enva a) :: (intern_args env subscopes args)
- in
- try
+ in
+ try
intern env c
with
InternalisationError (loc,e) ->
@@ -1175,26 +1175,26 @@ let internalise sigma globalenv env allow_patvar lvar c =
(**************************************************************************)
let extract_ids env =
- List.fold_right Idset.add
+ List.fold_right Idset.add
(Termops.ids_of_rel_context (Environ.rel_context env))
Idset.empty
let intern_gen isarity sigma env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
- let tmp_scope =
+ let tmp_scope =
if isarity then Some Notation.type_scope else None in
internalise sigma env (extract_ids env, false, tmp_scope,[])
allow_patvar (ltacvars,Environ.named_context env, [], impls) c
-
-let intern_constr sigma env c = intern_gen false sigma env c
-let intern_type sigma env c = intern_gen true sigma env c
+let intern_constr sigma env c = intern_gen false sigma env c
+
+let intern_type sigma env c = intern_gen true sigma env c
let intern_pattern env patt =
try
- intern_cases_pattern env [] ([],[]) None patt
- with
+ intern_cases_pattern env [] ([],[]) None patt
+ with
InternalisationError (loc,e) ->
user_err_loc (loc,"internalize",explain_internalisation_error e)
@@ -1204,7 +1204,7 @@ type manual_implicits = (explicitation * (bool * bool * bool)) list
(*********************************************************************)
(* Functions to parse and interpret constructions *)
-let interp_gen kind sigma env
+let interp_gen kind sigma env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
@@ -1217,7 +1217,7 @@ let interp_type sigma env ?(impls=([],[])) c =
interp_gen IsType sigma env ~impls c
let interp_casted_constr sigma env ?(impls=([],[])) c typ =
- interp_gen (OfType (Some typ)) sigma env ~impls c
+ interp_gen (OfType (Some typ)) sigma env ~impls c
let interp_open_constr sigma env c =
Default.understand_tcc sigma env (intern_constr sigma env c)
@@ -1228,8 +1228,8 @@ let interp_open_constr_patvar sigma env c =
let evars = ref (Gmap.empty : (identifier,rawconstr) Gmap.t) in
let rec patvar_to_evar r = match r with
| RPatVar (loc,(_,id)) ->
- ( try Gmap.find id !evars
- with Not_found ->
+ ( try Gmap.find id !evars
+ with Not_found ->
let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in
let ev = Evarutil.e_new_evar sigma env ev in
let rev = REvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
@@ -1253,7 +1253,7 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
let c = intern_gen (kind=IsType) ~impls !evdref env c in
let imps = Implicit_quantifiers.implicits_of_rawterm c in
Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
-
+
let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
env ?(impls=([],[])) c typ =
interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
@@ -1290,7 +1290,7 @@ let interp_aconstr impls (vars,varslist) a =
let a = aconstr_of_rawconstr vars c in
(* Returns [a] and the ordered list of variables with their scopes *)
(* Variables occurring in binders have no relevant scope since bound *)
- let vl = List.map (fun (id,r) ->
+ let vl = List.map (fun (id,r) ->
(id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl in
list_chop (List.length vars) vl, a
@@ -1320,7 +1320,7 @@ let intern_context fail_anonymous sigma env params =
(intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
((extract_ids env,false,None,[]), []) params)
-let interp_context_gen understand_type understand_judgment env bl =
+let interp_context_gen understand_type understand_judgment env bl =
let (env, par, _, impls) =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
@@ -1329,7 +1329,7 @@ let interp_context_gen understand_type understand_judgment env bl =
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
let t = understand_type env t' in
let d = (na,None,t) in
- let impls =
+ let impls =
if k = Implicit then
let na = match na with Name n -> Some n | Anonymous -> None in
(ExplByPos (n, na), (true, true, true)) :: impls
@@ -1343,34 +1343,34 @@ let interp_context_gen understand_type understand_judgment env bl =
(env,[],1,[]) (List.rev bl)
in (env, par), impls
-let interp_context ?(fail_anonymous=false) sigma env params =
+let interp_context ?(fail_anonymous=false) sigma env params =
let bl = intern_context fail_anonymous sigma env params in
- interp_context_gen (Default.understand_type sigma)
+ interp_context_gen (Default.understand_type sigma)
(Default.understand_judgment sigma) env bl
-
+
let interp_context_evars ?(fail_anonymous=false) evdref env params =
let bl = intern_context fail_anonymous !evdref env params in
interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
(Default.understand_judgment_tcc evdref) env bl
-
+
(**********************************************************************)
(* Locating reference, possibly via an abbreviation *)
let locate_reference qid =
match Nametab.locate_extended qid with
| TrueGlobal ref -> ref
- | SynDef kn ->
+ | SynDef kn ->
match Syntax_def.search_syntactic_definition dummy_loc kn with
| [],ARef ref -> ref
| _ -> raise Not_found
let is_global id =
- try
+ try
let _ = locate_reference (qualid_of_ident id) in true
- with Not_found ->
+ with Not_found ->
false
-let global_reference id =
+let global_reference id =
constr_of_global (locate_reference (qualid_of_ident id))
let construct_reference ctx id =
@@ -1379,6 +1379,6 @@ let construct_reference ctx id =
with Not_found ->
global_reference id
-let global_reference_in_absolute_module dir id =
+let global_reference_in_absolute_module dir id =
constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index bfccf03d1..b39f6e18b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -39,8 +39,8 @@ open Pretyping
argument associates a list of implicit positions and scopes to
identifiers declared in the [rel_context] of [env] *)
-type var_internalisation_type = Inductive | Recursive | Method
-
+type var_internalisation_type = Inductive | Recursive | Method
+
type var_internalisation_data =
var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
@@ -79,22 +79,22 @@ val interp_gen : typing_constraint -> evar_map -> env ->
(* Particular instances *)
-val interp_constr : evar_map -> env ->
+val interp_constr : evar_map -> env ->
constr_expr -> constr
-val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
+val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
constr_expr -> types
val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr
-val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
+val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
constr_expr -> types -> constr
(* Accepting evars and giving back the manual implicits in addition. *)
-val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env ->
+val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env ->
?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
@@ -105,7 +105,7 @@ val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
env -> ?impls:full_implicits_env ->
constr_expr -> constr * manual_implicits
-val interp_casted_constr_evars : evar_defs ref -> env ->
+val interp_casted_constr_evars : evar_defs ref -> env ->
?impls:full_implicits_env -> constr_expr -> types -> constr
val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env ->
@@ -117,8 +117,8 @@ val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
(* Interprets constr patterns *)
-val intern_constr_pattern :
- evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
+val intern_constr_pattern :
+ evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
constr_pattern_expr -> patvar list * constr_pattern
val interp_reference : ltac_sign -> reference -> rawconstr
@@ -131,10 +131,10 @@ val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types
(* Interpret contexts: returns extended env and context *)
-val interp_context : ?fail_anonymous:bool ->
+val interp_context : ?fail_anonymous:bool ->
evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
-val interp_context_evars : ?fail_anonymous:bool ->
+val interp_context_evars : ?fail_anonymous:bool ->
evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
(* Locating references of constructions, possibly via a syntactic definition *)
@@ -147,7 +147,7 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
(* Interprets into a abbreviatable constr *)
-val interp_aconstr : implicits_env -> identifier list * identifier list
+val interp_aconstr : implicits_env -> identifier list * identifier list
-> constr_expr -> interpretation
(* Globalization leak for Grammar *)
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 6879dc965..b44cabe8b 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -55,7 +55,7 @@ let gen_constant_in_modules locstr dirs s =
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
prlist_with_sep pr_coma pr_dirpath dirs)
| l ->
- anomalylabstrm ""
+ anomalylabstrm ""
(str (locstr^": found more than once object of name "^s^
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
prlist_with_sep pr_coma pr_dirpath dirs)
@@ -69,7 +69,7 @@ let check_required_library d =
if not (Library.library_is_loaded dir) then
(* Loading silently ...
let m, prefix = list_sep_last d' in
- read_library
+ read_library
(dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
*)
(* or failing ...*)
@@ -80,9 +80,9 @@ let check_required_library d =
let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s
-let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s
+let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s
-let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
+let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
let arith_dir = ["Coq";"Arith"]
let arith_modules = [arith_dir]
@@ -101,7 +101,7 @@ let init_modules = [
init_dir@["Peano"];
init_dir@["Wf"]
]
-
+
let coq_id = id_of_string "Coq"
let init_id = id_of_string "Init"
let arith_id = id_of_string "Arith"
@@ -178,7 +178,7 @@ type coq_bool_data = {
type 'a delayed = unit -> 'a
-let build_bool_type () =
+let build_bool_type () =
{ andb = init_constant ["Datatypes"] "andb";
andb_prop = init_constant ["Datatypes"] "andb_prop";
andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" }
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 79b58da84..9faea5406 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -15,11 +15,11 @@ let glob_file = ref Pervasives.stdout
let open_glob_file f =
glob_file := Pervasives.open_out f
-
+
let close_glob_file () =
Pervasives.close_out !glob_file
-type glob_output_t =
+type glob_output_t =
| NoGlob
| StdOut
| MultFiles
@@ -39,7 +39,7 @@ let dump_to_dotglob f = glob_output := MultFiles
let dump_into_file f = glob_output := File f; open_glob_file f
-let dump_string s =
+let dump_string s =
if dump () then Pervasives.output_string !glob_file s
@@ -68,7 +68,7 @@ let coqdoc_unfreeze (lt,tn,lp) =
open Decl_kinds
let type_of_logical_kind = function
- | IsDefinition def ->
+ | IsDefinition def ->
(match def with
| Definition -> "def"
| Coercion -> "coe"
@@ -102,7 +102,7 @@ let type_of_global_ref gr =
"class"
else
match gr with
- | Libnames.ConstRef cst ->
+ | Libnames.ConstRef cst ->
type_of_logical_kind (Decls.constant_kind cst)
| Libnames.VarRef v ->
"var" ^ type_of_logical_kind (Decls.variable_kind v)
@@ -124,7 +124,7 @@ let remove_sections dir =
dir
let dump_ref loc filepath modpath ident ty =
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) filepath modpath ident ty)
let add_glob_gen loc sp lib_dp ty =
@@ -137,16 +137,16 @@ let add_glob_gen loc sp lib_dp ty =
let ident = Names.string_of_id id in
dump_ref loc filepath modpath ident ty
-let add_glob loc ref =
+let add_glob loc ref =
if dump () && loc <> Util.dummy_loc then
let sp = Nametab.path_of_global ref in
let lib_dp = Lib.library_part ref in
let ty = type_of_global_ref ref in
add_glob_gen loc sp lib_dp ty
-
-let mp_of_kn kn =
- let mp,sec,l = Names.repr_kn kn in
- Names.MPdot (mp,l)
+
+let mp_of_kn kn =
+ let mp,sec,l = Names.repr_kn kn in
+ Names.MPdot (mp,l)
let add_glob_kn loc kn =
if dump () && loc <> Util.dummy_loc then
@@ -155,13 +155,13 @@ let add_glob_kn loc kn =
add_glob_gen loc sp lib_dp "syndef"
let dump_binding loc id = ()
-
+
let dump_definition (loc, id) sec s =
- dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
+ dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
-
+
let dump_reference loc modpath ident ty =
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
let dump_constraint ((loc, n), _, _) sec ty =
@@ -177,7 +177,7 @@ let dump_name (loc, n) sec ty =
let dump_local_binder b sec ty =
if dump () then
match b with
- | Topconstr.LocalRawAssum (nl, _, _) ->
+ | Topconstr.LocalRawAssum (nl, _, _) ->
List.iter (fun x -> dump_name x sec ty) nl
| Topconstr.LocalRawDef _ -> ()
@@ -187,7 +187,7 @@ let dump_modref loc mp ty =
let l = if l = [] then l else Util.list_drop_last l in
let fp = Names.string_of_dirpath dp in
let mp = Names.string_of_dirpath (Names.make_dirpath l) in
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) fp mp "<>" ty)
let dump_moddef loc mp ty =
@@ -197,7 +197,7 @@ let dump_moddef loc mp ty =
dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
let dump_libref loc dp ty =
- dump_string (Printf.sprintf "R%d %s <> <> %s\n"
+ dump_string (Printf.sprintf "R%d %s <> <> %s\n"
(fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
let dump_notation_location pos ((path,df),sc) =
diff --git a/interp/genarg.ml b/interp/genarg.ml
index c6dc12164..091a5c873 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -170,7 +170,7 @@ let globwit_constr_may_eval = ConstrMayEvalArgType
let wit_constr_may_eval = ConstrMayEvalArgType
let rawwit_open_constr_gen b = OpenConstrArgType b
-let globwit_open_constr_gen b = OpenConstrArgType b
+let globwit_open_constr_gen b = OpenConstrArgType b
let wit_open_constr_gen b = OpenConstrArgType b
let rawwit_open_constr = rawwit_open_constr_gen false
diff --git a/interp/genarg.mli b/interp/genarg.mli
index e6747db17..48e5b3c31 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -75,7 +75,7 @@ val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
effective use
\end{verbatim}
-To distinguish between the uninterpreted (raw), globalized and
+To distinguish between the uninterpreted (raw), globalized and
interpreted worlds, we annotate the type [generic_argument] by a
phantom argument which is either [constr_expr], [rawconstr] or
[constr].
@@ -107,11 +107,11 @@ ExtraArgType of string '_a '_b
\end{verbatim}
*)
-(* All of [rlevel], [glevel] and [tlevel] must be non convertible
+(* All of [rlevel], [glevel] and [tlevel] must be non convertible
to ensure the injectivity of the type inference from type
['co generic_argument] to [('a,'co) abstract_argument_type];
this guarantees that, for 'co fixed, the type of
- out_gen is monomorphic over 'a, hence type-safe
+ out_gen is monomorphic over 'a, hence type-safe
*)
type rlevel = constr_expr
@@ -222,29 +222,29 @@ val wit_pair :
(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
type 'a generic_argument
-val fold_list0 :
+val fold_list0 :
('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
-val fold_list1 :
+val fold_list1 :
('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
val fold_opt :
('a generic_argument -> 'c) -> 'c -> 'a generic_argument -> 'c
val fold_pair :
- ('a generic_argument -> 'a generic_argument -> 'c) ->
+ ('a generic_argument -> 'a generic_argument -> 'c) ->
'a generic_argument -> 'c
(* [app_list0] fails if applied to an argument not of tag [List0 t]
for some [t]; it's the responsability of the caller to ensure it *)
-val app_list0 : ('a generic_argument -> 'b generic_argument) ->
+val app_list0 : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
-val app_list1 : ('a generic_argument -> 'b generic_argument) ->
+val app_list1 : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
-val app_opt : ('a generic_argument -> 'b generic_argument) ->
+val app_opt : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
val app_pair :
@@ -294,7 +294,7 @@ val unquote : ('a,'co) abstract_argument_type -> argument_type
val in_gen :
('a,'co) abstract_argument_type -> 'a -> 'co generic_argument
val out_gen :
- ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
+ ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
(* [in_generic] is used in combination with camlp4 [Gramext.action] magic
@@ -308,5 +308,5 @@ val out_gen :
*)
type an_arg_of_this_type
-val in_generic :
+val in_generic :
argument_type -> an_arg_of_this_type -> 'co generic_argument
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a550111a3..7b1a1ff4c 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -26,7 +26,7 @@ open Typeclasses_errors
open Pp
(*i*)
-let ids_of_list l =
+let ids_of_list l =
List.fold_right Idset.add l Idset.empty
let locate_reference qid =
@@ -35,9 +35,9 @@ let locate_reference qid =
| SynDef kn -> true
let is_global id =
- try
+ try
locate_reference (qualid_of_ident id)
- with Not_found ->
+ with Not_found ->
false
let is_freevar ids env x =
@@ -48,13 +48,13 @@ let is_freevar ids env x =
with _ -> not (is_global x)
with _ -> true
-(* Auxilliary functions for the inference of implicitly quantified variables. *)
+(* Auxilliary functions for the inference of implicitly quantified variables. *)
-let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
- let found id bdvars l =
- if List.mem id l then l
+let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
+ let found id bdvars l =
+ if List.mem id l then l
else if not (is_freevar bdvars (Global.env ()) id)
- then l else id :: l
+ then l else id :: l
in
let rec aux bdvars l c = match c with
| CRef (Ident (_,id)) -> found id bdvars l
@@ -63,107 +63,107 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
| c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
in aux bound l c
-let ids_of_names l =
+let ids_of_names l =
List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
-let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
+let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
let rec aux bdvars l c = match c with
((LocalRawAssum (n, _, c)) :: tl) ->
let bound = ids_of_names n in
let l' = free_vars_of_constr_expr c ~bound:bdvars l in
aux (Idset.union (ids_of_list bound) bdvars) l' tl
- | ((LocalRawDef (n, c)) :: tl) ->
+ | ((LocalRawDef (n, c)) :: tl) ->
let bound = match snd n with Anonymous -> [] | Name n -> [n] in
let l' = free_vars_of_constr_expr c ~bound:bdvars l in
aux (Idset.union (ids_of_list bound) bdvars) l' tl
-
+
| [] -> bdvars, l
in aux bound l binders
-let add_name_to_ids set na =
- match na with
- | Anonymous -> set
- | Name id -> Idset.add id set
-
+let add_name_to_ids set na =
+ match na with
+ | Anonymous -> set
+ | Name id -> Idset.add id set
+
let free_vars_of_rawconstr ?(bound=Idset.empty) =
let rec vars bound vs = function
- | RVar (loc,id) ->
+ | RVar (loc,id) ->
if is_freevar bound (Global.env ()) id then
- if List.mem_assoc id vs then vs
+ if List.mem_assoc id vs then vs
else (id, loc) :: vs
else vs
| RApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
- | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
- let vs' = vars bound vs ty in
- let bound' = add_name_to_ids bound na in
+ | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
+ let vs' = vars bound vs ty in
+ let bound' = add_name_to_ids bound na in
vars bound' vs' c
| RCases (loc,sty,rtntypopt,tml,pl) ->
- let vs1 = vars_option bound vs rtntypopt in
- let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
+ let vs1 = vars_option bound vs rtntypopt in
+ let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
List.fold_left (vars_pattern bound) vs2 pl
| RLetTuple (loc,nal,rtntyp,b,c) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 b in
+ let vs1 = vars_return_type bound vs rtntyp in
+ let vs2 = vars bound vs1 b in
let bound' = List.fold_left add_name_to_ids bound nal in
vars bound' vs2 c
- | RIf (loc,c,rtntyp,b1,b2) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 c in
- let vs3 = vars bound vs2 b1 in
+ | RIf (loc,c,rtntyp,b1,b2) ->
+ let vs1 = vars_return_type bound vs rtntyp in
+ let vs2 = vars bound vs1 c in
+ let vs3 = vars bound vs2 b1 in
vars bound vs3 b2
| RRec (loc,fk,idl,bl,tyl,bv) ->
- let bound' = Array.fold_right Idset.add idl bound in
- let vars_fix i vs fid =
- let vs1,bound1 =
- List.fold_left
- (fun (vs,bound) (na,k,bbd,bty) ->
- let vs' = vars_option bound vs bbd in
+ let bound' = Array.fold_right Idset.add idl bound in
+ let vars_fix i vs fid =
+ let vs1,bound1 =
+ List.fold_left
+ (fun (vs,bound) (na,k,bbd,bty) ->
+ let vs' = vars_option bound vs bbd in
let vs'' = vars bound vs' bty in
- let bound' = add_name_to_ids bound na in
+ let bound' = add_name_to_ids bound na in
(vs'',bound')
)
(vs,bound')
bl.(i)
in
- let vs2 = vars bound1 vs1 tyl.(i) in
+ let vs2 = vars bound1 vs1 tyl.(i) in
vars bound1 vs2 bv.(i)
in
array_fold_left_i vars_fix vs idl
- | RCast (loc,c,k) -> let v = vars bound vs c in
+ | RCast (loc,c,k) -> let v = vars bound vs c in
(match k with CastConv (_,t) -> vars bound v t | _ -> v)
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
- and vars_pattern bound vs (loc,idl,p,c) =
- let bound' = List.fold_right Idset.add idl bound in
+ and vars_pattern bound vs (loc,idl,p,c) =
+ let bound' = List.fold_right Idset.add idl bound in
vars bound' vs c
and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
- and vars_return_type bound vs (na,tyopt) =
- let bound' = add_name_to_ids bound na in
+ and vars_return_type bound vs (na,tyopt) =
+ let bound' = add_name_to_ids bound na in
vars_option bound' vs tyopt
- in
+ in
fun rt -> List.rev (vars bound [] rt)
-
+
let rec make_fresh ids env x =
if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
-let fre_ids env ids =
+let fre_ids env ids =
List.filter (is_freevar env (Global.env())) ids
-
+
let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
-let next_name_away_from na avoid =
+let next_name_away_from na avoid =
match na with
| Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon")
| Name id -> make_fresh avoid (Global.env ()) id
let combine_params avoid fn applied needed =
- let named, applied =
- List.partition
+ let named, applied =
+ List.partition
(function
- (t, Some (loc, ExplByName id)) ->
+ (t, Some (loc, ExplByName id)) ->
if not (List.exists (fun (_, (id', _, _)) -> Name id = id') needed) then
user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id);
true
@@ -179,43 +179,43 @@ let combine_params avoid fn applied needed =
| app, (_, (Name id, _, _)) :: need when List.mem_assoc id named ->
aux (List.assoc id named :: ids) avoid app need
-
+
| (x, None) :: app, (None, (Name id, _, _)) :: need ->
aux (x :: ids) avoid app need
-
- | _, (Some cl, (_, _, _) as d) :: need ->
+
+ | _, (Some cl, (_, _, _) as d) :: need ->
let t', avoid' = fn avoid d in
aux (t' :: ids) avoid' app need
| x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
- | [], (None, _ as decl) :: need ->
+ | [], (None, _ as decl) :: need ->
let t', avoid' = fn avoid decl in
aux (t' :: ids) avoid' app need
- | (x,_) :: _, [] ->
+ | (x,_) :: _, [] ->
user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments")
in aux [] avoid applied needed
let combine_params_freevar =
- fun avoid (_, (na, _, _)) ->
+ fun avoid (_, (na, _, _)) ->
let id' = next_name_away_from na avoid in
(CRef (Ident (dummy_loc, id')), Idset.add id' avoid)
-
+
let destClassApp cl =
match cl with
| CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
| CAppExpl (loc, (None, ref), l) -> loc, ref, l
| CRef ref -> loc_of_reference ref, ref, []
| _ -> raise Not_found
-
+
let destClassAppExpl cl =
match cl with
| CApp (loc, (None,CRef ref), l) -> loc, ref, l
| CRef ref -> loc_of_reference ref, ref, []
| _ -> raise Not_found
-let implicit_application env ?(allow_partial=true) f ty =
+let implicit_application env ?(allow_partial=true) f ty =
let is_class =
try
let (loc, r, _ as clapp) = destClassAppExpl ty in
@@ -223,30 +223,30 @@ let implicit_application env ?(allow_partial=true) f ty =
let gr = Nametab.locate qid in
if Typeclasses.is_class gr then Some (clapp, gr) else None
with Not_found -> None
- in
+ in
match is_class with
| None -> ty
- | Some ((loc, id, par), gr) ->
+ | Some ((loc, id, par), gr) ->
let avoid = Idset.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
let c, avoid =
let c = class_info gr in
let (ci, rd) = c.cl_context in
if not allow_partial then
- begin
+ begin
let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 ci in
- if needlen <> applen then
+ if needlen <> applen then
Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
end;
let pars = List.rev (List.combine ci rd) in
let args, avoid = combine_params avoid f par pars in
CAppExpl (loc, (None, id), args), avoid
in c
-
-let implicits_of_rawterm l =
- let rec aux i c =
+
+let implicits_of_rawterm l =
+ let rec aux i c =
match c with
- RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) ->
+ RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) ->
let rest = aux (succ i) b in
if bk = Implicit then
let name =
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 991cfac57..3825f3d87 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,15 +3,15 @@ Topconstr
Ppextend
Notation
Dumpglob
-Genarg
+Genarg
Syntax_def
Smartlocate
Reserve
-Impargs
+Impargs
Implicit_quantifiers
Constrintern
Modintern
-Constrextern
+Constrextern
Coqlib
Discharge
Declare
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 3482dd3a0..041e32bf6 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -15,7 +15,7 @@ open Entries
open Libnames
open Topconstr
open Constrintern
-
+
let rec make_mp mp = function
[] -> mp
| h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
@@ -25,7 +25,7 @@ let rec make_mp mp = function
the module prefix *)
exception BadRef
-let lookup_qualid (modtype:bool) qid =
+let lookup_qualid (modtype:bool) qid =
let rec make_mp mp = function
[] -> mp
| h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
@@ -33,13 +33,13 @@ let lookup_qualid (modtype:bool) qid =
let rec find_module_prefix dir n =
if n<0 then raise Not_found;
let dir',dir'' = list_chop n dir in
- let id',dir''' =
- match dir'' with
- | hd::tl -> hd,tl
+ let id',dir''' =
+ match dir'' with
+ | hd::tl -> hd,tl
| _ -> anomaly "This list should not be empty!"
in
let qid' = make_qualid dir' id' in
- try
+ try
match Nametab.locate qid' with
| ModRef mp -> mp,dir'''
| _ -> raise BadRef
@@ -47,11 +47,11 @@ let lookup_qualid (modtype:bool) qid =
Not_found -> find_module_prefix dir (pred n)
in
try Nametab.locate qid
- with Not_found ->
+ with Not_found ->
let (dir,id) = repr_qualid qid in
let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in
- let mp =
- List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir'
+ let mp =
+ List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir'
in
if modtype then
ModTypeRef (make_ln mp (label_of_id id))
@@ -61,7 +61,7 @@ let lookup_qualid (modtype:bool) qid =
*)
-(* Search for the head of [qid] in [binders].
+(* Search for the head of [qid] in [binders].
If found, returns the module_path/kernel_name created from the dirpath
and the basename. Searches Nametab otherwise.
*)
@@ -71,22 +71,22 @@ let lookup_module (loc,qid) =
Dumpglob.dump_modref loc mp "modtype"; mp
with
| Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid)
-
+
let lookup_modtype (loc,qid) =
try
let mp = Nametab.locate_modtype qid in
Dumpglob.dump_modref loc mp "mod"; mp
with
- | Not_found ->
+ | Not_found ->
Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
-let transl_with_decl env = function
+let transl_with_decl env = function
| CWith_Module ((_,fqid),qid) ->
With_Module (fqid,lookup_module qid)
| CWith_Definition ((_,fqid),c) ->
With_Definition (fqid,interp_constr Evd.empty env c)
-let rec interp_modexpr env = function
+let rec interp_modexpr env = function
| CMEident qid ->
MSEident (lookup_module qid)
| CMEapply (me1,me2) ->
@@ -94,10 +94,10 @@ let rec interp_modexpr env = function
let me2 = interp_modexpr env me2 in
MSEapply(me1,me2)
-let rec interp_modtype env = function
+let rec interp_modtype env = function
| CMTEident qid ->
MSEident (lookup_modtype qid)
- | CMTEapply (mty1,me) ->
+ | CMTEapply (mty1,me) ->
let mty' = interp_modtype env mty1 in
let me' = interp_modexpr env me in
MSEapply(mty',me')
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 1f27e3c18..f39205d8b 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -18,7 +18,7 @@ open Names
open Topconstr
(*i*)
-(* Module expressions and module types are interpreted relatively to
+(* Module expressions and module types are interpreted relatively to
eventual functor or funsig arguments. *)
val interp_modtype : env -> module_type_ast -> module_struct_entry
diff --git a/interp/notation.ml b/interp/notation.ml
index 58c28149d..8dec15b60 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -30,7 +30,7 @@ open Ppextend
no interpretation for negative numbers in [nat]); interpreters both for
terms and patterns can be set; these interpreters are in permanent table
[numeral_interpreter_tab]
- - a set of ML printers for expressions denoting numbers parsable in
+ - a set of ML printers for expressions denoting numbers parsable in
this scope
- a set of interpretations for infix (more generally distfix) notations
- an optional pair of delimiters which, when occurring in a syntactic
@@ -92,10 +92,10 @@ let scope_stack = ref []
let current_scopes () = !scope_stack
-let scope_is_open_in_scopes sc l =
+let scope_is_open_in_scopes sc l =
List.mem (Scope sc) l
-let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
+let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
(* TODO: push nat_scope, z_scope, ... in scopes summary *)
@@ -118,7 +118,7 @@ let classify_scope (local,_,_ as o) =
let export_scope (local,_,_ as x) = if local then None else Some x
-let (inScope,outScope) =
+let (inScope,outScope) =
declare_object {(default_object "SCOPE") with
cache_function = cache_scope;
open_function = open_scope;
@@ -149,7 +149,7 @@ let declare_delimiters scope key =
let sc = find_scope scope in
if sc.delimiters <> None && Flags.is_verbose () then begin
let old = Option.get sc.delimiters in
- Flags.if_verbose
+ Flags.if_verbose
warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
end;
let sc = { sc with delimiters = Some key } in
@@ -160,10 +160,10 @@ let declare_delimiters scope key =
end;
delimiters_map := Gmap.add key scope !delimiters_map
-let find_delimiters_scope loc key =
+let find_delimiters_scope loc key =
try Gmap.find key !delimiters_map
- with Not_found ->
- user_err_loc
+ with Not_found ->
+ user_err_loc
(loc, "find_delimiters", str ("Unknown scope delimiting key "^key^"."))
(* Uninterpretation tables *)
@@ -201,7 +201,7 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
(**********************************************************************)
(* Interpreting numbers (not in summary because functional objects) *)
-type required_module = full_path * string list
+type required_module = full_path * string list
type 'a prim_token_interpreter =
loc -> 'a -> rawconstr
@@ -218,7 +218,7 @@ let prim_token_interpreter_tab =
(Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
let add_prim_token_interpreter sc interp =
- try
+ try
let cont = Hashtbl.find prim_token_interpreter_tab sc in
Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
with Not_found ->
@@ -228,7 +228,7 @@ let add_prim_token_interpreter sc interp =
let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
declare_scope sc;
add_prim_token_interpreter sc interp;
- List.iter (fun pat ->
+ List.iter (fun pat ->
Hashtbl.add prim_token_key_table (rawconstr_key pat) (sc,uninterp,b))
patl
@@ -265,7 +265,7 @@ let find_with_delimiters = function
| None -> None
let rec find_without_delimiters find (ntn_scope,ntn) = function
- | Scope scope :: scopes ->
+ | Scope scope :: scopes ->
(* Is the expected ntn/numpr attached to the most recently open scope? *)
if Some scope = ntn_scope then
Some (None,None)
@@ -277,7 +277,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
else
find_without_delimiters find (ntn_scope,ntn) scopes
| SingleNotation ntn' :: scopes ->
- if ntn_scope = None & ntn = Some ntn' then
+ if ntn_scope = None & ntn = Some ntn' then
Some (None,None)
else
find_without_delimiters find (ntn_scope,ntn) scopes
@@ -376,7 +376,7 @@ let availability_of_notation (ntn_scope,ntn) scopes =
find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
let uninterp_prim_token c =
- try
+ try
let (sc,numpr,_) = Hashtbl.find prim_token_key_table (rawconstr_key c) in
match numpr c with
| None -> raise No_match
@@ -384,7 +384,7 @@ let uninterp_prim_token c =
with Not_found -> raise No_match
let uninterp_prim_token_cases_pattern c =
- try
+ try
let k = cases_pattern_key c in
let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in
if not b then raise No_match;
@@ -480,7 +480,7 @@ let rebuild_arguments_scope (req,r,l) =
let l1,_ = list_chop (List.length l' - List.length l) l' in
(req,r,l1@l)
-let (inArgumentsScope,outArgumentsScope) =
+let (inArgumentsScope,outArgumentsScope) =
declare_object {(default_object "ARGUMENTS-SCOPE") with
cache_function = cache_arguments_scope;
load_function = load_arguments_scope;
@@ -517,7 +517,7 @@ type symbol =
let rec string_of_symbol = function
| NonTerminal _ -> ["_"]
| Terminal s -> [s]
- | SProdList (_,l) ->
+ | SProdList (_,l) ->
let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
| Break _ -> []
@@ -530,14 +530,14 @@ let decompose_notation_key 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 =
match String.sub s n (pos-n) with
| "_" -> NonTerminal (id_of_string "_")
| s -> Terminal (drop_simple_quotes s) in
- decomp_ntn (tok::dirs) (pos+1)
+ decomp_ntn (tok::dirs) (pos+1)
in
decomp_ntn [] 0
@@ -554,12 +554,12 @@ let classes_of_scope sc =
let pr_scope_classes sc =
let l = classes_of_scope sc in
if l = [] then mt()
- else
+ else
hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++
spc() ++ prlist_with_sep spc pr_class l) ++ fnl()
let pr_notation_info prraw ntn c =
- str "\"" ++ str ntn ++ str "\" := " ++
+ str "\"" ++ str ntn ++ str "\" := " ++
prraw (rawconstr_of_aconstr dummy_loc c)
let pr_named_scope prraw scope sc =
@@ -567,7 +567,7 @@ let pr_named_scope prraw scope sc =
match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
| 0 -> str "No lonely notation"
| n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
- else
+ else
str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
++ fnl ()
++ pr_scope_classes scope
@@ -579,7 +579,7 @@ let pr_named_scope prraw scope sc =
let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
let pr_scopes prraw =
- Gmap.fold
+ Gmap.fold
(fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
!scope_map (mt ())
@@ -611,7 +611,7 @@ let browse_notation strict ntn map =
let trms = List.filter (function Terminal _ -> true | _ -> false) toks in
if strict then [Terminal ntn] = trms else List.mem (Terminal ntn) trms in
let l =
- Gmap.fold
+ Gmap.fold
(fun scope_name sc ->
Gmap.fold (fun ntn ((_,r),df) l ->
if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
@@ -621,7 +621,7 @@ let browse_notation strict ntn map =
let global_reference_of_notation test (ntn,(sc,c,_)) =
match c with
| ARef ref when test ref -> Some (ntn,sc,ref)
- | AApp (ARef ref, l) when List.for_all isAVar_or_AHole l & test ref ->
+ | AApp (ARef ref, l) when List.for_all isAVar_or_AHole l & test ref ->
Some (ntn,sc,ref)
| _ -> None
@@ -643,7 +643,7 @@ let interp_notation_as_global_reference loc test ntn sc =
match Option.List.flatten refs with
| [_,_,ref] -> ref
| [] -> error_notation_not_reference loc ntn
- | refs ->
+ | refs ->
let f (ntn,sc,ref) = find_default ntn !scope_stack = Some sc in
match List.filter f refs with
| [_,_,ref] -> ref
@@ -657,14 +657,14 @@ let locate_notation prraw ntn scope =
str "Unknown notation"
else
t (str "Notation " ++
- tab () ++ str "Scope " ++ tab () ++ fnl () ++
+ tab () ++ str "Scope " ++ tab () ++ fnl () ++
prlist (fun (ntn,l) ->
let scope = find_default ntn scopes in
- prlist
+ prlist
(fun (sc,r,(_,df)) ->
hov 0 (
pr_notation_info prraw df r ++ tbrk (1,2) ++
- (if sc = default_scope then mt () else (str ": " ++ str sc)) ++
+ (if sc = default_scope then mt () else (str ": " ++ str sc)) ++
tbrk (1,2) ++
(if Some sc = scope then str "(default interpretation)" else mt ())
++ fnl ()))
@@ -694,7 +694,7 @@ let collect_notations stack =
let all' = match all with
| (s,lonelyntn)::rest when s = default_scope ->
(s,(df,r)::lonelyntn)::rest
- | _ ->
+ | _ ->
(default_scope,[df,r])::all in
(all',ntn::knownntn))
([],[]) stack)
@@ -706,11 +706,11 @@ let pr_visible_in_scope prraw (scope,ntns) =
ntns (mt ()) in
(if scope = default_scope then
str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt())
- else
+ else
str "Visible in scope " ++ str scope)
++ fnl () ++ strm
-let pr_scope_stack prraw stack =
+let pr_scope_stack prraw stack =
List.fold_left
(fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ())
(mt ()) (collect_notations stack)
@@ -725,7 +725,7 @@ let pr_visibility prraw = function
type unparsing_rule = unparsing list * precedence
(* Concrete syntax for symbolic-extension table *)
-let printing_rules =
+let printing_rules =
ref (Gmap.empty : (string,unparsing_rule) Gmap.t)
let declare_notation_printing_rule ntn unpl =
@@ -765,7 +765,7 @@ let init () =
printing_rules := Gmap.empty;
class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
-let _ =
+let _ =
declare_summary "symbols"
{ freeze_function = freeze;
unfreeze_function = unfreeze;
diff --git a/interp/notation.mli b/interp/notation.mli
index 57e0deb10..f3036f226 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -46,7 +46,7 @@ val scope_is_open : scope_name -> bool
(* Open scope *)
-val open_close_scope :
+val open_close_scope :
(* locality *) bool * (* open *) bool * scope_name -> unit
(* Extend a list of scopes *)
@@ -66,7 +66,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name
an appropriate error message *)
type notation_location = dir_path * string
-type required_module = full_path * string list
+type required_module = full_path * string list
type cases_pattern_status = bool (* true = use prim token in patterns *)
type 'a prim_token_interpreter =
@@ -86,18 +86,18 @@ val declare_string_interpreter : scope_name -> required_module ->
val interp_prim_token : loc -> prim_token -> local_scopes ->
rawconstr * (notation_location * scope_name option)
-val interp_prim_token_cases_pattern : loc -> prim_token -> name ->
+val interp_prim_token_cases_pattern : loc -> prim_token -> name ->
local_scopes -> cases_pattern * (notation_location * scope_name option)
(* Return the primitive token associated to a [term]/[cases_pattern];
raise [No_match] if no such token *)
-val uninterp_prim_token :
+val uninterp_prim_token :
rawconstr -> scope_name * prim_token
-val uninterp_prim_token_cases_pattern :
+val uninterp_prim_token_cases_pattern :
cases_pattern -> name * scope_name * prim_token
-val availability_of_prim_token :
+val availability_of_prim_token :
scope_name -> local_scopes -> delimiters option option
(*s Declare and interpret back and forth a notation *)
@@ -125,7 +125,7 @@ val uninterp_cases_pattern_notations : cases_pattern ->
(* 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 -> local_scopes ->
+val availability_of_notation : scope_name option * notation -> local_scopes ->
(scope_name option * delimiters option) option
(*s Declare and test the level of a (possibly uninterpreted) notation *)
@@ -135,7 +135,7 @@ val level_of_notation : notation -> level (* raise [Not_found] if no level *)
(*s** Miscellaneous *)
-val interp_notation_as_global_reference : loc -> (global_reference -> bool) ->
+val interp_notation_as_global_reference : loc -> (global_reference -> bool) ->
notation -> delimiters option -> global_reference
(* Checks for already existing notations *)
@@ -143,7 +143,7 @@ val exists_notation_in_scope : scope_name option -> notation ->
interpretation -> bool
(* Declares and looks for scopes associated to arguments of a global ref *)
-val declare_arguments_scope :
+val declare_arguments_scope :
bool (* true=local *) -> global_reference -> scope_name option list -> unit
val find_arguments_scope : global_reference -> scope_name option list
@@ -167,7 +167,7 @@ val decompose_notation_key : notation -> symbol list
(* Prints scopes (expect a pure aconstr printer *)
val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
-val locate_notation : (rawconstr -> std_ppcmds) -> notation ->
+val locate_notation : (rawconstr -> std_ppcmds) -> notation ->
scope_name option -> std_ppcmds
val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index baef2c628..a4142d694 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -50,7 +50,7 @@ let ppcmd_of_cut = function
| PpBrk(n1,n2) -> brk(n1,n2)
| PpTbrk(n1,n2) -> tbrk(n1,n2)
-type unparsing =
+type unparsing =
| UnpMetaVar of int * parenRelation
| UnpListMetaVar of int * parenRelation * unparsing list
| UnpTerminal of string
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index bddd1eef2..3d09587d0 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -40,7 +40,7 @@ val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
val ppcmd_of_cut : ppcut -> std_ppcmds
-type unparsing =
+type unparsing =
| UnpMetaVar of int * parenRelation
| UnpListMetaVar of int * parenRelation * unparsing list
| UnpTerminal of string
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 93fc60dfb..9d8412825 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -24,22 +24,22 @@ let cache_reserved_type (_,(id,t)) =
reserve_table := Idmap.add id t !reserve_table
let (in_reserved, _) =
- declare_object {(default_object "RESERVED-TYPE") with
+ declare_object {(default_object "RESERVED-TYPE") with
cache_function = cache_reserved_type }
-let _ =
+let _ =
Summary.declare_summary "reserved-type"
{ Summary.freeze_function = (fun () -> !reserve_table);
Summary.unfreeze_function = (fun r -> reserve_table := r);
Summary.init_function = (fun () -> reserve_table := Idmap.empty) }
-let declare_reserved_type (loc,id) t =
+let declare_reserved_type (loc,id) t =
if id <> root_of_id id then
user_err_loc(loc,"declare_reserved_type",
(pr_id id ++ str
" is not reservable: it must have no trailing digits, quote, or _"));
begin try
- let _ = Idmap.find id !reserve_table in
+ let _ = Idmap.find id !reserve_table in
user_err_loc(loc,"declare_reserved_type",
(pr_id id++str" is already bound to a type"))
with Not_found -> () end;
@@ -66,7 +66,7 @@ let rec unloc = function
RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
| RRec (_,fk,idl,bl,tyl,bv) ->
RRec (dummy_loc,fk,idl,
- Array.map (List.map
+ Array.map (List.map
(fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty)))
bl,
Array.map unloc tyl,
@@ -82,7 +82,7 @@ let rec unloc = function
let anonymize_if_reserved na t = match na with
| Name id as na ->
- (try
+ (try
if not !Flags.raw_print & unloc t = find_reserved_type id
then RHole (dummy_loc,Evd.BinderType na)
else t
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 07ae87fa0..f16f5363c 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -24,7 +24,7 @@ open Topconstr
let global_of_extended_global = function
| TrueGlobal ref -> ref
- | SynDef kn ->
+ | SynDef kn ->
match search_syntactic_definition dummy_loc kn with
| [],ARef ref -> ref
| _ -> raise Not_found
@@ -33,7 +33,7 @@ let locate_global_with_alias (loc,qid) =
let ref = Nametab.locate_extended qid in
try global_of_extended_global ref
with Not_found ->
- user_err_loc (loc,"",pr_qualid qid ++
+ user_err_loc (loc,"",pr_qualid qid ++
str " is bound to a notation that does not denote a reference")
let global_inductive_with_alias r =
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 3ba78e91d..747f7b9da 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -21,7 +21,7 @@ open Libnames
type syndef_interpretation = (identifier * subscopes) list * aconstr
-val declare_syntactic_definition : bool -> identifier -> bool ->
+val declare_syntactic_definition : bool -> identifier -> bool ->
syndef_interpretation -> unit
val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index eb46a5d6e..bea0eae31 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -23,7 +23,7 @@ open Mod_subst
(* This is the subtype of rawconstr allowed in syntactic extensions *)
(* For AList: first constr is iterator, second is terminator;
- first id is where each argument of the list has to be substituted
+ first id is where each argument of the list has to be substituted
in iterator and snd id is alternative name just for printing;
boolean is associativity *)
@@ -43,7 +43,7 @@ type aconstr =
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
| ARec of fix_kind * identifier array *
- (name * aconstr option * aconstr) list array * aconstr array *
+ (name * aconstr option * aconstr) list array * aconstr array *
aconstr array
| ASort of rawsort
| AHole of Evd.hole_kind
@@ -55,7 +55,7 @@ type aconstr =
let name_to_ident = function
| Anonymous -> error "This expression should be a simple identifier."
- | Name id -> id
+ | Name id -> id
let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
@@ -92,8 +92,8 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
| None -> e',None
- | Some (ind,npar,nal) ->
- let e',nal' = List.fold_right (fun na (e',nal) ->
+ | Some (ind,npar,nal) ->
+ let e',nal' = List.fold_right (fun na (e',nal) ->
let e',na' = g e' na in e',na'::nal) nal (e',[]) in
e',Some (loc,ind,npar,nal') in
let e',na' = g e' na in
@@ -105,7 +105,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
(loc,idl,patl,f e rhs)) eqnl in
RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
| ALetTuple (nal,(na,po),b,c) ->
- let e,nal = list_fold_map g e nal in
+ let e,nal = list_fold_map g e nal in
let e,na = g e na in
RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
| AIf (c,(na,po),b1,b2) ->
@@ -117,8 +117,8 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let e,na = g e na in
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
- | ACast (c,k) -> RCast (loc,f e c,
- match k with
+ | ACast (c,k) -> RCast (loc,f e c,
+ match k with
| CastConv (k,t) -> CastConv (k,f e t)
| CastCoerce -> CastCoerce)
| ASort x -> RSort (loc,x)
@@ -127,7 +127,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
| ARef x -> RRef (loc,x)
let rec rawconstr_of_aconstr loc x =
- let rec aux () x =
+ let rec aux () x =
rawconstr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x
in aux () x
@@ -167,7 +167,7 @@ let discriminate_patterns foundvars nl l1 l2 =
let rec aux n c1 c2 = match c1,c2 with
| RVar (_,v1), RVar (_,v2) when v1<>v2 ->
if !diff = None then (diff := Some (v1,v2,(n>=nl)); true)
- else
+ else
!diff = Some (v1,v2,(n>=nl)) or !diff = Some (v2,v1,(n<nl))
or (error
"Both ends of the recursive pattern differ in more than one place")
@@ -188,7 +188,7 @@ let aconstr_and_vars_of_rawconstr a =
let found = ref [] in
let rec aux = function
| RVar (_,id) -> found := id::!found; AVar id
- | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args
+ | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args
| RApp (_,RVar (_,f),[RApp (_,t,[c]);d]) when f = ldots_var ->
(* Special case for alternative (recursive) notation of application *)
let x,y,lassoc = discriminate_patterns found 0 [c] [d] in
@@ -216,13 +216,13 @@ let aconstr_and_vars_of_rawconstr a =
AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
| RRec (_,fk,idl,dll,tl,bl) ->
Array.iter (fun id -> found := id::!found) idl;
- let dll = Array.map (List.map (fun (na,bk,oc,b) ->
- if bk <> Explicit then
+ let dll = Array.map (List.map (fun (na,bk,oc,b) ->
+ if bk <> Explicit then
error "Binders marked as implicit not allowed in notations.";
add_name found na; (na,Option.map aux oc,aux b))) dll in
ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
- | RCast (_,c,k) -> ACast (aux c,
- match k with CastConv (k,t) -> CastConv (k,aux t)
+ | RCast (_,c,k) -> ACast (aux c,
+ match k with CastConv (k,t) -> CastConv (k,aux t)
| CastCoerce -> CastCoerce)
| RSort (_,s) -> ASort s
| RHole (_,w) -> AHole w
@@ -277,65 +277,65 @@ let aconstr_of_rawconstr vars a =
let aconstr_of_constr avoiding t =
aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t)
-let rec subst_pat subst pat =
+let rec subst_pat subst pat =
match pat with
| PatVar _ -> pat
- | PatCstr (loc,((kn,i),j),cpl,n) ->
- let kn' = subst_kn subst kn
+ | PatCstr (loc,((kn,i),j),cpl,n) ->
+ let kn' = subst_kn subst kn
and cpl' = list_smartmap (subst_pat subst) cpl in
if kn' == kn && cpl' == cpl then pat else
PatCstr (loc,((kn',i),j),cpl',n)
let rec subst_aconstr subst bound raw =
match raw with
- | ARef ref ->
- let ref',t = subst_global subst ref in
+ | ARef ref ->
+ let ref',t = subst_global subst ref in
if ref' == ref then raw else
aconstr_of_constr bound t
| AVar _ -> raw
- | AApp (r,rl) ->
- let r' = subst_aconstr subst bound r
+ | AApp (r,rl) ->
+ let r' = subst_aconstr subst bound r
and rl' = list_smartmap (subst_aconstr subst bound) rl in
if r' == r && rl' == rl then raw else
AApp(r',rl')
- | AList (id1,id2,r1,r2,b) ->
+ | AList (id1,id2,r1,r2,b) ->
let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
AList (id1,id2,r1',r2',b)
- | ALambda (n,r1,r2) ->
+ | ALambda (n,r1,r2) ->
let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
ALambda (n,r1',r2')
- | AProd (n,r1,r2) ->
+ | AProd (n,r1,r2) ->
let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
AProd (n,r1',r2')
- | ALetIn (n,r1,r2) ->
- let r1' = subst_aconstr subst bound r1
+ | ALetIn (n,r1,r2) ->
+ let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
ALetIn (n,r1',r2')
- | ACases (sty,rtntypopt,rl,branches) ->
+ | ACases (sty,rtntypopt,rl,branches) ->
let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
and rl' = list_smartmap
- (fun (a,(n,signopt) as x) ->
+ (fun (a,(n,signopt) as x) ->
let a' = subst_aconstr subst bound a in
let signopt' = Option.map (fun ((indkn,i),n,nal as z) ->
let indkn' = subst_kn subst indkn in
if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
rl
- and branches' = list_smartmap
+ and branches' = list_smartmap
(fun (cpl,r as branch) ->
let cpl' = list_smartmap (subst_pat subst) cpl
and r' = subst_aconstr subst bound r in
@@ -349,7 +349,7 @@ let rec subst_aconstr subst bound raw =
| ALetTuple (nal,(na,po),b,c) ->
let po' = Option.smartmap (subst_aconstr subst bound) po
- and b' = subst_aconstr subst bound b
+ and b' = subst_aconstr subst bound b
and c' = subst_aconstr subst bound c in
if po' == po && b' == b && c' == c then raw else
ALetTuple (nal,(na,po'),b',c')
@@ -357,13 +357,13 @@ let rec subst_aconstr subst bound raw =
| AIf (c,(na,po),b1,b2) ->
let po' = Option.smartmap (subst_aconstr subst bound) po
and b1' = subst_aconstr subst bound b1
- and b2' = subst_aconstr subst bound b2
+ and b2' = subst_aconstr subst bound b2
and c' = subst_aconstr subst bound c in
if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
AIf (c',(na,po'),b1',b2')
| ARec (fk,idl,dll,tl,bl) ->
- let dll' =
+ let dll' =
array_smartmap (list_smartmap (fun (na,oc,b as x) ->
let oc' = Option.smartmap (subst_aconstr subst bound) oc in
let b' = subst_aconstr subst bound b in
@@ -376,17 +376,17 @@ let rec subst_aconstr subst bound raw =
| APatVar _ | ASort _ -> raw
| AHole (Evd.ImplicitArg (ref,i,b)) ->
- let ref',t = subst_global subst ref in
+ let ref',t = subst_global subst ref in
if ref' == ref then raw else
AHole (Evd.InternalHole)
- | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType
+ | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType
| Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar
| Evd.ImpossibleCase) -> raw
- | ACast (r1,k) ->
+ | ACast (r1,k) ->
match k with
CastConv (k, r2) ->
- let r1' = subst_aconstr subst bound r1
+ let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
ACast (r1',CastConv (k,r2'))
@@ -394,7 +394,7 @@ let rec subst_aconstr subst bound raw =
let r1' = subst_aconstr subst bound r1 in
if r1' == r1 then raw else
ACast (r1',CastCoerce)
-
+
let subst_interpretation subst (metas,pat) =
let bound = List.map fst (fst metas @ snd metas) in
(metas,subst_aconstr subst bound pat)
@@ -449,7 +449,7 @@ let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
| RCoFix n1, RCoFix n2 -> n1 = n2
| RFix (nl1,n1), RFix (nl2,n2) ->
- n1 = n2 &&
+ n1 = n2 &&
array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
| _ -> false
@@ -496,7 +496,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
let l11,l12 = list_chop (n1-n2) l1 in RApp (loc,f1,l11),l12, f2,l2
else f1,l1, f2, l2 in
List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
- | RApp (loc,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
+ | RApp (loc,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
when List.length l1 >= List.length l2 ->
let f1,l1 = adjust_application_n (List.length l2) loc f1 l1 in
match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
@@ -506,20 +506,20 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
| RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
- | RCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2)
+ | RCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2)
when sty1 = sty2
& List.length tml1 = List.length tml2
& List.length eqnl1 = List.length eqnl2 ->
let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
- let sigma =
- try Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2'
- with Option.Heterogeneous -> raise No_match
+ let sigma =
+ try Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2'
+ with Option.Heterogeneous -> raise No_match
in
- let sigma = List.fold_left2
+ let sigma = List.fold_left2
(fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
- | RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2)
+ | RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2)
when List.length nal1 = List.length nal2 ->
let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
let sigma = match_ alp metas sigma b1 b2 in
@@ -529,7 +529,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
| RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2]
- | RRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2)
+ | RRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2)
when match_fix_kind fk1 fk2 & Array.length idl1 = Array.length idl2 &
array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2
->
@@ -539,7 +539,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
match_ alp metas (match_opt (match_ alp metas) sigma oc1 oc2) b1 b2
in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in
let sigma = array_fold_left2 (match_ alp metas) sigma tl1 tl2 in
- let alp,sigma = array_fold_right2 (fun id1 id2 alsig ->
+ let alp,sigma = array_fold_right2 (fun id1 id2 alsig ->
match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
array_fold_left2 (match_ alp metas) sigma bl1 bl2
| RCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) ->
@@ -549,7 +549,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
| RSort (_,s1), ASort s2 when s1 = s2 -> sigma
| RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, AHole _ -> sigma
- | (RDynamic _ | RRec _ | REvar _), _
+ | (RDynamic _ | RRec _ | REvar _), _
| _,_ -> raise No_match
and match_alist alp metas sigma l1 l2 x iter termin lassoc =
@@ -563,7 +563,7 @@ and match_alist alp metas sigma l1 l2 x iter termin lassoc =
let sigmavar = List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
(* try to find the remaining elements or the terminator *)
let rec match_alist_tail alp metas sigma acc rest =
- try
+ try
let sigmavar,sigmalist = match_ alp (ldots_var::metas) sigma rest iter in
let rest = List.assoc ldots_var sigmavar in
let t = List.assoc x sigmavar in
@@ -582,7 +582,7 @@ and match_binders alp metas na1 na2 sigma b1 b2 =
and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
(* patl1 and patl2 have the same length because they respectively
correspond to some tml1 and tml2 that have the same length *)
- let (alp,sigma) =
+ let (alp,sigma) =
List.fold_left2 (match_cases_pattern metas) (alp,sigma) patl1 patl2 in
match_ alp metas sigma rhs1 rhs2
@@ -645,7 +645,7 @@ type constr_expr =
| CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
- | CApp of loc * (proj_flag * constr_expr) *
+ | CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
| CRecord of loc * constr_expr option * (identifier located * constr_expr) list
| CCases of loc * case_style * constr_expr option *
@@ -672,7 +672,7 @@ and fixpoint_expr =
and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * binder_kind * constr_expr
-
+
and typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
@@ -680,7 +680,7 @@ and typeclass_context = typeclass_constraint list
and cofixpoint_expr =
identifier located * local_binder list * constr_expr * constr_expr
-and recursion_order_expr =
+and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
| CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
@@ -755,7 +755,7 @@ let ids_of_cases_indtype =
let rec vars_of = function
(* We deal only with the regular cases *)
| CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l)
- | CNotation (_,_,(l,[]))
+ | CNotation (_,_,(l,[]))
(* assume the ntn is applicative and does not instantiate the head !! *)
| CAppExpl (_,_,l) -> List.fold_left add_var [] l
| CDelimiters(_,_,c) -> vars_of c
@@ -772,7 +772,7 @@ let ids_of_cases_tomatch tms =
let is_constructor id =
try ignore (Nametab.locate_extended (qualid_of_ident id)); true
with Not_found -> true
-
+
let rec cases_pattern_fold_names f a = function
| CPatAlias (_,pat,id) -> f id a
| CPatCstr (_,_,patl) | CPatOr (_,patl) ->
@@ -785,7 +785,7 @@ let rec cases_pattern_fold_names f a = function
let ids_of_pattern_list =
List.fold_left
- (located_fold_left
+ (located_fold_left
(List.fold_left (cases_pattern_fold_names Idset.add)))
Idset.empty
@@ -837,12 +837,12 @@ let fold_constr_expr_with_binders g f n acc = function
| CFix (loc,_,l) ->
let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
- fold_local_binders g f n'
+ fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
- | CCoFix (loc,_,_) ->
+ | CCoFix (loc,_,_) ->
Pp.warning "Capture check in multiple binders not done"; acc
-let free_vars_of_constr_expr c =
+let free_vars_of_constr_expr c =
let rec aux bdvars l = function
| CRef (Ident (_,id)) -> if List.mem id bdvars then l else Idset.add id l
| c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
@@ -860,18 +860,18 @@ let mkProdC (idl,bk,a,b) = CProdN (dummy_loc,[idl,bk,a],b)
let rec mkCProdN loc bll c =
match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
| [] -> c
| LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
let rec mkCLambdaN loc bll c =
match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
| [] -> c
| LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
@@ -882,7 +882,7 @@ let rec abstract_constr_expr c = function
| LocalRawAssum (idl,bk,t)::bl ->
List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
(abstract_constr_expr c bl)
-
+
let rec prod_constr_expr c = function
| [] -> c
| LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
@@ -932,8 +932,8 @@ let map_local_binders f g e bl =
let map_constr_expr_with_binders g f e = function
| CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
- | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l)
- | CApp (loc,(p,a),l) ->
+ | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l)
+ | CApp (loc,(p,a),l) ->
CApp (loc,(p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
| CProdN (loc,bl,b) ->
let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b)
@@ -946,7 +946,7 @@ let map_constr_expr_with_binders g f e = function
CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll))
| CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c)
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
- | CHole _ | CEvar _ | CPatVar _ | CSort _
+ | CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CDynamic _ | CRef _ as x -> x
| CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
| CCases (loc,sty,rtnpo,a,bl) ->
@@ -963,7 +963,7 @@ let map_constr_expr_with_binders g f e = function
let e' = Option.fold_right (name_fold g) ona e in
CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (loc,id,dl) ->
- CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
+ CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
let (e',bl') = map_local_binders f g e bl in
let t' = f e' t in
(* Note: fix names should be inserted before the arguments... *)
@@ -982,22 +982,22 @@ let map_constr_expr_with_binders g f e = function
let rec replace_vars_constr_expr l = function
| CRef (Ident (loc,id)) as x ->
(try CRef (Ident (loc,List.assoc id l)) with Not_found -> x)
- | c -> map_constr_expr_with_binders List.remove_assoc
+ | c -> map_constr_expr_with_binders List.remove_assoc
replace_vars_constr_expr l c
(**********************************************************************)
(* Concrete syntax for modules and modules types *)
-type with_declaration_ast =
+type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
-type module_ast =
+type module_ast =
| CMEident of qualid located
| CMEapply of module_ast * module_ast
-type module_type_ast =
+type module_type_ast =
| CMTEident of qualid located
| CMTEapply of module_type_ast * module_ast
| CMTEwith of module_type_ast * with_declaration_ast
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 0b6cf46c5..2c28b3bea 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -39,7 +39,7 @@ type aconstr =
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
| ARec of fix_kind * identifier array *
- (name * aconstr option * aconstr) list array * aconstr array *
+ (name * aconstr option * aconstr) list array * aconstr array *
aconstr array
| ASort of rawsort
| AHole of Evd.hole_kind
@@ -48,7 +48,7 @@ type aconstr =
(**********************************************************************)
(* Translate a rawconstr into a notation given the list of variables *)
-(* bound by the notation; also interpret recursive patterns *)
+(* bound by the notation; also interpret recursive patterns *)
val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
@@ -61,7 +61,7 @@ val eq_rawconstr : rawconstr -> rawconstr -> bool
(**********************************************************************)
(* Re-interpret a notation as a rawconstr, taking care of binders *)
-val rawconstr_of_aconstr_with_binders : loc ->
+val rawconstr_of_aconstr_with_binders : loc ->
('a -> name -> 'a * name) ->
('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
@@ -97,9 +97,9 @@ val subst_interpretation : substitution -> interpretation -> interpretation
type notation = string
type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
-
-type binder_kind =
- | Default of binding_kind
+
+type binder_kind =
+ | Default of binding_kind
| Generalized of binding_kind * binding_kind * bool
(* Inner binding, outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
@@ -131,7 +131,7 @@ type constr_expr =
| CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
- | CApp of loc * (proj_flag * constr_expr) *
+ | CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
| CRecord of loc * constr_expr option * (identifier located * constr_expr) list
| CCases of loc * case_style * constr_expr option *
@@ -158,7 +158,7 @@ and fixpoint_expr =
and cofixpoint_expr =
identifier located * local_binder list * constr_expr * constr_expr
-and recursion_order_expr =
+and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
| CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
@@ -167,7 +167,7 @@ and recursion_order_expr =
and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * binder_kind * constr_expr
-
+
type typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
@@ -240,16 +240,16 @@ val map_constr_expr_with_binders :
(**********************************************************************)
(* Concrete syntax for modules and module types *)
-type with_declaration_ast =
+type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
-type module_ast =
+type module_ast =
| CMEident of qualid located
| CMEapply of module_ast * module_ast
-type module_type_ast =
+type module_type_ast =
| CMTEident of qualid located
| CMTEapply of module_type_ast * module_ast
| CMTEwith of module_type_ast * with_declaration_ast
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 17:08:48 +0000