aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.ml4')
-rw-r--r--parsing/pcoq.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d72a49046..07055869a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -576,7 +576,7 @@ let find_position forpat other assoc lev =
| (p,_ as pa)::l when p > n -> pa :: add_level (Some p) l
| (p,a)::l when p = n ->
if admissible_assoc (a,assoc) then raise Exit;
- error_level_assoc p a (out_some assoc)
+ error_level_assoc p a (Option.get assoc)
| l -> after := q; (n,create_assoc assoc)::l
in
try
@@ -587,7 +587,7 @@ let find_position forpat other assoc lev =
level_stack := updated:: !level_stack;
let assoc = create_assoc assoc in
(if !after = None then Some Gramext.First
- else Some (Gramext.After (constr_level (out_some !after)))),
+ else Some (Gramext.After (constr_level (Option.get !after)))),
Some assoc, Some (constr_level n)
with
Exit ->