From 4395637a6471fc95934fe93da671bda68d415a77 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Jul 2017 17:53:04 +0200
Subject: Ensuring that inductive constructors are always capitalized.

---
 src/tac2core.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src/tac2core.ml')

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 ()
-- 
cgit v1.2.3