diff options
Diffstat (limited to 'src/tac2core.ml')
| -rw-r--r-- | src/tac2core.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index b665f761ce..2ccc49b043 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -734,7 +734,7 @@ let dummy_loc = Loc.make_loc (-1, -1) let rthunk e = let loc = Tac2intern.loc_of_tacexpr e in - let var = [CPatAny loc, Some (CTypRef (loc, AbsKn Core.t_unit, []))] in + let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn Core.t_unit, []))] in CTacFun (loc, var, e) let add_generic_scope s entry arg = @@ -795,9 +795,9 @@ let () = add_scope "opt" begin function let scope = Extend.Aopt scope in let act opt = match opt with | None -> - CTacRef (AbsKn (TacConstructor Core.c_none)) + CTacCst (AbsKn Core.c_none) | Some x -> - CTacApp (dummy_loc, CTacRef (AbsKn (TacConstructor Core.c_some)), [act x]) + CTacApp (dummy_loc, CTacCst (AbsKn Core.c_some), [act x]) in Tac2entries.ScopeRule (scope, act) | _ -> scope_fail () |