diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 15:38:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 15:38:39 +0100 |
| commit | d016f69818b30b75d186fb14f440b93b0518fc66 (patch) | |
| tree | 32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /vernac/egramcoq.ml | |
| parent | b680b06b31c27751a7d551d95839aea38f7fbea1 (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.ml | 28 |
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 |
