diff options
| author | Pierre-Marie Pédrot | 2017-07-26 17:53:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-26 18:40:15 +0200 |
| commit | 4395637a6471fc95934fe93da671bda68d415a77 (patch) | |
| tree | fd51fbf117afb8dda9f97e1988e437c133ffeaa7 /src/tac2core.ml | |
| parent | 2a74da7b6f275634fd8ed9c209edc73f2ae15427 (diff) | |
Ensuring that inductive constructors are always capitalized.
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 () |