diff options
| author | Pierre-Marie Pédrot | 2017-07-27 16:50:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-27 19:08:15 +0200 |
| commit | 86e7ec3bd7b26b1d377c8397b62346f5e44f5d87 (patch) | |
| tree | 0d92b784ace5c130c8f41bd856f19113e8bebcde /src/tac2core.ml | |
| parent | fee254e2f7a343629df31d5a39780ca4698de571 (diff) | |
Factorizing code for constructors and tuples.
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 ab1eaec9d9..a3678d1ad0 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -844,7 +844,7 @@ let dummy_loc = Loc.make_loc (-1, -1) let rthunk e = let loc = Tac2intern.loc_of_tacexpr e in - let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn Core.t_unit, []))] in + let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Other Core.t_unit), []))] in CTacFun (loc, var, e) let add_generic_scope s entry arg = @@ -905,9 +905,9 @@ let () = add_scope "opt" begin function let scope = Extend.Aopt scope in let act opt = match opt with | None -> - CTacCst (AbsKn Core.c_none) + CTacCst (dummy_loc, AbsKn (Other Core.c_none)) | Some x -> - CTacApp (dummy_loc, CTacCst (AbsKn Core.c_some), [act x]) + CTacApp (dummy_loc, CTacCst (dummy_loc, AbsKn (Other Core.c_some)), [act x]) in Tac2entries.ScopeRule (scope, act) | _ -> scope_fail () |