aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml102
-rw-r--r--vernac/class.ml20
-rw-r--r--vernac/egramcoq.ml28
-rw-r--r--vernac/g_proofs.mlg12
-rw-r--r--vernac/g_vernac.mlg168
-rw-r--r--vernac/himsg.ml64
-rw-r--r--vernac/indschemes.ml72
-rw-r--r--vernac/locality.ml4
-rw-r--r--vernac/metasyntax.ml126
-rw-r--r--vernac/mltop.ml4
-rw-r--r--vernac/obligations.ml232
-rw-r--r--vernac/record.ml120
-rw-r--r--vernac/search.ml4
-rw-r--r--vernac/topfmt.ml8
-rw-r--r--vernac/vernacentries.ml82
15 files changed, 523 insertions, 523 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5822a1a586..310ea62a1d 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -205,7 +205,7 @@ let build_beq_scheme mode kn =
mkVar eid, Evd.empty_side_effects
| Cast (x,_,_) -> aux (Term.applist (x,a))
| App _ -> assert false
- | Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
+ | Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Evd.empty_side_effects
else begin
try
@@ -271,13 +271,13 @@ let build_beq_scheme mode kn =
let n = Array.length constrsi in
let ar = Array.make n (ff ()) in
let eff = ref Evd.empty_side_effects in
- for i=0 to n-1 do
- let nb_cstr_args = List.length constrsi.(i).cs_args in
+ for i=0 to n-1 do
+ let nb_cstr_args = List.length constrsi.(i).cs_args in
let ar2 = Array.make n (ff ()) in
let constrsj = constrs (3+nparrec+nb_cstr_args) in
- for j=0 to n-1 do
- if Int.equal i j then
- ar2.(j) <- let cc = (match nb_cstr_args with
+ for j=0 to n-1 do
+ if Int.equal i j then
+ ar2.(j) <- let cc = (match nb_cstr_args with
| 0 -> tt ()
| _ -> let eqs = Array.make nb_cstr_args (tt ()) in
for ndx = 0 to nb_cstr_args-1 do
@@ -299,22 +299,22 @@ let build_beq_scheme mode kn =
(eqs.(0))
(Array.sub eqs 1 (nb_cstr_args - 1))
)
- in
+ in
(List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) cc
(constrsj.(j).cs_args)
- )
- else ar2.(j) <- (List.fold_left (fun a decl ->
+ )
+ else ar2.(j) <- (List.fold_left (fun a decl ->
mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) (ff ()) (constrsj.(j).cs_args) )
done;
ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
- (mkCase (ci,do_predicate rel_list nb_cstr_args,
- mkVar (Id.of_string "Y") ,ar2))
- (constrsi.(i).cs_args))
+ (mkCase (ci,do_predicate rel_list nb_cstr_args,
+ mkVar (Id.of_string "Y") ,ar2))
+ (constrsi.(i).cs_args))
done;
mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) (
mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) (
- mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))),
+ mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))),
!eff
in (* build_beq_scheme *)
let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
@@ -333,10 +333,10 @@ let build_beq_scheme mode kn =
(Array.init nb_ind (fun i ->
let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
if not (Sorts.family_leq InSet kelim) then
- raise (NonSingletonProp (kn,i));
+ raise (NonSingletonProp (kn,i));
let fix = match mib.mind_finite with
| CoFinite ->
- raise NoDecidabilityCoInductive;
+ raise NoDecidabilityCoInductive;
| Finite ->
mkFix (((Array.make nb_ind 0),i),(names,types,cores))
| BiFinite ->
@@ -405,13 +405,13 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
Proofview.tclUNIT (mkConst c, eff)
with Not_found ->
(* spiwack: the format of this error message should probably
- be improved. *)
+ be improved. *)
let err_msg =
- (str "Leibniz->boolean:" ++
+ (str "Leibniz->boolean:" ++
str "You have to declare the" ++
- str "decidability over " ++
+ str "decidability over " ++
Printer.pr_econstr_env env sigma type_of_pq ++
- str " first.")
+ str " first.")
in
Tacticals.New.tclZEROMSG err_msg
in
@@ -470,20 +470,20 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
else (
let bl_t1, eff =
- try
+ try
let c, eff = find_scheme bl_scheme_key (fst u) (*FIXME*) in
mkConst c, eff
with Not_found ->
- (* spiwack: the format of this error message should probably
- be improved. *)
- let err_msg =
- (str "boolean->Leibniz:" ++
+ (* spiwack: the format of this error message should probably
+ be improved. *)
+ let err_msg =
+ (str "boolean->Leibniz:" ++
str "You have to declare the" ++
- str "decidability over " ++
+ str "decidability over " ++
Printer.pr_econstr_env env sigma tt1 ++
- str " first.")
- in
- user_err err_msg
+ str " first.")
+ in
+ user_err err_msg
in let bl_args =
Array.append (Array.append
v
@@ -547,8 +547,8 @@ let eqI ind l =
let list_id = list_id l in
let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@
(List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
- and e, eff =
- try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
+ and e, eff =
+ try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
(str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed.");
in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff
@@ -659,7 +659,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
then
Tacticals.New.tclTHEN
(do_replace_bl mode bl_scheme_key ind
- (!avoid)
+ (!avoid)
nparrec (ca.(2))
(ca.(1)))
Auto.default_auto
@@ -683,7 +683,7 @@ let side_effect_of_mode = function
let make_bl_scheme mode mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
- user_err
+ user_err
(str "Automatic building of boolean->Leibniz lemmas not supported");
let ind = (mind,0) in
let nparams = mib.mind_nparams in
@@ -781,7 +781,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
Tacticals.New.tclORELSE reflexivity my_discr_tac
);
my_inj_tac freshz;
- intros; simpl_in_concl;
+ intros; simpl_in_concl;
Auto.default_auto;
Tacticals.New.tclREPEAT (
Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
@@ -796,7 +796,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
| App(c',ca') ->
let n = Array.length ca' in
do_replace_lb mode lb_scheme_key
- (!avoid)
+ (!avoid)
nparrec
ca'.(n-2) ca'.(n-1)
| _ ->
@@ -813,7 +813,7 @@ let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
let make_lb_scheme mode mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
- user_err
+ user_err
(str "Automatic building of Leibniz->boolean lemmas not supported");
let ind = (mind,0) in
let nparams = mib.mind_nparams in
@@ -943,48 +943,48 @@ let compute_dec_tact ind lnamesparrec nparrec =
Proofview.tclEFFECTS eff;
intros_using fresh_first_intros;
intros_using [freshn;freshm];
- (*we do this so we don't have to prove the same goal twice *)
+ (*we do this so we don't have to prove the same goal twice *)
assert_by (Name freshH) (EConstr.of_constr (
mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
- ))
- (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
+ ))
+ (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
Proofview.Goal.enter begin fun gl ->
let freshH2 = fresh_id (Id.of_string "H") gl in
- Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
- (* left *)
- Tacticals.New.tclTHENLIST [
- simplest_left;
+ Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
+ (* left *)
+ Tacticals.New.tclTHENLIST [
+ simplest_left;
apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs)));
Auto.default_auto
]
;
- (*right *)
+ (*right *)
Proofview.Goal.enter begin fun gl ->
let freshH3 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENLIST [
- simplest_right ;
+ simplest_right ;
unfold_constr (Coqlib.lib_ref "core.not.type");
intro;
Equality.subst_all ();
assert_by (Name freshH3)
- (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])))
- (Tacticals.New.tclTHENLIST [
+ (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])))
+ (Tacticals.New.tclTHENLIST [
apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs)));
Auto.default_auto
- ]);
- Equality.general_rewrite_bindings_in true
- Locus.AllOccurrences true false
+ ]);
+ Equality.general_rewrite_bindings_in true
+ Locus.AllOccurrences true false
(List.hd !avoid)
((EConstr.mkVar (List.hd (List.tl !avoid))),
NoBindings
)
true;
my_discr_tac
- ]
+ ]
end
- ]
+ ]
end
]
end
diff --git a/vernac/class.ml b/vernac/class.ml
index 766625a21a..3c43b125d1 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -96,8 +96,8 @@ let class_of_global = function
| GlobRef.VarRef id -> CL_SECVAR id
| GlobRef.ConstructRef _ as c ->
user_err ~hdr:"class_of_global"
- (str "Constructors, such as " ++ Printer.pr_global c ++
- str ", cannot be used as a class.")
+ (str "Constructors, such as " ++ Printer.pr_global c ++
+ str ", cannot be used as a class.")
(*
lp est la liste (inverse'e) des arguments de la coercion
@@ -144,7 +144,7 @@ let get_target t ind =
| CL_CONST p when Recordops.is_primitive_projection p ->
CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
| x -> x
-
+
let strength_of_cl = function
| CL_CONST kn -> `GLOBAL
| CL_SECVAR id -> `LOCAL
@@ -188,8 +188,8 @@ let build_id_coercion idf_opt source poly =
let val_f =
it_mkLambda_or_LetIn
(mkLambda (make_annot (Name Namegen.default_dependent_ident) Sorts.Relevant,
- applistc vs (Context.Rel.to_extended_list mkRel 0 lams),
- mkRel 1))
+ applistc vs (Context.Rel.to_extended_list mkRel 0 lams),
+ mkRel 1))
lams
in
let typ_f =
@@ -201,24 +201,24 @@ let build_id_coercion idf_opt source poly =
let _ =
if not
(Reductionops.is_conv_leq env sigma
- (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f))
+ (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f))
then
user_err (strbrk
- "Cannot be defined as coercion (maybe a bad number of arguments).")
+ "Cannot be defined as coercion (maybe a bad number of arguments).")
in
let name =
match idf_opt with
| Some idf -> idf
| None ->
- let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in
- Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
+ let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in
+ Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
let univs = Evd.univ_entry ~poly sigma in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry
(definition_entry ~types:typ_f ~univs
- ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
+ ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
in
let kind = Decls.(IsDefinition IdentityCoercion) in
let kn = declare_constant ~name ~kind constr_entry in
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index c9d9b65e04..e02f94629c 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -84,7 +84,7 @@ let error_level_assoc p current expected =
| Gramlib.Gramext.LeftA -> str "left"
| Gramlib.Gramext.RightA -> str "right"
| Gramlib.Gramext.NonA -> str "non" in
- user_err
+ user_err
(str "Level " ++ int p ++ str " is already declared " ++
pr_assoc current ++ str " associative while it is now expected to be " ++
pr_assoc expected ++ str " associative.")
@@ -104,29 +104,29 @@ let find_position_gen current ensure assoc lev =
| (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
| (p,a,reinit)::l when Int.equal p n ->
if reinit then
- let a' = create_assoc assoc in
+ let a' = create_assoc assoc in
(init := Some (a',create_pos q); (p,a',false)::l)
- else if admissible_assoc (a,assoc) then
- raise Exit
+ else if admissible_assoc (a,assoc) then
+ raise Exit
else
- error_level_assoc p a (Option.get assoc)
- | l -> after := q; (n,create_assoc assoc,ensure)::l
+ error_level_assoc p a (Option.get assoc)
+ | l -> after := q; (n,create_assoc assoc,ensure)::l
in
try
- let updated = add_level None current in
- let assoc = create_assoc assoc in
+ let updated = add_level None current in
+ let assoc = create_assoc assoc in
begin match !init with
| None ->
- (* Create the entry *)
- updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
+ (* Create the entry *)
+ updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
| _ ->
- (* The reinit flag has been updated *)
+ (* The reinit flag has been updated *)
updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init)
end
with
- (* Nothing has changed *)
+ (* Nothing has changed *)
Exit ->
- (* Just inherit the existing associativity and name (None) *)
+ (* Just inherit the existing associativity and name (None) *)
current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None)
let rec list_mem_assoc_triple x = function
@@ -450,7 +450,7 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env ->
let constrlist, tail = List.chop (n - p) heads in
constrlist :: env.constrlists, tail @ constrs
in
- ty_eval rem f { env with constrs; constrlists; }
+ ty_eval rem f { env with constrs; constrlists; }
type ('s, 'a, 'r) mayrec_rule =
| MayRecRNo : ('s, Extend.norec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 5cffa18511..03dfc576a1 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -63,14 +63,14 @@ GRAMMAR EXTEND Gram
| IDENT "Abort"; IDENT "All" -> { VernacAbortAll }
| IDENT "Abort"; id = identref -> { VernacAbort (Some id) }
| IDENT "Existential"; n = natural; c = constr_body ->
- { VernacSolveExistential (n,c) }
+ { VernacSolveExistential (n,c) }
| IDENT "Admitted" -> { VernacEndProof Admitted }
| IDENT "Qed" -> { VernacEndProof (Proved (Opaque,None)) }
| IDENT "Save"; id = identref ->
- { VernacEndProof (Proved (Opaque, Some id)) }
+ { VernacEndProof (Proved (Opaque, Some id)) }
| IDENT "Defined" -> { VernacEndProof (Proved (Transparent,None)) }
| IDENT "Defined"; id=identref ->
- { VernacEndProof (Proved (Transparent,Some id)) }
+ { VernacEndProof (Proved (Transparent,Some id)) }
| IDENT "Restart" -> { VernacRestart }
| IDENT "Undo" -> { VernacUndo 1 }
| IDENT "Undo"; n = natural -> { VernacUndo n }
@@ -98,10 +98,10 @@ GRAMMAR EXTEND Gram
| IDENT "Guarded" -> { VernacCheckGuard }
(* Hints for Auto and EAuto *)
| IDENT "Create"; IDENT "HintDb" ;
- id = IDENT ; b = [ "discriminated" -> { true } | -> { false } ] ->
- { VernacCreateHintDb (id, b) }
+ id = IDENT ; b = [ "discriminated" -> { true } | -> { false } ] ->
+ { VernacCreateHintDb (id, b) }
| IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
- { VernacRemoveHints (dbnames, ids) }
+ { VernacRemoveHints (dbnames, ids) }
| IDENT "Hint"; h = hint; dbnames = opt_hintbases ->
{ VernacHints (dbnames, h) }
] ];
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 61de1bfd26..0515e88a15 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -200,9 +200,9 @@ GRAMMAR EXTEND Gram
{ (id,(bl,c)) } ] ->
{ VernacStartTheoremProof (thm, (id,(bl,c))::l) }
| stre = assumption_token; nl = inline; bl = assum_list ->
- { VernacAssumption (stre, nl, bl) }
+ { VernacAssumption (stre, nl, bl) }
| tk = assumptions_token; nl = inline; bl = assum_list ->
- { let (kwd,stre) = tk in
+ { let (kwd,stre) = tk in
test_plural_form loc kwd bl;
VernacAssumption (stre, nl, bl) }
| d = def_token; id = ident_decl; b = def_body ->
@@ -212,7 +212,7 @@ GRAMMAR EXTEND Gram
(* Gallina inductive declarations *)
| cum = OPT cumulativity_token; priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
- { let (k,f) = f in
+ { let (k,f) = f in
let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
VernacInductive (cum, priv,f,indl) }
| "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -225,7 +225,7 @@ GRAMMAR EXTEND Gram
{ VernacCoFixpoint (DoDischarge, corecs) }
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
| IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
- l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
+ l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
| IDENT "Register"; g = global; "as"; quid = qualid ->
{ VernacRegister(g, RegisterCoqlib quid) }
| IDENT "Register"; IDENT "Inline"; g = global ->
@@ -370,7 +370,7 @@ GRAMMAR EXTEND Gram
then
(* FIXME: "red" will be applied to types in bl and Cast with remain *)
let c = mkLambdaCN ~loc bl c in
- DefineBody ([], red, c, None)
+ DefineBody ([], red, c, None)
else
(match c with
| { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t)
@@ -384,7 +384,7 @@ GRAMMAR EXTEND Gram
(([],mkLambdaCN ~loc bl c), None)
else ((bl, c), Some t)
in
- DefineBody (bl, red, c, tyo) }
+ DefineBody (bl, red, c, tyo) }
| bl = binders; ":"; t = lconstr ->
{ ProveBody (bl, t) } ] ]
;
@@ -412,15 +412,15 @@ GRAMMAR EXTEND Gram
[ [ oc = opt_coercion; id = ident_decl; indpar = binders;
c = OPT [ ":"; c = lconstr -> { c } ];
lc=opt_constructors_or_fields; ntn = decl_notation ->
- { (((oc,id),indpar,c,lc),ntn) } ] ]
+ { (((oc,id),indpar,c,lc),ntn) } ] ]
;
constructor_list_or_record_decl:
[ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
| id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
- { Constructors ((c id)::l) }
+ { Constructors ((c id)::l) }
| id = identref ; c = constructor_type -> { Constructors [ c id ] }
| cstr = identref; "{"; fs = record_fields; "}" ->
- { RecordDecl (Some cstr,fs) }
+ { RecordDecl (Some cstr,fs) }
| "{";fs = record_fields; "}" -> { RecordDecl (None,fs) }
| -> { Constructors [] } ] ]
;
@@ -436,7 +436,7 @@ GRAMMAR EXTEND Gram
(* (co)-fixpoints *)
rec_definition:
[ [ id_decl = ident_decl;
- bl = binders_fixannot;
+ bl = binders_fixannot;
rtype = type_cstr;
body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation ->
{ let binders, rec_order = bl in
@@ -497,13 +497,13 @@ GRAMMAR EXTEND Gram
t = lconstr -> { fun id -> (oc,AssumExpr (id,mkProdCN ~loc l t)) }
| l = binders; oc = of_type_with_opt_coercion;
t = lconstr; ":="; b = lconstr -> { fun id ->
- (oc,DefExpr (id,mkLambdaCN ~loc l b,Some (mkProdCN ~loc l t))) }
+ (oc,DefExpr (id,mkLambdaCN ~loc l b,Some (mkProdCN ~loc l t))) }
| l = binders; ":="; b = lconstr -> { fun id ->
match b.CAst.v with
- | CCast(b', (CastConv t|CastVM t|CastNative t)) ->
- (None,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t)))
+ | CCast(b', (CastConv t|CastVM t|CastNative t)) ->
+ (None,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t)))
| _ ->
- (None,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ]
+ (None,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ]
;
record_binder:
[ [ id = name -> { (None,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
@@ -523,10 +523,10 @@ GRAMMAR EXTEND Gram
constructor_type:
[[ l = binders;
t= [ coe = of_type_with_opt_coercion; c = lconstr ->
- { fun l id -> (not (Option.is_empty coe),(id,mkProdCN ~loc l c)) }
+ { fun l id -> (not (Option.is_empty coe),(id,mkProdCN ~loc l c)) }
| ->
{ fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
- -> { t l }
+ -> { t l }
]]
;
@@ -535,11 +535,11 @@ GRAMMAR EXTEND Gram
;
of_type_with_opt_coercion:
[ [ ":>>" -> { Some false }
- | ":>"; ">" -> { Some false }
- | ":>" -> { Some true }
- | ":"; ">"; ">" -> { Some false }
- | ":"; ">" -> { Some true }
- | ":" -> { None } ] ]
+ | ":>"; ">" -> { Some false }
+ | ":>" -> { Some true }
+ | ":"; ">"; ">" -> { Some false }
+ | ":"; ">" -> { Some true }
+ | ":" -> { None } ] ]
;
END
@@ -573,16 +573,16 @@ GRAMMAR EXTEND Gram
gallina_ext:
[ [ (* Interactive module declaration *)
IDENT "Module"; export = export_token; id = identref;
- bl = LIST0 module_binder; sign = of_module_type;
- body = is_module_expr ->
- { VernacDefineModule (export, id, bl, sign, body) }
+ bl = LIST0 module_binder; sign = of_module_type;
+ body = is_module_expr ->
+ { VernacDefineModule (export, id, bl, sign, body) }
| IDENT "Module"; "Type"; id = identref;
- bl = LIST0 module_binder; sign = check_module_types;
- body = is_module_type ->
- { VernacDeclareModuleType (id, bl, sign, body) }
+ bl = LIST0 module_binder; sign = check_module_types;
+ body = is_module_type ->
+ { VernacDeclareModuleType (id, bl, sign, body) }
| IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
- bl = LIST0 module_binder; ":"; mty = module_type_inl ->
- { VernacDeclareModule (export, id, bl, mty) }
+ bl = LIST0 module_binder; ":"; mty = module_type_inl ->
+ { VernacDeclareModule (export, id, bl, mty) }
(* Section beginning *)
| IDENT "Section"; id = identref -> { VernacBeginSection id }
| IDENT "Chapter"; id = identref -> { VernacBeginSection id }
@@ -598,14 +598,14 @@ GRAMMAR EXTEND Gram
| IDENT "Require"; export = export_token; qidl = LIST1 global ->
{ VernacRequire (None, export, qidl) }
| IDENT "From" ; ns = global ; IDENT "Require"; export = export_token
- ; qidl = LIST1 global ->
- { VernacRequire (Some ns, export, qidl) }
+ ; qidl = LIST1 global ->
+ { VernacRequire (Some ns, export, qidl) }
| IDENT "Import"; qidl = LIST1 global -> { VernacImport (false,qidl) }
| IDENT "Export"; qidl = LIST1 global -> { VernacImport (true,qidl) }
| IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
- { VernacInclude(e::l) }
+ { VernacInclude(e::l) }
| IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
- { warn_deprecated_include_type ~loc ();
+ { warn_deprecated_include_type ~loc ();
VernacInclude(e::l) } ] ]
;
export_token:
@@ -670,7 +670,7 @@ GRAMMAR EXTEND Gram
[ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
{ CWith_Definition (fqid,udecl,c) }
| IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
- { CWith_Module (fqid,qid) }
+ { CWith_Module (fqid,qid) }
] ]
;
module_type:
@@ -695,7 +695,7 @@ GRAMMAR EXTEND Gram
| "Type"; "*" -> { SsFwdClose SsType } ]]
;
ssexpr:
- [ "35"
+ [ "35"
[ "-"; e = ssexpr -> { SsCompl e } ]
| "50"
[ e1 = ssexpr; "-"; e2 = ssexpr-> { SsSubstr(e1,e2) }
@@ -754,25 +754,25 @@ GRAMMAR EXTEND Gram
| IDENT "Instance"; namesup = instance_name; ":";
t = operconstr LEVEL "200";
- info = hint_info ;
- props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
- ":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
+ info = hint_info ;
+ props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
+ ":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
{ VernacInstance (fst namesup,snd namesup,t,props,info) }
| IDENT "Existing"; IDENT "Instance"; id = global;
info = hint_info ->
- { VernacExistingInstance [id, info] }
+ { VernacExistingInstance [id, info] }
| IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
pri = OPT [ "|"; i = natural -> { i } ] ->
{ let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in
let insts = List.map (fun i -> (i, info)) ids in
- VernacExistingInstance insts }
+ VernacExistingInstance insts }
| IDENT "Existing"; IDENT "Class"; is = global -> { VernacExistingClass is }
(* Arguments *)
- | IDENT "Arguments"; qid = smart_global;
+ | IDENT "Arguments"; qid = smart_global;
args = LIST0 argument_spec_block;
more_implicits = OPT
[ ","; impl = LIST1
@@ -802,18 +802,18 @@ GRAMMAR EXTEND Gram
VernacArguments (qid, args, more_implicits, !slash_position, !ampersand_position, mods) }
| IDENT "Implicit"; "Type"; bl = reserv_list ->
- { VernacReserve bl }
+ { VernacReserve bl }
| IDENT "Implicit"; IDENT "Types"; bl = reserv_list ->
{ test_plural_form_types loc "Implicit Types" bl;
VernacReserve bl }
- | IDENT "Generalizable";
- gen = [IDENT "All"; IDENT "Variables" -> { Some [] }
- | IDENT "No"; IDENT "Variables" -> { None }
- | ["Variable" -> { () } | IDENT "Variables" -> { () } ];
- idl = LIST1 identref -> { Some idl } ] ->
- { VernacGeneralizable gen } ] ]
+ | IDENT "Generalizable";
+ gen = [IDENT "All"; IDENT "Variables" -> { Some [] }
+ | IDENT "No"; IDENT "Variables" -> { None }
+ | ["Variable" -> { () } | IDENT "Variables" -> { () } ];
+ idl = LIST1 identref -> { Some idl } ] ->
+ { VernacGeneralizable gen } ] ]
;
arguments_modifier:
[ [ IDENT "simpl"; IDENT "nomatch" -> { [`ReductionDontExposeCase] }
@@ -927,7 +927,7 @@ GRAMMAR EXTEND Gram
(* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
| IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
t = operconstr LEVEL "200";
- info = hint_info ->
+ info = hint_info ->
{ VernacDeclareInstance (id, bl, t, info) }
(* Should be in syntax, but camlp5 would not factorize *)
@@ -940,28 +940,28 @@ GRAMMAR EXTEND Gram
| IDENT "Cd"; dir = ne_string -> { VernacChdir (Some dir) }
| IDENT "Load"; verbosely = [ IDENT "Verbose" -> { true } | -> { false } ];
- s = [ s = ne_string -> { s } | s = IDENT -> { s } ] ->
- { VernacLoad (verbosely, s) }
+ s = [ s = ne_string -> { s } | s = IDENT -> { s } ] ->
+ { VernacLoad (verbosely, s) }
| IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
- { VernacDeclareMLModule l }
+ { VernacDeclareMLModule l }
| IDENT "Locate"; l = locatable -> { VernacLocate l }
(* Managing load paths *)
| IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath ->
- { VernacAddLoadPath (false, dir, alias) }
+ { VernacAddLoadPath (false, dir, alias) }
| IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string;
- alias = as_dirpath -> { VernacAddLoadPath (true, dir, alias) }
+ alias = as_dirpath -> { VernacAddLoadPath (true, dir, alias) }
| IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
- { VernacRemoveLoadPath dir }
+ { VernacRemoveLoadPath dir }
(* For compatibility *)
| IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath ->
- { VernacAddLoadPath (false, dir, alias) }
+ { VernacAddLoadPath (false, dir, alias) }
| IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath ->
- { VernacAddLoadPath (true, dir, alias) }
+ { VernacAddLoadPath (true, dir, alias) }
| IDENT "DelPath"; dir = ne_string ->
- { VernacRemoveLoadPath dir }
+ { VernacRemoveLoadPath dir }
(* Type-Checking (pas dans le refman) *)
| "Type"; c = lconstr -> { VernacGlobalCheck c }
@@ -970,17 +970,17 @@ GRAMMAR EXTEND Gram
| IDENT "Print"; p = printable -> { VernacPrint p }
| IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> { VernacPrint (PrintName (qid,l)) }
| IDENT "Print"; IDENT "Module"; "Type"; qid = global ->
- { VernacPrint (PrintModuleType qid) }
+ { VernacPrint (PrintModuleType qid) }
| IDENT "Print"; IDENT "Module"; qid = global ->
- { VernacPrint (PrintModule qid) }
+ { VernacPrint (PrintModule qid) }
| IDENT "Print"; IDENT "Namespace" ; ns = dirpath ->
{ VernacPrint (PrintNamespace ns) }
| IDENT "Inspect"; n = natural -> { VernacPrint (PrintInspect n) }
| IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
- { VernacAddMLPath (false, dir) }
- | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
- { VernacAddMLPath (true, dir) }
+ { VernacAddMLPath (false, dir) }
+ | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
+ { VernacAddMLPath (true, dir) }
(* For acting on parameter tables *)
| "Set"; table = option_table; v = option_setting ->
@@ -989,7 +989,7 @@ GRAMMAR EXTEND Gram
{ VernacSetOption (false, table, OptionUnset) }
| IDENT "Print"; IDENT "Table"; table = option_table ->
- { VernacPrintOption table }
+ { VernacPrintOption table }
| IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
-> { VernacAddOption ([table;field], v) }
@@ -1008,32 +1008,32 @@ GRAMMAR EXTEND Gram
| IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
-> { VernacRemoveOption ([table;field], v) }
| IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
- { VernacRemoveOption ([table], v) } ]]
+ { VernacRemoveOption ([table], v) } ]]
;
query_command: (* TODO: rapprocher Eval et Check *)
[ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." ->
{ fun g -> VernacCheckMayEval (Some r, g, c) }
| IDENT "Compute"; c = lconstr; "." ->
- { fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) }
+ { fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) }
| IDENT "Check"; c = lconstr; "." ->
- { fun g -> VernacCheckMayEval (None, g, c) }
+ { fun g -> VernacCheckMayEval (None, g, c) }
(* Searching the environment *)
| IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." ->
{ fun g -> VernacPrint (PrintAbout (qid,l,g)) }
| IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." ->
- { fun g -> VernacSearch (SearchHead c,g, l) }
+ { fun g -> VernacSearch (SearchHead c,g, l) }
| IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
- { fun g -> VernacSearch (SearchPattern c,g, l) }
+ { fun g -> VernacSearch (SearchPattern c,g, l) }
| IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
- { fun g -> VernacSearch (SearchRewrite c,g, l) }
+ { fun g -> VernacSearch (SearchRewrite c,g, l) }
| IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." ->
- { let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) }
+ { let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) }
(* compatibility: SearchAbout *)
| IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." ->
- { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) }
+ { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) }
(* compatibility: SearchAbout with "[ ... ]" *)
| IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]";
- l = in_or_out_modules; "." ->
+ l = in_or_out_modules; "." ->
{ fun g -> VernacSearch (SearchAbout sl,g, l) }
] ]
;
@@ -1043,7 +1043,7 @@ GRAMMAR EXTEND Gram
| IDENT "Section"; s = global -> { PrintSectionContext s }
| IDENT "Grammar"; ent = IDENT ->
(* This should be in "syntax" section but is here for factorization*)
- { PrintGrammar ent }
+ { PrintGrammar ent }
| IDENT "Custom"; IDENT "Grammar"; ent = IDENT ->
(* Should also be in "syntax" section *)
{ PrintCustomGrammar ent }
@@ -1179,7 +1179,7 @@ GRAMMAR EXTEND Gram
| IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":=";
r = red_expr ->
- { VernacDeclareReduction (s,r) }
+ { VernacDeclareReduction (s,r) }
(* factorized here, though relevant for syntax extensions *)
@@ -1202,37 +1202,37 @@ GRAMMAR EXTEND Gram
{ VernacOpenCloseScope (false,sc) }
| IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
- { VernacDelimiters (sc, Some key) }
+ { VernacDelimiters (sc, Some key) }
| IDENT "Undelimit"; IDENT "Scope"; sc = IDENT ->
- { VernacDelimiters (sc, None) }
+ { VernacDelimiters (sc, None) }
| IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
refl = LIST1 class_rawexpr -> { VernacBindScope (sc,refl) }
| IDENT "Infix"; op = ne_lstring; ":="; p = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ];
- sc = OPT [ ":"; sc = IDENT -> { sc } ] ->
+ sc = OPT [ ":"; sc = IDENT -> { sc } ] ->
{ VernacInfix ((op,modl),p,sc) }
| IDENT "Notation"; id = identref;
- idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
+ idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
{ VernacSyntacticDefinition
(id,(idl,c),b) }
| IDENT "Notation"; s = lstring; ":=";
- c = constr;
+ c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ];
- sc = OPT [ ":"; sc = IDENT -> { sc } ] ->
+ sc = OPT [ ":"; sc = IDENT -> { sc } ] ->
{ VernacNotation (c,(s,modl),sc) }
| IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
{ VernacNotationAddFormat (n,s,fmt) }
| IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
- l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] ->
+ l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] ->
{ let s = CAst.map (fun s -> "x '"^s^"' y") s in
VernacSyntaxExtension (true,(s,l)) }
| IDENT "Reserved"; IDENT "Notation";
- s = ne_lstring;
- l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]
+ s = ne_lstring;
+ l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]
-> { VernacSyntaxExtension (false, (s,l)) }
(* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index c335d3ad55..2e58bf4a93 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -223,21 +223,21 @@ let explain_elim_arity env sigma ind c pj okinds =
let pki = Sorts.pr_sort_family ki in
let pkp = Sorts.pr_sort_family kp in
let explanation = match explanation with
- | NonInformativeToInformative ->
+ | NonInformativeToInformative ->
"proofs can be eliminated only to build proofs"
- | StrongEliminationOnNonSmallType ->
+ | StrongEliminationOnNonSmallType ->
"strong elimination on non-small inductive types leads to paradoxes"
- | WrongArity ->
- "wrong arity" in
+ | WrongArity ->
+ "wrong arity" in
let ppar = pr_disjunction (fun s -> quote (Sorts.pr_sort_family s)) sorts in
let ppt = pr_leconstr_env env sigma (snd (decompose_prod_assum sigma pj.uj_type)) in
hov 0
- (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
- str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++
+ (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
+ str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++
fnl () ++
hov 0
- (str "Elimination of an inductive object of sort " ++
- pki ++ brk(1,0) ++
+ (str "Elimination of an inductive object of sort " ++
+ pki ++ brk(1,0) ++
str "is not allowed on a predicate in sort " ++ pkp ++ fnl () ++
str "because" ++ spc () ++ str explanation ++ str ".")
| None ->
@@ -254,11 +254,11 @@ let explain_case_not_inductive env sigma cj =
let pct = pr_leconstr_env env sigma cj.uj_type in
match EConstr.kind sigma cj.uj_type with
| Evar _ ->
- str "Cannot infer a type for this expression."
+ str "Cannot infer a type for this expression."
| _ ->
- str "The term" ++ brk(1,1) ++ pc ++ spc () ++
- str "has type" ++ brk(1,1) ++ pct ++ spc () ++
- str "which is not a (co-)inductive type."
+ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
+ str "has type" ++ brk(1,1) ++ pct ++ spc () ++
+ str "which is not a (co-)inductive type."
let explain_number_branches env sigma cj expn =
let env = make_all_name_different env sigma in
@@ -294,12 +294,12 @@ let explain_unification_error env sigma p1 p2 = function
let rec aux p1 p2 = function
| OccurCheck (evk,rhs) ->
[str "cannot define " ++ quote (pr_existential_key sigma evk) ++
- strbrk " with term " ++ pr_leconstr_env env sigma rhs ++
+ strbrk " with term " ++ pr_leconstr_env env sigma rhs ++
strbrk " that would depend on itself"]
| NotClean ((evk,args),env,c) ->
[str "cannot instantiate " ++ quote (pr_existential_key sigma evk)
++ strbrk " because " ++ pr_leconstr_env env sigma c ++
- strbrk " is not in its scope" ++
+ strbrk " is not in its scope" ++
(if Array.is_empty args then mt() else
strbrk ": available arguments are " ++
pr_sequence (pr_leconstr_env env sigma) (List.rev (Array.to_list args)))]
@@ -316,7 +316,7 @@ let explain_unification_error env sigma p1 p2 = function
else []
| MetaOccurInBody evk ->
[str "instance for " ++ quote (pr_existential_key sigma evk) ++
- strbrk " refers to a metavariable - please report your example" ++
+ strbrk " refers to a metavariable - please report your example" ++
strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."]
| InstanceNotSameType (evk,env,t,u) ->
let t, u = pr_explicit env sigma t u in
@@ -326,9 +326,9 @@ let explain_unification_error env sigma p1 p2 = function
t ++ strbrk " is a subtype of " ++ u]
| UnifUnivInconsistency p ->
if !Constrextern.print_universes then
- [str "universe inconsistency: " ++
+ [str "universe inconsistency: " ++
Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p]
- else
+ else
[str "universe inconsistency"]
| CannotSolveConstraint ((pb,env,t,u),e) ->
let env = make_all_name_different env sigma in
@@ -386,9 +386,9 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
if nargs>1 then str "The " ++ pr_nth n ++ str " term" else str "This term"
in
let appl = prvect_with_sep fnl
- (fun c ->
- let pc,pct = pr_ljudge_env env sigma c in
- hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
+ (fun c ->
+ let pc,pct = pr_ljudge_env env sigma c in
+ hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
in
str "Illegal application: " ++ (* pe ++ *) fnl () ++
str "The term" ++ brk(1,1) ++ pr ++ spc () ++
@@ -406,10 +406,10 @@ let explain_cant_apply_not_functional env sigma rator randl =
let pr = pr_leconstr_env env sigma rator.uj_val in
let prt = pr_leconstr_env env sigma rator.uj_type in
let appl = prvect_with_sep fnl
- (fun c ->
- let pc = pr_leconstr_env env sigma c.uj_val in
- let pct = pr_leconstr_env env sigma c.uj_type in
- hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
+ (fun c ->
+ let pc = pr_leconstr_env env sigma c.uj_val in
+ let pct = pr_leconstr_env env sigma c.uj_type in
+ hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
in
str "Illegal application (Non-functional construction): " ++
(* pe ++ *) fnl () ++
@@ -517,7 +517,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
(try (* May fail with unresolved globals. *)
let fixenv = make_all_name_different fixenv sigma in
let pvd = pr_lconstr_env fixenv sigma vdefj.(i).uj_val in
- str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
+ str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
with e when CErrors.noncritical e -> mt ())
let explain_ill_typed_rec_body env sigma i names vdefj vargs =
@@ -723,8 +723,8 @@ let explain_non_linear_unification env sigma m t =
pr_lconstr_env env sigma t ++ str "."
let explain_unsatisfied_constraints env sigma cst =
- strbrk "Unsatisfied constraints: " ++
- Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++
+ strbrk "Unsatisfied constraints: " ++
+ Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++
spc () ++ str "(maybe a bugged tactic)."
let explain_undeclared_universe env sigma l =
@@ -841,7 +841,7 @@ let explain_unsatisfiable_constraints env sigma constr comp =
| None -> Evar.Set.mem evk tcs
| Some comp -> Evar.Set.mem evk tcs && Evar.Set.mem evk comp
in
- let undef =
+ let undef =
let m = Evar.Map.filter is_kept undef in
if Evar.Map.is_empty m then undef
else m
@@ -942,12 +942,12 @@ let explain_not_match_error = function
str "Aliases to inductive types do not match"
| CumulativeStatusExpected b ->
let status b = if b then str"cumulative" else str"non-cumulative" in
- str "a " ++ status b ++ str" declaration was expected, but a " ++
- status (not b) ++ str" declaration was found"
+ str "a " ++ status b ++ str" declaration was expected, but a " ++
+ status (not b) ++ str" declaration was found"
| PolymorphicStatusExpected b ->
let status b = if b then str"polymorphic" else str"monomorphic" in
- str "a " ++ status b ++ str" declaration was expected, but a " ++
- status (not b) ++ str" declaration was found"
+ str "a " ++ status b ++ str" declaration was expected, but a " ++
+ status (not b) ++ str" declaration was found"
| IncompatibleUniverses incon ->
str"the universe constraints are inconsistent: " ++
Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index a6c577a878..b2e1a5e796 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -118,7 +118,7 @@ let alarm what internal msg =
| InternalTacticRequest ->
(if debug then
Feedback.msg_debug
- (hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
+ (hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
| _ -> Some msg
let try_declare_scheme what f internal names kn =
@@ -128,27 +128,27 @@ let try_declare_scheme what f internal names kn =
let rec extract_exn = function Logic_monad.TacticFailure e -> extract_exn e | e -> e in
let msg = match extract_exn (fst e) with
| ParameterWithoutEquality cst ->
- alarm what internal
- (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++
- str".")
+ alarm what internal
+ (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++
+ str".")
| InductiveWithProduct ->
- alarm what internal
- (str "Unable to decide equality of functional arguments.")
+ alarm what internal
+ (str "Unable to decide equality of functional arguments.")
| InductiveWithSort ->
- alarm what internal
- (str "Unable to decide equality of type arguments.")
+ alarm what internal
+ (str "Unable to decide equality of type arguments.")
| NonSingletonProp ind ->
- alarm what internal
- (str "Cannot extract computational content from proposition " ++
- quote (Printer.pr_inductive (Global.env()) ind) ++ str ".")
+ alarm what internal
+ (str "Cannot extract computational content from proposition " ++
+ quote (Printer.pr_inductive (Global.env()) ind) ++ str ".")
| EqNotFound (ind',ind) ->
- alarm what internal
- (str "Boolean equality on " ++
- quote (Printer.pr_inductive (Global.env()) ind') ++
- strbrk " is missing.")
+ alarm what internal
+ (str "Boolean equality on " ++
+ quote (Printer.pr_inductive (Global.env()) ind') ++
+ strbrk " is missing.")
| UndefinedCst s ->
- alarm what internal
- (strbrk "Required constant " ++ str s ++ str " undefined.")
+ alarm what internal
+ (strbrk "Required constant " ++ str s ++ str " undefined.")
| AlreadyDeclared (kind, id) as exn ->
let msg = CErrors.print exn in
alarm what internal msg
@@ -171,7 +171,7 @@ let try_declare_scheme what f internal names kn =
str " is applied to an argument which is not a variable.")
| e when CErrors.noncritical e ->
alarm what internal
- (str "Unexpected error during scheme creation: " ++ CErrors.print e)
+ (str "Unexpected error during scheme creation: " ++ CErrors.print e)
| _ -> iraise e
in
match msg with
@@ -370,10 +370,10 @@ requested
let newref = CAst.make newid in
((newref,isdep,ind,z)::l1),l2
in
- match t with
- | CaseScheme (x,y,z) -> names "_case" "_case" x y z
- | InductionScheme (x,y,z) -> names "_ind" "_rec" x y z
- | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2)
+ match t with
+ | CaseScheme (x,y,z) -> names "_case" "_case" x y z
+ | InductionScheme (x,y,z) -> names "_ind" "_rec" x y z
+ | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2)
let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) lnamedepindsort
@@ -382,13 +382,13 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
List.fold_right
(fun (_,dep,ind,sort) (evd, l, inst) ->
let evd, indu, inst =
- match inst with
- | None ->
+ match inst with
+ | None ->
let _, ctx = Typeops.type_of_global_in_context env0 (GlobRef.IndRef ind) in
let u, ctx = UnivGen.fresh_instance_from ctx None in
let evd = Evd.from_ctx (UState.of_context_set ctx) in
- evd, (ind,u), Some u
- | Some ui -> evd, (ind, ui), inst
+ evd, (ind,u), Some u
+ | Some ui -> evd, (ind, ui), inst
in
(evd, (indu,dep,sort) :: l, inst))
lnamedepindsort (Evd.from_env env0,[],None)
@@ -416,10 +416,10 @@ let get_common_underlying_mutual_inductive env = function
| (_,ind')::_ ->
raise (RecursionSchemeError (env, NotMutualInScheme (ind,ind')))
| [] ->
- if not (List.distinct_f Int.compare (List.map snd (List.map snd all)))
+ if not (List.distinct_f Int.compare (List.map snd (List.map snd all)))
then user_err Pp.(str "A type occurs twice");
- mind,
- List.map_filter
+ mind,
+ List.map_filter
(function (Some id,(_,i)) -> Some (i,id.CAst.v) | (None,_) -> None) all
let do_scheme l =
@@ -434,8 +434,8 @@ tried to declare different schemes at once *)
if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme
else
let mind,l = get_common_underlying_mutual_inductive env escheme in
- declare_beq_scheme_with l mind;
- declare_eq_decidability_scheme_with l mind
+ declare_beq_scheme_with l mind;
+ declare_eq_decidability_scheme_with l mind
)
(**********************************************************************)
@@ -468,11 +468,11 @@ let build_combined_scheme env schemes =
let (ctx, arity) = decompose_prod ty in
let (_, last) = List.hd ctx in
match Constr.kind last with
- | App (ind, args) ->
- let ind = destInd ind in
- let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in
- ctx, ind, spec.mind_nrealargs
- | _ -> ctx, destInd last, 0
+ | App (ind, args) ->
+ let ind = destInd ind in
+ let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in
+ ctx, ind, spec.mind_nrealargs
+ | _ -> ctx, destInd last, 0
in
let (c, t) = List.hd defs in
let ctx, ind, nargs = find_inductive t in
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 5862f51b43..c31f722a61 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -69,8 +69,8 @@ let enforce_section_locality locality_flag =
let make_module_locality = function
| Some false ->
if Global.sections_are_opened () then
- CErrors.user_err Pp.(str
- "This command does not support the Global option in sections.");
+ CErrors.user_err Pp.(str
+ "This command does not support the Global option in sections.");
false
| Some true -> true
| None -> false
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e754ead5dd..fd57901acd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -131,37 +131,37 @@ let parse_format ({CAst.loc;v=str} : lstring) =
(* Parse " // " *)
| '/' when i+1 < len && str.[i+1] == '/' ->
(* We discard the useless n spaces... *)
- push_token (make_loc (i-n) (i+1)) (UnpCut PpFnl)
+ push_token (make_loc (i-n) (i+1)) (UnpCut PpFnl)
(parse_token 1 (close_quotation i (i+2)))
(* Parse " .. / .. " *)
| '/' when i+1 < len ->
- let p = spaces 0 (i+1) in
- push_token (make_loc (i-n) (i+p)) (UnpCut (PpBrk (n,p)))
+ let p = spaces 0 (i+1) in
+ push_token (make_loc (i-n) (i+p)) (UnpCut (PpBrk (n,p)))
(parse_token 1 (close_quotation i (i+p+1)))
| c ->
(* The spaces are real spaces *)
push_white i n (match c with
| '[' ->
- if i+1 < len then match str.[i+1] with
- (* Parse " [h .. ", *)
- | 'h' when i+1 <= len && str.[i+2] == 'v' ->
- (parse_box i (fun n -> PpHVB n) (i+3))
- (* Parse " [v .. ", *)
- | 'v' ->
- parse_box i (fun n -> PpVB n) (i+2)
- (* Parse " [ .. ", *)
- | ' ' | '\'' ->
- parse_box i (fun n -> PpHOVB n) (i+1)
- | _ -> user_err ?loc:(make_loc i i) Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.")
- else user_err ?loc:(make_loc i i) Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.")
+ if i+1 < len then match str.[i+1] with
+ (* Parse " [h .. ", *)
+ | 'h' when i+1 <= len && str.[i+2] == 'v' ->
+ (parse_box i (fun n -> PpHVB n) (i+3))
+ (* Parse " [v .. ", *)
+ | 'v' ->
+ parse_box i (fun n -> PpVB n) (i+2)
+ (* Parse " [ .. ", *)
+ | ' ' | '\'' ->
+ parse_box i (fun n -> PpHOVB n) (i+1)
+ | _ -> user_err ?loc:(make_loc i i) Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.")
+ else user_err ?loc:(make_loc i i) Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.")
(* Parse "]" *)
| ']' ->
- ((i,[]) :: parse_token 1 (close_quotation i (i+1)))
+ ((i,[]) :: parse_token 1 (close_quotation i (i+1)))
(* Parse a non formatting token *)
| c ->
- let n = nonspaces true 0 i in
- push_token (make_loc i (i+n-1)) (UnpTerminal (String.sub str (i-1) (n+2)))
- (parse_token 1 (close_quotation i (i+n))))
+ let n = nonspaces true 0 i in
+ push_token (make_loc i (i+n-1)) (UnpTerminal (String.sub str (i-1) (n+2)))
+ (parse_token 1 (close_quotation i (i+n))))
else
if Int.equal n 0 then []
else user_err ?loc:(make_loc (len-n) len) Pp.(str "Ending spaces non part of a format annotation.")
@@ -174,7 +174,7 @@ let parse_format ({CAst.loc;v=str} : lstring) =
if i < len then match str.[i] with
(* Parse a ' *)
| '\'' when i+1 >= len || str.[i+1] == ' ' ->
- push_white (i-n) (n-k) (push_token (make_loc i (i+1)) (UnpTerminal "'") (parse_token 1 (i+1)))
+ push_white (i-n) (n-k) (push_token (make_loc i (i+1)) (UnpTerminal "'") (parse_token 1 (i+1)))
(* Parse the beginning of a quoted expression *)
| '\'' ->
parse_quoted (n-k) (i+1)
@@ -261,11 +261,11 @@ let rec get_notation_vars onlyprint = function
| NonTerminal id :: sl ->
let vars = get_notation_vars onlyprint sl in
if Id.equal id ldots_var then vars else
- (* don't check for nonlinearity if printing only, see Bug 5526 *)
- if not onlyprint && Id.List.mem id vars then
- user_err ~hdr:"Metasyntax.get_notation_vars"
+ (* don't check for nonlinearity if printing only, see Bug 5526 *)
+ if not onlyprint && Id.List.mem id vars then
+ user_err ~hdr:"Metasyntax.get_notation_vars"
(str "Variable " ++ Id.print id ++ str " occurs more than once.")
- else id::vars
+ else id::vars
| (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
| SProdList _ :: _ -> assert false
@@ -393,23 +393,23 @@ let make_hunks etyps symbols from =
let vars,typs = List.split etyps in
let rec make b = function
| NonTerminal m :: prods ->
- let i = index_id m vars in
+ let i = index_id m vars in
let u = unparsing_metavar i from typs in
if is_next_non_terminal b prods then
(None, u) :: add_break_if_none 1 b (make b prods)
- else
+ else
(None, u) :: make_with_space b prods
| Terminal s :: prods
when (* true to simulate presence of non-terminal *) b || List.exists is_non_terminal prods ->
if (is_comma s || is_operator s) then
(* Always a breakable space after comma or separator *)
(None, UnpTerminal s) :: add_break_if_none 1 b (make b prods)
- else if is_right_bracket s && is_next_terminal prods then
+ else if is_right_bracket s && is_next_terminal prods then
(* Always no space after right bracked, but possibly a break *)
(None, UnpTerminal s) :: add_break_if_none 0 b (make b prods)
else if is_left_bracket s && is_next_non_terminal b prods then
(None, UnpTerminal s) :: make b prods
- else if not (is_next_break prods) then
+ else if not (is_next_break prods) then
(* Add rigid space, no break, unless user asked for something *)
(None, UnpTerminal (s^" ")) :: make b prods
else
@@ -426,20 +426,20 @@ let make_hunks etyps symbols from =
add_break n (make b prods)
| SProdList (m,sl) :: prods ->
- let i = index_id m vars in
- let typ = List.nth typs (i-1) in
- let _,prec = precedence_of_entry_type from typ in
+ let i = index_id m vars in
+ let typ = List.nth typs (i-1) in
+ let _,prec = precedence_of_entry_type from typ in
let sl' =
(* If no separator: add a break *)
- if List.is_empty sl then add_break 1 []
+ if List.is_empty sl then add_break 1 []
(* We add NonTerminal for simulation but remove it afterwards *)
else make true sl in
- let hunk = match typ with
- | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl')
- | ETBinder isopen ->
- check_open_binder isopen sl m;
- UnpBinderListMetaVar (i,isopen,List.map snd sl')
- | _ -> assert false in
+ let hunk = match typ with
+ | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl')
+ | ETBinder isopen ->
+ check_open_binder isopen sl m;
+ UnpBinderListMetaVar (i,isopen,List.map snd sl')
+ | _ -> assert false in
(None, hunk) :: make_with_space b prods
| [] -> []
@@ -552,11 +552,11 @@ let hunks_of_format (from,(vars,typs)) symfmt =
if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) ();
let symbs, l = aux (symbs,rfmt) in
let hunk = match typ with
- | ETConstr _ -> UnpListMetaVar (i,prec,slfmt)
- | ETBinder isopen ->
- check_open_binder isopen sl m;
- UnpBinderListMetaVar (i,isopen,slfmt)
- | _ -> assert false in
+ | ETConstr _ -> UnpListMetaVar (i,prec,slfmt)
+ | ETBinder isopen ->
+ check_open_binder isopen sl m;
+ UnpBinderListMetaVar (i,isopen,slfmt)
+ | _ -> assert false in
symbs, hunk :: l
| symbs, [] -> symbs, []
| Break _ :: symbs, fmt -> warn_format_break (); aux (symbs,fmt)
@@ -656,7 +656,7 @@ let make_production etyps symbols =
(List.map (function Terminal s -> [CLexer.terminal s]
| Break _ -> []
| _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
- match List.assoc x etyps with
+ match List.assoc x etyps with
| ETConstr (s,_,typ) ->
let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in
expand_list_rule s typ tkl x 1 p (aux l')
@@ -712,7 +712,7 @@ let pr_level ntn (from,fromlevel,args,typs) =
prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
let error_incompatible_level ntn oldprec prec =
- user_err
+ user_err
(str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
@@ -829,17 +829,17 @@ let interp_modifiers modl = let open NotationMods in
let rec interp subtyps acc = function
| [] -> subtyps, acc
| SetEntryType (s,typ) :: l ->
- let id = Id.of_string s in
- if Id.List.mem_assoc id acc.etyps then
- user_err ~hdr:"Metasyntax.interp_modifiers"
+ let id = Id.of_string s in
+ if Id.List.mem_assoc id acc.etyps then
+ user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
interp subtyps { acc with etyps = (id,typ) :: acc.etyps; } l
| SetItemLevel ([],bko,n) :: l ->
interp subtyps acc l
| SetItemLevel (s::idl,bko,n) :: l ->
- let id = Id.of_string s in
- if Id.List.mem_assoc id acc.etyps then
- user_err ~hdr:"Metasyntax.interp_modifiers"
+ let id = Id.of_string s in
+ if Id.List.mem_assoc id acc.etyps then
+ user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
interp ((id,bko,n)::subtyps) acc (SetItemLevel (idl,bko,n)::l)
| SetLevel n :: l ->
@@ -871,7 +871,7 @@ let interp_modifiers modl = let open NotationMods in
user_err (str "Entry is already assigned to custom " ++ str s ++ (match acc.level with None -> mt () | Some lev -> str " at level " ++ int lev) ++ str ".");
interp subtyps { acc with custom = InCustomEntry s; level = n } l
| SetAssoc a :: l ->
- if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
+ if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
interp subtyps { acc with assoc = Some a; } l
| SetOnlyParsing :: l ->
interp subtyps { acc with only_parsing = true; } l
@@ -880,7 +880,7 @@ let interp_modifiers modl = let open NotationMods in
| SetCompatVersion v :: l ->
interp subtyps { acc with compat = Some v; } l
| SetFormat ("text",s) :: l ->
- if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
+ if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
interp subtyps { acc with format = Some s; } l
| SetFormat (k,s) :: l ->
interp subtyps { acc with extra = (k,s.CAst.v)::acc.extra; } l
@@ -955,9 +955,9 @@ let join_auxiliary_recursive_types recvars etyps =
| None, Some ytyp -> (x,ytyp)::typs
| Some xtyp, Some ytyp when (=) xtyp ytyp -> typs (* FIXME *)
| Some xtyp, Some ytyp ->
- user_err
- (strbrk "In " ++ Id.print x ++ str " .. " ++ Id.print y ++
- strbrk ", both ends have incompatible types."))
+ user_err
+ (strbrk "In " ++ Id.print x ++ str " .. " ++ Id.print y ++
+ strbrk ", both ends have incompatible types."))
recvars etyps
let internalization_type_of_entry_type = function
@@ -1103,7 +1103,7 @@ let find_precedence custom lev etyps symbols onlyprint =
| (ETIdent | ETBigint | ETGlobal), _ ->
begin match lev with
| None ->
- ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
+ ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
| Some 0 ->
([],0)
| _ ->
@@ -1115,12 +1115,12 @@ let find_precedence custom lev etyps symbols onlyprint =
user_err Pp.(str "Need an explicit level.")
else [],Option.get lev
with Not_found ->
- if Option.is_empty lev then
- user_err Pp.(str "A left-recursive notation must have an explicit level.")
- else [],Option.get lev)
+ if Option.is_empty lev then
+ user_err Pp.(str "A left-recursive notation must have an explicit level.")
+ else [],Option.get lev)
| Some (Terminal _) when last_is_terminal () ->
if Option.is_empty lev then
- ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
+ ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
else [],Option.get lev
| Some _ ->
if Option.is_empty lev then user_err Pp.(str "Cannot determine the level.");
@@ -1146,7 +1146,7 @@ let remove_curly_brackets l =
let br',next' = skip_break [] l' in
(match next' with
| Terminal "}" as t2 :: l'' ->
- if deb && List.is_empty l'' then [t1;x;t2] else begin
+ if deb && List.is_empty l'' then [t1;x;t2] else begin
check_curly_brackets_notation_exists ();
x :: aux false l''
end
@@ -1565,7 +1565,7 @@ let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc =
Dumpglob.dump_notation (loc,df') sc true
let add_notation_extra_printing_rule df k v =
- let notk =
+ let notk =
let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
make_notation_key InConstrEntrySomeLevel symbs in
add_notation_extra_printing_rule notk k v
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 0130de2543..9c18441d9c 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -127,7 +127,7 @@ let ml_load s =
| WithoutTop ->
try
Dynlink.loadfile s; s
- with Dynlink.Error a ->
+ with Dynlink.Error a ->
user_err ~hdr:"Mltop.load_object"
(strbrk "while loading " ++ str s ++
strbrk ": " ++ str (Dynlink.error_message a))
@@ -147,7 +147,7 @@ let dir_ml_use s =
| _ ->
let moreinfo =
if Sys.(backend_type = Native) then " Loading ML code works only in bytecode."
- else ""
+ else ""
in
user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 4ea34e2b60..76dbf1ad5a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -61,39 +61,39 @@ let subst_evar_constr evm evs n idf t =
let evar_info id = List.assoc_f Evar.equal id evs in
let rec substrec (depth, fixrels) c = match EConstr.kind evm c with
| Evar (k, args) ->
- let { ev_name = (id, idstr) ;
- ev_hyps = hyps ; ev_chop = chop } =
- try evar_info k
- with Not_found ->
- anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.")
- in
+ let { ev_name = (id, idstr) ;
+ ev_hyps = hyps ; ev_chop = chop } =
+ try evar_info k
+ with Not_found ->
+ anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.")
+ in
seen := Int.Set.add id !seen;
- (* Evar arguments are created in inverse order,
- and we must not apply to defined ones (i.e. LetIn's)
- *)
- let args =
- let n = match chop with None -> 0 | Some c -> c in
- let (l, r) = List.chop n (List.rev (Array.to_list args)) in
- List.rev r
- in
- let args =
- let rec aux hyps args acc =
+ (* Evar arguments are created in inverse order,
+ and we must not apply to defined ones (i.e. LetIn's)
+ *)
+ let args =
+ let n = match chop with None -> 0 | Some c -> c in
+ let (l, r) = List.chop n (List.rev (Array.to_list args)) in
+ List.rev r
+ in
+ let args =
+ let rec aux hyps args acc =
let open Context.Named.Declaration in
- match hyps, args with
- (LocalAssum _ :: tlh), (c :: tla) ->
- aux tlh tla ((substrec (depth, fixrels) c) :: acc)
- | (LocalDef _ :: tlh), (_ :: tla) ->
- aux tlh tla acc
- | [], [] -> acc
- | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
- in aux hyps args []
- in
- if List.exists
+ match hyps, args with
+ (LocalAssum _ :: tlh), (c :: tla) ->
+ aux tlh tla ((substrec (depth, fixrels) c) :: acc)
+ | (LocalDef _ :: tlh), (_ :: tla) ->
+ aux tlh tla acc
+ | [], [] -> acc
+ | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
+ in aux hyps args []
+ in
+ if List.exists
(fun x -> match EConstr.kind evm x with
| Rel n -> Int.List.mem n fixrels
| _ -> false) args
then
- transparent := Id.Set.add idstr !transparent;
+ transparent := Id.Set.add idstr !transparent;
EConstr.mkApp (idf idstr, Array.of_list args)
| Fix _ ->
EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
@@ -122,22 +122,22 @@ let etype_of_evar evm evs hyps concl =
let rec aux acc n = function
decl :: tl ->
let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in
- let t'' = subst_vars acc 0 t' in
- let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
- let s' = Int.Set.union s s' in
- let trans' = Id.Set.union trans trans' in
- (match decl with
+ let t'' = subst_vars acc 0 t' in
+ let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
+ let s' = Int.Set.union s s' in
+ let trans' = Id.Set.union trans trans' in
+ (match decl with
| LocalDef (id,c,_) ->
let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
- let c' = subst_vars acc 0 c' in
+ let c' = subst_vars acc 0 c' in
mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
- Int.Set.union s'' s',
- Id.Set.union trans'' trans'
+ Int.Set.union s'' s',
+ Id.Set.union trans'' trans'
| LocalAssum (id,_) ->
mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
| [] ->
let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
- subst_vars acc 0 t', s, trans
+ subst_vars acc 0 t', s, trans
in aux [] 0 (List.rev hyps)
let trunc_named_context n ctx =
@@ -171,10 +171,10 @@ let evar_dependencies evm oev =
let move_after (id, ev, deps as obl) l =
let rec aux restdeps = function
| (id', _, _) as obl' :: tl ->
- let restdeps' = Evar.Set.remove id' restdeps in
- if Evar.Set.is_empty restdeps' then
- obl' :: obl :: tl
- else obl' :: aux restdeps' tl
+ let restdeps' = Evar.Set.remove id' restdeps in
+ if Evar.Set.is_empty restdeps' then
+ obl' :: obl :: tl
+ else obl' :: aux restdeps' tl
| [] -> [obl]
in aux (Evar.Set.remove id deps) l
@@ -182,10 +182,10 @@ let sort_dependencies evl =
let rec aux l found list =
match l with
| (id, ev, deps) as obl :: tl ->
- let found' = Evar.Set.union found (Evar.Set.singleton id) in
- if Evar.Set.subset deps found' then
- aux tl found' (obl :: list)
- else aux (move_after obl tl) found list
+ let found' = Evar.Set.union found (Evar.Set.singleton id) in
+ if Evar.Set.subset deps found' then
+ aux tl found' (obl :: list)
+ else aux (move_after obl tl) found list
| [] -> List.rev list
in aux evl Evar.Set.empty []
@@ -204,54 +204,54 @@ let eterm_obligations env name evm fs ?status t ty =
let evn =
let i = ref (-1) in
List.rev_map (fun (id, ev) -> incr i;
- (id, (!i, Id.of_string
- (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))),
- ev)) evl
+ (id, (!i, Id.of_string
+ (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))),
+ ev)) evl
in
let evts =
(* Remove existential variables in types and build the corresponding products *)
List.fold_right
(fun (id, (n, nstr), ev) l ->
- let hyps = Evd.evar_filtered_context ev in
+ let hyps = Evd.evar_filtered_context ev in
let hyps = trunc_named_context nc_len hyps in
let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in
- let evtyp, hyps, chop =
- match chop_product fs evtyp with
- | Some t -> t, trunc_named_context fs hyps, fs
- | None -> evtyp, hyps, 0
- in
- let loc, k = evar_source id evm in
- let status = match k with
+ let evtyp, hyps, chop =
+ match chop_product fs evtyp with
+ | Some t -> t, trunc_named_context fs hyps, fs
+ | None -> evtyp, hyps, 0
+ in
+ let loc, k = evar_source id evm in
+ let status = match k with
| Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o
| _ -> match status with
| Some o -> o
| None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
in
let force_status, status, chop = match status with
- | Evar_kinds.Define true as stat ->
- if not (Int.equal chop fs) then true, Evar_kinds.Define false, None
- else false, stat, Some chop
- | s -> false, s, None
- in
- let info = { ev_name = (n, nstr);
- ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop;
- ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None }
- in (id, info) :: l)
+ | Evar_kinds.Define true as stat ->
+ if not (Int.equal chop fs) then true, Evar_kinds.Define false, None
+ else false, stat, Some chop
+ | s -> false, s, None
+ in
+ let info = { ev_name = (n, nstr);
+ ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop;
+ ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None }
+ in (id, info) :: l)
evn []
in
let t', _, transparent = (* Substitute evar refs in the term by variables *)
subst_evar_constr evm evts 0 EConstr.mkVar t
in
let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
- let evars =
+ let evars =
List.map (fun (ev, info) ->
let { ev_name = (_, name); ev_status = force_status, status;
- ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
+ ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
in
let force_status, status = match status with
- | Evar_kinds.Define true when Id.Set.mem name transparent ->
- true, Evar_kinds.Define false
- | _ -> force_status, status
+ | Evar_kinds.Define true when Id.Set.mem name transparent ->
+ true, Evar_kinds.Define false
+ | _ -> force_status, status
in name, typ, src, (force_status, status), deps, tac) evts
in
let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
@@ -303,20 +303,20 @@ let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind
let obls', b =
match b with
| None ->
- assert(Int.equal (Array.length obls) 0);
- let n = Nameops.add_suffix n "_obligation" in
- [| { obl_name = n; obl_body = None;
- obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t;
- obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
- obl_tac = None } |],
- mkVar n
+ assert(Int.equal (Array.length obls) 0);
+ let n = Nameops.add_suffix n "_obligation" in
+ [| { obl_name = n; obl_body = None;
+ obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t;
+ obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
+ obl_tac = None } |],
+ mkVar n
| Some b ->
- Array.mapi
- (fun i (n, t, l, o, d, tac) ->
+ Array.mapi
+ (fun i (n, t, l, o, d, tac) ->
{ obl_name = n ; obl_body = None;
- obl_location = l; obl_type = t; obl_status = o;
- obl_deps = d; obl_tac = tac })
- obls, b
+ obl_location = l; obl_type = t; obl_status = o;
+ obl_deps = d; obl_tac = tac })
+ obls, b
in
let ctx = UState.make_flexible_nonalgebraic ctx in
{ prg_name = n
@@ -348,23 +348,23 @@ exception Found of program_info CEphemeron.key
let map_first m =
try
ProgMap.iter (fun _ v ->
- if snd (CEphemeron.get v).prg_obligations > 0 then
- raise (Found v)) m;
+ if snd (CEphemeron.get v).prg_obligations > 0 then
+ raise (Found v)) m;
assert(false)
with Found x -> x
let get_prog name =
let prg_infos = get_prg_info_map () in
match name with
- Some n ->
+ Some n ->
(try CEphemeron.get (ProgMap.find n prg_infos)
- with Not_found -> raise (NoObligations (Some n)))
+ with Not_found -> raise (NoObligations (Some n)))
| None ->
- (let n = map_cardinal prg_infos in
- match n with
- 0 -> raise (NoObligations None)
+ (let n = map_cardinal prg_infos in
+ match n with
+ 0 -> raise (NoObligations None)
| 1 -> CEphemeron.get (map_first prg_infos)
- | _ ->
+ | _ ->
let progs = Id.Set.elements (ProgMap.domain prg_infos) in
let prog = List.hd progs in
let progs = prlist_with_sep pr_comma Id.print progs in
@@ -505,9 +505,9 @@ and obligation (user_num, name, typ) tac =
let obls, rem = prg.prg_obligations in
if num >= 0 && num < Array.length obls then
let obl = obls.(num) in
- match obl.obl_body with
+ match obl.obl_body with
| None -> solve_obligation prg num tac
- | Some r -> error "Obligation already solved"
+ | Some r -> error "Obligation already solved"
else error (sprintf "Unknown obligation number %i" (succ num))
@@ -560,12 +560,12 @@ and solve_prg_obligations prg ?oblset tac =
Array.iteri (fun i x ->
if p i then
match solve_obligation_by_tac !prgref obls' i tac with
- | None -> ()
- | Some prg' ->
- prgref := prg';
- let deps = dependencies obls i in
- (set := Int.Set.union !set deps;
- decr rem))
+ | None -> ()
+ | Some prg' ->
+ prgref := prg';
+ let deps = dependencies obls i in
+ (set := Int.Set.union !set deps;
+ decr rem))
obls'
in
update_obls !prgref obls' !rem
@@ -599,18 +599,18 @@ let show_obligations_of_prg ?(msg=true) prg =
let showed = ref 5 in
if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: ");
Array.iteri (fun i x ->
- match x.obl_body with
- | None ->
- if !showed > 0 then (
- decr showed;
- let x = subst_deps_obl obls x in
+ match x.obl_body with
+ | None ->
+ if !showed > 0 then (
+ decr showed;
+ let x = subst_deps_obl obls x in
let env = Global.env () in
let sigma = Evd.from_env env in
- Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
- str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
+ Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
+ str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
hov 1 (Printer.pr_constr_env env sigma x.obl_type ++
- str "." ++ fnl ())))
- | Some _ -> ())
+ str "." ++ fnl ())))
+ | Some _ -> ())
obls
let show_obligations ?(msg=true) n =
@@ -618,7 +618,7 @@ let show_obligations ?(msg=true) n =
| None -> all_programs ()
| Some n ->
try [ProgMap.find n (get_prg_info_map ())]
- with Not_found -> raise (NoObligations (Some n))
+ with Not_found -> raise (NoObligations (Some n))
in List.iter (fun x -> show_obligations_of_prg ~msg (CEphemeron.get x)) progs
let show_term n =
@@ -645,9 +645,9 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
progmap_add name (CEphemeron.create prg);
let res = auto_solve_obligations (Some name) tactic in
- match res with
+ match res with
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res
- | _ -> res)
+ | _ -> res)
let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce)
@@ -660,15 +660,15 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
in progmap_add n (CEphemeron.create prg)) l;
let _defined =
List.fold_left (fun finished x ->
- if finished then finished
- else
- let res = auto_solve_obligations (Some x) tactic in
- match res with
+ if finished then finished
+ else
+ let res = auto_solve_obligations (Some x) tactic in
+ match res with
| Defined _ ->
(* If one definition is turned into a constant,
- the whole block is defined. *) true
- | _ -> false)
- false deps
+ the whole block is defined. *) true
+ | _ -> false)
+ false deps
in ()
let admit_prog prg =
diff --git a/vernac/record.ml b/vernac/record.ml
index b60bfdfa22..49a73271f0 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -71,8 +71,8 @@ let interp_fields_evars env sigma impls_env nots l =
Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
let impls =
- match i with
- | Anonymous -> impls
+ match i with
+ | Anonymous -> impls
| Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
in
let d = match b' with
@@ -87,7 +87,7 @@ let compute_constructor_level evars env l =
List.fold_right (fun d (env, univ) ->
let univ =
if is_local_assum d then
- let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
+ let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
Univ.sup (univ_of_sort s) univ
else univ
in (EConstr.push_rel d env, univ))
@@ -123,8 +123,8 @@ let typecheck_params_and_fields finite def poly pl ps records =
| _ -> ()
in
List.iter
- (function CLocalDef (b, _, _) -> error default_binder_kind b
- | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
+ (function CLocalDef (b, _, _) -> error default_binder_kind b
+ | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
| CLocalPattern {CAst.loc} ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps
in
@@ -138,9 +138,9 @@ let typecheck_params_and_fields finite def poly pl ps records =
let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in
let sred = Reductionops.whd_allnolet env sigma s in
(match EConstr.kind sigma sred with
- | Sort s' ->
+ | Sort s' ->
let s' = EConstr.ESorts.kind sigma s' in
- (if poly then
+ (if poly then
match Evd.is_sort_variable sigma s' with
| Some l ->
let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in
@@ -148,7 +148,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
| None ->
(sigma, false), (s, s')
else (sigma, false), (s, s'))
- | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
+ | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
| None ->
let uvarkind = Evd.univ_flexible_alg in
let sigma, s = Evd.new_sort_variable uvarkind sigma in
@@ -184,8 +184,8 @@ let typecheck_params_and_fields finite def poly pl ps records =
let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in
if Univ.is_small_univ univ &&
Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
- (* We can assume that the level in aritysort is not constrained
- and clear it, if it is flexible *)
+ (* We can assume that the level in aritysort is not constrained
+ and clear it, if it is flexible *)
Evd.set_eq_sort env_ar sigma Sorts.set sort, (univ, EConstr.mkSort (Sorts.sort_of_univ univ))
else sigma, (univ, typ)
in
@@ -220,24 +220,24 @@ message. The user might still want to name the field of the record. *)
let warning_or_error coe indsp err =
let st = match err with
| MissingProj (fi,projs) ->
- let s,have = if List.length projs > 1 then "s","were" else "","was" in
+ let s,have = if List.length projs > 1 then "s","were" else "","was" in
(Id.print fi ++
- strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
+ strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
prlist_with_sep pr_comma Id.print projs ++ spc () ++ str have ++
- strbrk " not defined.")
+ strbrk " not defined.")
| BadTypedProj (fi,ctx,te) ->
- match te with
+ match te with
| ElimArity (_,_,_,Some (_,_,_,NonInformativeToInformative)) ->
(Id.print fi ++
- strbrk" cannot be defined because it is informative and " ++
- Printer.pr_inductive (Global.env()) indsp ++
- strbrk " is not.")
+ strbrk" cannot be defined because it is informative and " ++
+ Printer.pr_inductive (Global.env()) indsp ++
+ strbrk " is not.")
| ElimArity (_,_,_,Some (_,_,_,StrongEliminationOnNonSmallType)) ->
- (Id.print fi ++
- strbrk" cannot be defined because it is large and " ++
- Printer.pr_inductive (Global.env()) indsp ++
- strbrk " is not.")
- | _ ->
+ (Id.print fi ++
+ strbrk" cannot be defined because it is large and " ++
+ Printer.pr_inductive (Global.env()) indsp ++
+ strbrk " is not.")
+ | _ ->
(Id.print fi ++ strbrk " cannot be defined because it is not typable.")
in
if coe then user_err ~hdr:"structure" st;
@@ -259,19 +259,19 @@ let subst_projection fid l c =
let bad_projs = ref [] in
let rec substrec depth c = match Constr.kind c with
| Rel k ->
- (* We are in context [[params;fields;x:ind;...depth...]] *)
+ (* We are in context [[params;fields;x:ind;...depth...]] *)
if k <= depth+1 then
- c
+ c
else if k-depth-1 <= lv then
- match List.nth l (k-depth-2) with
- | Projection t -> lift depth t
- | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
- | NoProjection Anonymous ->
+ match List.nth l (k-depth-2) with
+ | Projection t -> lift depth t
+ | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
+ | NoProjection Anonymous ->
user_err (str "Field " ++ Id.print fid ++
str " depends on the " ++ pr_nth (k-depth-1) ++ str
" field which has no name.")
else
- mkRel (k-lv)
+ mkRel (k-lv)
| _ -> Constr.map_with_binders succ substrec depth c
in
let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *)
@@ -316,13 +316,13 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
(fun (nfi,i,kinds,sp_projs,subst) flags decl impls ->
let fi = RelDecl.get_name decl in
let ti = RelDecl.get_type decl in
- let (sp_projs,i,subst) =
- match fi with
- | Anonymous ->
- (None::sp_projs,i,NoProjection fi::subst)
- | Name fid -> try
+ let (sp_projs,i,subst) =
+ match fi with
+ | Anonymous ->
+ (None::sp_projs,i,NoProjection fi::subst)
+ | Name fid -> try
let kn, term =
- if is_local_assum decl && primitive then
+ if is_local_assum decl && primitive then
let p = Projection.Repr.make indsp
~proj_npars:mib.mind_nparams
~proj_arg:i
@@ -332,48 +332,48 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
let kn = Projection.Repr.constant p in
Declare.definition_message fid;
kn, mkProj (Projection.make p false,mkRel 1)
- else
- let ccl = subst_projection fid subst ti in
- let body = match decl with
+ else
+ let ccl = subst_projection fid subst ti in
+ let body = match decl with
| LocalDef (_,ci,_) -> subst_projection fid subst ci
| LocalAssum ({binder_relevance=rci},_) ->
- (* [ccl] is defined in context [params;x:rp] *)
- (* [ccl'] is defined in context [params;x:rp;x:rp] *)
- let ccl' = liftn 1 2 ccl in
+ (* [ccl] is defined in context [params;x:rp] *)
+ (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+ let ccl' = liftn 1 2 ccl in
let p = mkLambda (x, lift 1 rp, ccl') in
- let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
+ let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
let ci = Inductiveops.make_case_info env indsp rci LetStyle in
(* Record projections have no is *)
mkCase (ci, p, mkRel 1, [|branch|])
in
- let proj =
+ let proj =
it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
- let projtyp =
+ let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
- try
+ try
let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
let kind = Decls.IsDefinition kind in
let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
- let constr_fip =
- let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
+ let constr_fip =
+ let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
applist (mkConstU (kn,u),proj_args)
in
Declare.definition_message fid;
- kn, constr_fip
+ kn, constr_fip
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te)))
- in
+ in
let refi = GlobRef.ConstRef kn in
- Impargs.maybe_declare_manual_implicits false refi impls;
+ Impargs.maybe_declare_manual_implicits false refi impls;
if flags.pf_subclass then begin
let cl = Class.class_of_global (GlobRef.IndRef indsp) in
Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
- end;
- let i = if is_local_assum decl then i+1 else i in
- (Some kn::sp_projs, i, Projection term::subst)
+ end;
+ let i = if is_local_assum decl then i+1 else i in
+ (Some kn::sp_projs, i, Projection term::subst)
with NotDefinable why ->
warning_or_error flags.pf_subclass indsp why;
- (None::sp_projs,i,NoProjection fi::subst) in
+ (None::sp_projs,i,NoProjection fi::subst) in
(nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))
(List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
@@ -536,8 +536,8 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
in
let coers = List.map2 (fun coe pri ->
Option.map (fun b ->
- if b then Backward, pri else Forward, pri) coe)
- coers priorities
+ if b then Backward, pri else Forward, pri) coe)
+ coers priorities
in
let map ind =
let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y)
@@ -615,11 +615,11 @@ let add_inductive_class env sigma ind =
let r = Inductive.relevance_of_inductive env ind in
{ cl_univs = univs;
cl_impl = GlobRef.IndRef ind;
- cl_context = List.map (const None) ctx, ctx;
+ cl_context = List.map (const None) ctx, ctx;
cl_props = [LocalAssum (make_annot Anonymous r, ty)];
- cl_projs = [];
- cl_strict = !typeclasses_strict;
- cl_unique = !typeclasses_unique }
+ cl_projs = [];
+ cl_strict = !typeclasses_strict;
+ cl_unique = !typeclasses_unique }
in
Classes.add_class env sigma k
diff --git a/vernac/search.ml b/vernac/search.ml
index 06554aae20..364dae7152 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -39,7 +39,7 @@ module SearchBlacklist =
let key = ["Search";"Blacklist"]
let title = "Current search blacklist : "
let member_message s b =
- str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s
+ str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s
end)
(* The functions iter_constructors and iter_declarations implement the behavior
@@ -330,7 +330,7 @@ let interface_search ?pstate =
in
let match_subtype (pat, flag) =
toggle
- (Constr_matching.is_matching_appsubterm ~closed:false
+ (Constr_matching.is_matching_appsubterm ~closed:false
env (Evd.from_env env) pat (EConstr.of_constr constr)) flag
in
let match_module (mdl, flag) =
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 046defc26b..45f40b1258 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -368,12 +368,12 @@ let pr_loc loc =
match fname with
| Loc.ToplevelInput ->
Loc.(str"Toplevel input, characters " ++ int loc.bp ++
- str"-" ++ int loc.ep ++ str":")
+ str"-" ++ int loc.ep ++ str":")
| Loc.InFile fname ->
Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
- str", line " ++ int loc.line_nb ++ str", characters " ++
- int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
- str":")
+ str", line " ++ int loc.line_nb ++ str", characters " ++
+ int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
+ str":")
let pr_phase ?loc () =
match !default_phase, loc with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 128c30908b..f56cc00c3b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -176,7 +176,7 @@ let print_module qid =
match globdir with
DirModule Nametab.{ obj_dir; obj_mp; _ } ->
Printmod.print_module ~mod_ops:Declaremods.mod_ops (Printmod.printable_body obj_dir) obj_mp
- | _ -> raise Not_found
+ | _ -> raise Not_found
with
Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid)
@@ -696,11 +696,11 @@ let vernac_inductive ~atts cum lo finite indl =
if Dumpglob.dump () then
List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
match cstrs with
- | Constructors cstrs ->
- Dumpglob.dump_definition lid false "ind";
- List.iter (fun (_, (lid, _)) ->
- Dumpglob.dump_definition lid false "constr") cstrs
- | _ -> () (* dumping is done by vernac_record (called below) *) )
+ | Constructors cstrs ->
+ Dumpglob.dump_definition lid false "ind";
+ List.iter (fun (_, (lid, _)) ->
+ Dumpglob.dump_definition lid false "constr") cstrs
+ | _ -> () (* dumping is done by vernac_record (called below) *) )
indl;
let is_record = function
@@ -780,7 +780,7 @@ let vernac_inductive ~atts cum lo finite indl =
| [ ( id , bl , c , Class _, Constructors [l]), [] ] ->
let f =
let (coe, ({loc;v=id}, ce)) = l in
- let coe' = if coe then Some true else None in
+ let coe' = if coe then Some true else None in
(((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), [])
in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
*)
@@ -829,11 +829,11 @@ let vernac_cofixpoint ~atts discharge l =
let vernac_scheme l =
if Dumpglob.dump () then
List.iter (fun (lid, s) ->
- Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid;
- match s with
- | InductionScheme (_, r, _)
+ Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid;
+ match s with
+ | InductionScheme (_, r, _)
| CaseScheme (_, r, _)
- | EqualityScheme r -> dump_global r) l;
+ | EqualityScheme r -> dump_global r) l;
Indschemes.do_scheme l
let vernac_combined_scheme lid l =
@@ -845,15 +845,15 @@ let vernac_combined_scheme lid l =
let vernac_universe ~poly l =
if poly && not (Global.sections_are_opened ()) then
user_err ~hdr:"vernac_universe"
- (str"Polymorphic universes can only be declared inside sections, " ++
- str "use Monomorphic Universe instead");
+ (str"Polymorphic universes can only be declared inside sections, " ++
+ str "use Monomorphic Universe instead");
DeclareUniv.do_universe ~poly l
let vernac_constraint ~poly l =
if poly && not (Global.sections_are_opened ()) then
user_err ~hdr:"vernac_constraint"
- (str"Polymorphic universe constraints can only be declared"
- ++ str " inside sections, use Monomorphic Constraint instead");
+ (str"Polymorphic universe constraints can only be declared"
+ ++ str " inside sections, use Monomorphic Constraint instead");
DeclareUniv.do_constraint ~poly l
(**********************)
@@ -911,11 +911,11 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
else (idl,ty)) binders_ast in
let mp =
Declaremods.declare_module
- id binders_ast mty_ast_o mexpr_ast_l
+ id binders_ast mty_ast_o mexpr_ast_l
in
Dumpglob.dump_moddef ?loc mp "mod";
Flags.if_verbose Feedback.msg_info
- (str "Module " ++ Id.print id ++ str " is defined");
+ (str "Module " ++ Id.print id ++ str " is defined");
Option.iter (fun export -> vernac_import export [qualid_of_ident id])
export
@@ -932,7 +932,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
match mty_ast_l with
| [] ->
let binders_ast,argsexport =
- List.fold_right
+ List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
(idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast
([],[]) in
@@ -940,7 +940,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
let mp = Declaremods.start_modtype id binders_ast mty_sign in
Dumpglob.dump_moddef ?loc mp "modtype";
Flags.if_verbose Feedback.msg_info
- (str "Interactive Module Type " ++ Id.print id ++ str " started");
+ (str "Interactive Module Type " ++ Id.print id ++ str " started");
List.iter
(fun (export,id) ->
Option.iter
@@ -948,15 +948,15 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
) argsexport
| _ :: _ ->
- let binders_ast = List.map
+ let binders_ast = List.map
(fun (export,idl,ty) ->
if not (Option.is_empty export) then
user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
else (idl,ty)) binders_ast in
let mp = Declaremods.declare_modtype id binders_ast mty_sign mty_ast_l in
Dumpglob.dump_moddef ?loc mp "modtype";
- Flags.if_verbose Feedback.msg_info
- (str "Module Type " ++ Id.print id ++ str " is defined")
+ Flags.if_verbose Feedback.msg_info
+ (str "Module Type " ++ Id.print id ++ str " is defined")
let vernac_end_modtype {loc;v=id} =
let mp = Declaremods.end_modtype () in
@@ -1157,12 +1157,12 @@ let vernac_chdir = function
| None -> Feedback.msg_notice (str (Sys.getcwd()))
| Some path ->
begin
- try Sys.chdir (expand path)
- with Sys_error err ->
- (* Cd is typically used to control the output directory of
- extraction. A failed Cd could lead to overwriting .ml files
- so we make it an error. *)
- user_err Pp.(str ("Cd failed: " ^ err))
+ try Sys.chdir (expand path)
+ with Sys_error err ->
+ (* Cd is typically used to control the output directory of
+ extraction. A failed Cd could lead to overwriting .ml files
+ so we make it an error. *)
+ user_err Pp.(str ("Cd failed: " ^ err))
end;
Flags.if_verbose Feedback.msg_info (str (Sys.getcwd()))
@@ -1357,8 +1357,8 @@ let () =
optkey = ["Inline";"Level"];
optread = (fun () -> Some (Flags.get_inline_level ()));
optwrite = (fun o ->
- let lev = Option.default Flags.default_inline_level o in
- Flags.set_inline_level lev) }
+ let lev = Option.default Flags.default_inline_level o in
+ Flags.set_inline_level lev) }
let () =
declare_bool_option
@@ -1433,7 +1433,7 @@ let () =
optwrite = CWarnings.set_flags }
let () =
- declare_string_option
+ declare_string_option
{ optdepr = false;
optname = "native_compute profiler output";
optkey = ["NativeCompute"; "Profile"; "Filename"];
@@ -1599,7 +1599,7 @@ let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l
| Some r ->
let (sigma,r_interp) = Hook.get f_interp_redexp env sigma r in
- let redfun env evm c =
+ let redfun env evm c =
let (redfun, _) = reduction_of_red_expr env r_interp in
let (_, c) = redfun env evm c in
c
@@ -1656,8 +1656,8 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
(try get_nth_goal ~pstate 1, qualid_basename qid with _ -> raise NoHyp)
| Some n,AN qid when qualid_is_ident qid -> (* goal number given, catch if wong *)
(try get_nth_goal ~pstate n, qualid_basename qid
- with
- Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs"
+ with
+ Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs"
(str "No such goal: " ++ int n ++ str "."))
| _ , _ -> raise NoHyp in
let hyps = pf_hyps gl in
@@ -1667,7 +1667,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
| LocalDef (_,bdy,_) ->"Constant (let in)" in
let sigma, env = Pfedit.get_current_context pstate in
v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl()
- ++ str natureofid ++ str " of the goal context.")
+ ++ str natureofid ++ str " of the goal context.")
with (* fallback to globals *)
| NoHyp | Not_found ->
let sigma, env = get_current_or_global_context ~pstate in
@@ -1730,7 +1730,7 @@ let vernac_print ~pstate ~atts =
let cstr = printable_constr_of_global gr in
let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
let nassums =
- Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in
+ Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in
Printer.pr_assumptionset env sigma nassums
| PrintStrategy r -> print_strategy r
| PrintRegistered -> print_registered ()
@@ -1756,12 +1756,12 @@ let interp_search_about_item env sigma =
GlobSearchString s
| SearchString (s,sc) ->
try
- let ref =
- Notation.interp_notation_as_global_reference
- (fun _ -> true) s sc in
- GlobSearchSubPattern (Pattern.PRef ref)
+ let ref =
+ Notation.interp_notation_as_global_reference
+ (fun _ -> true) s sc in
+ GlobSearchSubPattern (Pattern.PRef ref)
with UserError _ ->
- user_err ~hdr:"interp_search_about_item"
+ user_err ~hdr:"interp_search_about_item"
(str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 10:56:23 +0000