aboutsummaryrefslogtreecommitdiff
path: root/vernac/egramcoq.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-11-21 15:38:39 +0100
committerEmilio Jesus Gallego Arias2019-11-21 15:38:39 +0100
commitd016f69818b30b75d186fb14f440b93b0518fc66 (patch)
tree32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /vernac/egramcoq.ml
parentb680b06b31c27751a7d551d95839aea38f7fbea1 (diff)
[coq] Untabify the whole ML codebase.
We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ```
Diffstat (limited to 'vernac/egramcoq.ml')
-rw-r--r--vernac/egramcoq.ml28
1 files changed, 14 insertions, 14 deletions
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