Ensuring that inductive constructors are always capitalized.

8 files changed, 143 insertions, 140 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 605cb75d66..88a64dacd9 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -28,20 +28,32 @@ let inj_constr loc c = inj_wit Stdarg.wit_constr loc c
 let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c
 let inj_ident loc c = inj_wit Stdarg.wit_ident loc c
 
+let pattern_of_qualid loc id =
+  if Tac2env.is_constructor (snd id) then CPatRef (loc, RelId id, [])
+  else
+    let (dp, id) = Libnames.repr_qualid (snd id) in
+    if DirPath.is_empty dp then CPatVar (Some loc, Name id)
+    else
+      CErrors.user_err ~loc (Pp.str "Syntax error")
+
 GEXTEND Gram
   GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn;
   tac2pat:
     [ "1" LEFTA
-      [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, RelId id, pl)
-      | id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
+      [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" ->
+        if Tac2env.is_constructor (snd id) then
+          CPatRef (!@loc, RelId id, pl)
+        else
+          CErrors.user_err ~loc:!@loc (Pp.str "Syntax error")
+      | id = Prim.qualid -> pattern_of_qualid !@loc id
       | "["; "]" -> CPatRef (!@loc, AbsKn Tac2core.Core.c_nil, [])
       | p1 = tac2pat; "::"; p2 = tac2pat ->
         CPatRef (!@loc, AbsKn Tac2core.Core.c_cons, [p1; p2])
       ]
     | "0"
-      [ "_" -> CPatAny (!@loc)
+      [ "_" -> CPatVar (Some !@loc, Anonymous)
       | "()" -> CPatTup (Loc.tag ~loc:!@loc [])
-      | id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
+      | id = Prim.qualid -> pattern_of_qualid !@loc id
       | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (Loc.tag ~loc:!@loc pl) ]
     ]
   ;
@@ -90,7 +102,8 @@ GEXTEND Gram
   tactic_atom:
     [ [ n = Prim.integer -> CTacAtm (Loc.tag ~loc:!@loc (AtmInt n))
       | s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s))
-      | id = Prim.qualid -> CTacRef (RelId id)
+      | id = Prim.qualid ->
+        if Tac2env.is_constructor (snd id) then CTacCst (RelId id) else CTacRef (RelId id)
       | "@"; id = Prim.ident -> inj_ident !@loc id
       | "'"; c = Constr.constr -> inj_open_constr !@loc c
       | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
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 ()
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 100041f15e..da0e213340 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -34,14 +34,14 @@ type tacdef = {
 }
 
 let perform_tacdef visibility ((sp, kn), def) =
-  let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp (TacConstant kn) in
+  let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp kn in
   Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
 
 let load_tacdef i obj = perform_tacdef (Until i) obj
 let open_tacdef i obj = perform_tacdef (Exactly i) obj
 
 let cache_tacdef ((sp, kn), def) =
-  let () = Tac2env.push_ltac (Until 1) sp (TacConstant kn) in
+  let () = Tac2env.push_ltac (Until 1) sp kn in
   Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
 
 let subst_tacdef (subst, def) =
@@ -83,7 +83,7 @@ let push_typedef visibility sp kn (_, def) = match def with
   let iter (c, _) =
     let spc = change_sp_label sp c in
     let knc = change_kn_label kn c in
-    Tac2env.push_ltac visibility spc (TacConstructor knc)
+    Tac2env.push_constructor visibility spc knc
   in
   Tac2env.push_type visibility sp kn;
   List.iter iter cstrs
@@ -185,7 +185,7 @@ let push_typext vis sp kn def =
   let iter data =
     let spc = change_sp_label sp data.edata_name in
     let knc = change_kn_label kn data.edata_name in
-    Tac2env.push_ltac vis spc (TacConstructor knc)
+    Tac2env.push_constructor vis spc knc
   in
   List.iter iter def.typext_expr
 
@@ -620,12 +620,18 @@ let register_struct ?local str = match str with
 
 let print_ltac ref =
   let (loc, qid) = qualid_of_reference ref in
-  let kn =
-    try Tac2env.locate_ltac qid
-    with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid)
-  in
-  match kn with
-  | TacConstant kn ->
+  if Tac2env.is_constructor qid then
+    let kn =
+      try Tac2env.locate_constructor qid
+      with Not_found -> user_err ?loc (str "Unknown constructor " ++ pr_qualid qid)
+    in
+    let _ = Tac2env.interp_constructor kn in
+    Feedback.msg_notice (hov 2 (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid))
+  else
+    let kn =
+      try Tac2env.locate_ltac qid
+      with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid)
+    in
     let (e, _, (_, t)) = Tac2env.interp_global kn in
     let name = int_name () in
     Feedback.msg_notice (
@@ -634,9 +640,6 @@ let print_ltac ref =
         hov 2 (pr_qualid qid ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr e)
       )
     )
-  | TacConstructor kn ->
-    let _ = Tac2env.interp_constructor kn in
-    Feedback.msg_notice (hov 2 (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid))
 
 (** Calling tactics *)
 
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 08c7b321be..6e47e78a9d 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -115,25 +115,13 @@ struct
     id, (DirPath.repr dir)
 end
 
-type tacref = Tac2expr.tacref =
-| TacConstant of ltac_constant
-| TacConstructor of ltac_constructor
-
-module TacRef =
-struct
-type t = tacref
-let equal r1 r2 = match r1, r2 with
-| TacConstant c1, TacConstant c2 -> KerName.equal c1 c2
-| TacConstructor c1, TacConstructor c2 -> KerName.equal c1 c2
-| _ -> false
-end
-
 module KnTab = Nametab.Make(FullPath)(KerName)
-module RfTab = Nametab.Make(FullPath)(TacRef)
 
 type nametab = {
-  tab_ltac : RfTab.t;
-  tab_ltac_rev : full_path KNmap.t * full_path KNmap.t;
+  tab_ltac : KnTab.t;
+  tab_ltac_rev : full_path KNmap.t;
+  tab_cstr : KnTab.t;
+  tab_cstr_rev : full_path KNmap.t;
   tab_type : KnTab.t;
   tab_type_rev : full_path KNmap.t;
   tab_proj : KnTab.t;
@@ -141,8 +129,10 @@ type nametab = {
 }
 
 let empty_nametab = {
-  tab_ltac = RfTab.empty;
-  tab_ltac_rev = (KNmap.empty, KNmap.empty);
+  tab_ltac = KnTab.empty;
+  tab_ltac_rev = KNmap.empty;
+  tab_cstr = KnTab.empty;
+  tab_cstr_rev = KNmap.empty;
   tab_type = KnTab.empty;
   tab_type_rev = KNmap.empty;
   tab_proj = KnTab.empty;
@@ -153,29 +143,41 @@ let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab"
 
 let push_ltac vis sp kn =
   let tab = !nametab in
-  let tab_ltac = RfTab.push vis sp kn tab.tab_ltac in
-  let (constant_map, constructor_map) = tab.tab_ltac_rev in
-  let tab_ltac_rev = match kn with
-  | TacConstant c -> (KNmap.add c sp constant_map, constructor_map)
-  | TacConstructor c -> (constant_map, KNmap.add c sp constructor_map)
-  in
+  let tab_ltac = KnTab.push vis sp kn tab.tab_ltac in
+  let tab_ltac_rev = KNmap.add kn sp tab.tab_ltac_rev in
   nametab := { tab with tab_ltac; tab_ltac_rev }
 
 let locate_ltac qid =
   let tab = !nametab in
-  RfTab.locate qid tab.tab_ltac
+  KnTab.locate qid tab.tab_ltac
 
 let locate_extended_all_ltac qid =
   let tab = !nametab in
-  RfTab.find_prefixes qid tab.tab_ltac
+  KnTab.find_prefixes qid tab.tab_ltac
 
 let shortest_qualid_of_ltac kn =
   let tab = !nametab in
-  let sp = match kn with
-  | TacConstant c -> KNmap.find c (fst tab.tab_ltac_rev)
-  | TacConstructor c -> KNmap.find c (snd tab.tab_ltac_rev)
-  in
-  RfTab.shortest_qualid Id.Set.empty sp tab.tab_ltac
+  let sp = KNmap.find kn tab.tab_ltac_rev in
+  KnTab.shortest_qualid Id.Set.empty sp tab.tab_ltac
+
+let push_constructor vis sp kn =
+  let tab = !nametab in
+  let tab_cstr = KnTab.push vis sp kn tab.tab_cstr in
+  let tab_cstr_rev = KNmap.add kn sp tab.tab_cstr_rev in
+  nametab := { tab with tab_cstr; tab_cstr_rev }
+
+let locate_constructor qid =
+  let tab = !nametab in
+  KnTab.locate qid tab.tab_cstr
+
+let locate_extended_all_constructor qid =
+  let tab = !nametab in
+  KnTab.find_prefixes qid tab.tab_cstr
+
+let shortest_qualid_of_constructor kn =
+  let tab = !nametab in
+  let sp = KNmap.find kn tab.tab_cstr_rev in
+  KnTab.shortest_qualid Id.Set.empty sp tab.tab_cstr
 
 let push_type vis sp kn =
   let tab = !nametab in
@@ -240,3 +242,14 @@ let coq_prefix =
 (** Generic arguments *)
 
 let wit_ltac2 = Genarg.make0 "ltac2"
+
+let is_constructor qid =
+  let (_, id) = repr_qualid qid in
+  let id = Id.to_string id in
+  assert (String.length id > 0);
+  match id with
+  | "true" | "false" -> true (** built-in constructors *)
+  | _ ->
+    match id.[0] with
+    | 'A'..'Z' -> true
+    | _ -> false
diff --git a/src/tac2env.mli b/src/tac2env.mli
index c4b8c1e0ca..8ab9656cb9 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -63,10 +63,15 @@ val interp_projection : ltac_projection -> projection_data
 
 (** {5 Name management} *)
 
-val push_ltac : visibility -> full_path -> tacref -> unit
-val locate_ltac : qualid -> tacref
-val locate_extended_all_ltac : qualid -> tacref list
-val shortest_qualid_of_ltac : tacref -> qualid
+val push_ltac : visibility -> full_path -> ltac_constant -> unit
+val locate_ltac : qualid -> ltac_constant
+val locate_extended_all_ltac : qualid -> ltac_constant list
+val shortest_qualid_of_ltac : ltac_constant -> qualid
+
+val push_constructor : visibility -> full_path -> ltac_constructor -> unit
+val locate_constructor : qualid -> ltac_constructor
+val locate_extended_all_constructor : qualid -> ltac_constructor list
+val shortest_qualid_of_constructor : ltac_constructor -> qualid
 
 val push_type : visibility -> full_path -> type_constant -> unit
 val locate_type : qualid -> type_constant
@@ -104,3 +109,7 @@ val coq_prefix : ModPath.t
 (** {5 Generic arguments} *)
 
 val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
+
+(** {5 Helper functions} *)
+
+val is_constructor : qualid -> bool
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index a9f2109cb2..b268e70cb3 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -70,19 +70,16 @@ type atom =
 | AtmInt of int
 | AtmStr of string
 
-type tacref =
-| TacConstant of ltac_constant
-| TacConstructor of ltac_constructor
-
 (** Tactic expressions *)
 type raw_patexpr =
-| CPatAny of Loc.t
+| CPatVar of Name.t located
 | CPatRef of Loc.t * ltac_constructor or_relid * raw_patexpr list
 | CPatTup of raw_patexpr list located
 
 type raw_tacexpr =
 | CTacAtm of atom located
-| CTacRef of tacref or_relid
+| CTacRef of ltac_constant or_relid
+| CTacCst of ltac_constructor or_relid
 | CTacFun of Loc.t * (raw_patexpr * raw_typexpr option) list * raw_tacexpr
 | CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list
 | CTacLet of Loc.t * rec_flag * (Name.t located * raw_typexpr option * raw_tacexpr) list * raw_tacexpr
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 79e33f3a94..3ea35171bb 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -191,6 +191,8 @@ let loc_of_tacexpr = function
 | CTacAtm (loc, _) -> Option.default dummy_loc loc
 | CTacRef (RelId (loc, _)) -> Option.default dummy_loc loc
 | CTacRef (AbsKn _) -> dummy_loc
+| CTacCst (RelId (loc, _)) -> Option.default dummy_loc loc
+| CTacCst (AbsKn _) -> dummy_loc
 | CTacFun (loc, _, _) -> loc
 | CTacApp (loc, _, _) -> loc
 | CTacLet (loc, _, _, _) -> loc
@@ -206,7 +208,7 @@ let loc_of_tacexpr = function
 | CTacExt (loc, _) -> loc
 
 let loc_of_patexpr = function
-| CPatAny loc -> loc
+| CPatVar (loc, _) -> Option.default dummy_loc loc
 | CPatRef (loc, _, _) -> loc
 | CPatTup (loc, _) -> Option.default dummy_loc loc
 
@@ -516,22 +518,17 @@ let get_variable env var =
 
 let get_constructor env var = match var with
 | RelId (loc, qid) ->
-  let c = try Some (Tac2env.locate_ltac qid) with Not_found -> None in
+  let c = try Some (Tac2env.locate_constructor qid) with Not_found -> None in
   begin match c with
-  | Some (TacConstructor knc) ->
+  | Some knc ->
     let kn = Tac2env.interp_constructor knc in
-    ArgArg (kn, knc)
-  | Some (TacConstant _) ->
-    CErrors.user_err ?loc (str "The term " ++ pr_qualid qid ++
-      str " is not the constructor of an inductive type.")
+    (kn, knc)
   | None ->
-    let (dp, id) = repr_qualid qid in
-    if DirPath.is_empty dp then ArgVar (loc, id)
-    else CErrors.user_err ?loc (str "Unbound constructor " ++ pr_qualid qid)
+    CErrors.user_err ?loc (str "Unbound constructor " ++ pr_qualid qid)
   end
 | AbsKn knc ->
   let kn = Tac2env.interp_constructor knc in
-  ArgArg (kn, knc)
+  (kn, knc)
 
 let get_projection var = match var with
 | RelId (loc, qid) ->
@@ -562,18 +559,10 @@ type glb_patexpr =
 | GPatTup of glb_patexpr list
 
 let rec intern_patexpr env = function
-| CPatAny _ -> GPatVar Anonymous
-| CPatRef (_, qid, []) ->
-  begin match get_constructor env qid with
-  | ArgVar (_, id) -> GPatVar (Name id)
-  | ArgArg (_, kn) -> GPatRef (kn, [])
-  end
+| CPatVar (_, na) -> GPatVar na
 | CPatRef (_, qid, pl) ->
-  begin match get_constructor env qid with
-  | ArgVar (loc, id) ->
-    user_err ?loc (str "Unbound constructor " ++ Nameops.pr_id id)
-  | ArgArg (_, kn) -> GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
-  end
+  let (_, kn) = get_constructor env qid in
+  GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
 | CPatTup (_, pl) ->
   GPatTup (List.map (fun p -> intern_patexpr env p) pl)
 
@@ -603,10 +592,6 @@ let get_pattern_kind env pl = match pl with
 
 (** Internalization *)
 
-let is_constructor env qid = match get_variable env qid with
-| ArgArg (TacConstructor _) -> true
-| _ -> false
-
 (** Used to generate a fresh tactic variable for pattern-expansion *)
 let fresh_var env =
   let bad id =
@@ -617,18 +602,19 @@ let fresh_var env =
 
 let rec intern_rec env = function
 | CTacAtm (_, atm) -> intern_atm env atm
-| CTacRef qid as e ->
+| CTacRef qid ->
   begin match get_variable env qid with
   | ArgVar (_, id) ->
     let sch = Id.Map.find id env.env_var in
     (GTacVar id, fresh_mix_type_scheme env sch)
-  | ArgArg (TacConstant kn) ->
+  | ArgArg kn ->
     let (_, _, sch) = Tac2env.interp_global kn in
     (GTacRef kn, fresh_type_scheme env sch)
-  | ArgArg (TacConstructor kn) ->
-    let loc = loc_of_tacexpr e in
-    intern_constructor env loc kn []
   end
+| CTacCst qid as e ->
+  let loc = loc_of_tacexpr e in
+  let (_, kn) = get_constructor env qid in
+  intern_constructor env loc kn []
 | CTacFun (loc, bnd, e) ->
   let fold (env, bnd, tl) (pat, t) =
     let t = match t with
@@ -651,11 +637,8 @@ let rec intern_rec env = function
   let (e, t) = intern_rec env e in
   let t = List.fold_left (fun accu t -> GTypArrow (t, accu)) t tl in
   (GTacFun (bnd, e), t)
-| CTacApp (loc, CTacRef qid, args) as e when is_constructor env qid ->
-  let kn = match get_variable env qid with
-  | ArgArg (TacConstructor kn) -> kn
-  | _ -> assert false
-  in
+| CTacApp (loc, CTacCst qid, args) as e ->
+  let (_, kn) = get_constructor env qid in
   let loc = loc_of_tacexpr e in
   intern_constructor env loc kn args
 | CTacApp (loc, f, args) ->
@@ -823,7 +806,7 @@ and intern_let_rec env loc el e =
     to depth-one where leaves are either variables or catch-all *)
 and intern_case env loc e pl =
   let (e', t) = intern_rec env e in
-  let todo ~loc () = user_err ~loc (str "Pattern not handled yet") in
+  let todo ?loc () = user_err ?loc (str "Pattern not handled yet") in
   match get_pattern_kind env pl with
   | PKind_any ->
     let (pat, b) = List.hd pl in
@@ -848,12 +831,7 @@ and intern_case env loc e pl =
       (GTacCse (e', GCaseAlg t_unit, [|b|], [||]), tb)
     | [CPatTup (_, pl), b] ->
       let map = function
-      | CPatAny _ -> Anonymous
-      | CPatRef (loc, qid, []) ->
-        begin match get_constructor env qid with
-        | ArgVar (_, id) -> Name id
-        | ArgArg _ -> todo ~loc ()
-        end
+      | CPatVar (_, na) -> na
       | p -> todo ~loc:(loc_of_patexpr p) ()
       in
       let ids = List.map map pl in
@@ -885,7 +863,8 @@ and intern_case env loc e pl =
     | [] -> ()
     | (pat, br) :: rem ->
       let tbr = match pat with
-      | CPatAny _ ->
+      | CPatVar (loc, Name _) -> todo ?loc ()
+      | CPatVar (_, Anonymous) ->
         let () = check_redundant_clause rem in
         let (br', brT) = intern_rec env br in
         (** Fill all remaining branches *)
@@ -906,23 +885,14 @@ and intern_case env loc e pl =
         let _ = List.fold_left fill (0, 0) cstrs in
         brT
       | CPatRef (loc, qid, args) ->
-        let data = match get_constructor env qid with
-        | ArgVar _ -> todo ~loc ()
-        | ArgArg (data, _) ->
-          let () =
-            let kn' = data.cdata_type in
-            if not (KerName.equal kn kn') then
-              invalid_pattern ~loc kn (GCaseAlg kn')
-          in
-          data
+        let (data, _) = get_constructor env qid in
+        let () =
+          let kn' = data.cdata_type in
+          if not (KerName.equal kn kn') then
+            invalid_pattern ~loc kn (GCaseAlg kn')
         in
         let get_id = function
-        | CPatAny _ -> Anonymous
-        | CPatRef (loc, qid, []) ->
-          begin match get_constructor env qid with
-          | ArgVar (_, id) -> Name id
-          | ArgArg _ -> todo ~loc ()
-          end
+        | CPatVar (_, na) -> na
         | p -> todo ~loc:(loc_of_patexpr p) ()
         in
         let ids = List.map get_id args in
@@ -1165,12 +1135,9 @@ let get_projection0 var = match var with
 | AbsKn kn -> kn
 
 let rec ids_of_pattern accu = function
-| CPatAny _ -> accu
-| CPatRef (_, RelId (_, qid), pl) ->
-  let (dp, id) = repr_qualid qid in
-  let accu = if DirPath.is_empty dp then Id.Set.add id accu else accu in
-  List.fold_left ids_of_pattern accu pl
-| CPatRef (_, AbsKn _, pl) ->
+| CPatVar (_, Anonymous) -> accu
+| CPatVar (_, Name id) -> Id.Set.add id accu
+| CPatRef (_, _, pl) ->
   List.fold_left ids_of_pattern accu pl
 | CPatTup (_, pl) ->
   List.fold_left ids_of_pattern accu pl
@@ -1183,6 +1150,9 @@ let rec globalize ids e = match e with
   | ArgVar _ -> e
   | ArgArg kn -> CTacRef (AbsKn kn)
   end
+| CTacCst qid ->
+  let (_, knc) = get_constructor () qid in
+  CTacCst (AbsKn knc)
 | CTacFun (loc, bnd, e) ->
   let fold (pats, accu) (pat, t) =
     let accu = ids_of_pattern accu pat in
@@ -1252,12 +1222,10 @@ and globalize_case ids (p, e) =
   (globalize_pattern ids p, globalize ids e)
 
 and globalize_pattern ids p = match p with
-| CPatAny _ -> p
+| CPatVar _ -> p
 | CPatRef (loc, cst, pl) ->
-  let cst = match get_constructor () cst with
-  | ArgVar _ -> cst
-  | ArgArg (_, knc) -> AbsKn knc
-  in
+  let (_, knc) = get_constructor () cst in
+  let cst = AbsKn knc in
   let pl = List.map (fun p -> globalize_pattern ids p) pl in
   CPatRef (loc, cst, pl)
 | CPatTup (loc, pl) ->
@@ -1393,12 +1361,9 @@ let rec subst_rawtype subst t = match t with
 
 let subst_tacref subst ref = match ref with
 | RelId _ -> ref
-| AbsKn (TacConstant kn) ->
-  let kn' = subst_kn subst kn in
-  if kn' == kn then ref else AbsKn (TacConstant kn')
-| AbsKn (TacConstructor kn) ->
+| AbsKn kn ->
   let kn' = subst_kn subst kn in
-  if kn' == kn then ref else AbsKn (TacConstructor kn')
+  if kn' == kn then ref else AbsKn kn'
 
 let subst_projection subst prj = match prj with
 | RelId _ -> prj
@@ -1407,7 +1372,7 @@ let subst_projection subst prj = match prj with
   if kn' == kn then prj else AbsKn kn'
 
 let rec subst_rawpattern subst p = match p with
-| CPatAny _ -> p
+| CPatVar _ -> p
 | CPatRef (loc, c, pl) ->
   let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in
   let c' = match c with
@@ -1427,6 +1392,9 @@ let rec subst_rawexpr subst t = match t with
 | CTacRef ref ->
   let ref' = subst_tacref subst ref in
   if ref' == ref then t else CTacRef ref'
+| CTacCst ref ->
+  let ref' = subst_tacref subst ref in
+  if ref' == ref then t else CTacCst ref'
 | CTacFun (loc, bnd, e) ->
   let map (na, t as p) =
     let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
diff --git a/src/tac2print.ml b/src/tac2print.ml
index e6f0582e3d..2afcfb4a6e 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -83,7 +83,7 @@ let int_name () =
 (** Term printing *)
 
 let pr_constructor kn =
-  Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstructor kn))
+  Libnames.pr_qualid (Tac2env.shortest_qualid_of_constructor kn)
 
 let pr_projection kn =
   Libnames.pr_qualid (Tac2env.shortest_qualid_of_projection kn)
@@ -138,7 +138,7 @@ let pr_glbexpr_gen lvl c =
   | GTacAtm atm -> pr_atom atm
   | GTacVar id -> Id.print id
   | GTacRef gr ->
-    let qid = shortest_qualid_of_ltac (TacConstant gr) in
+    let qid = shortest_qualid_of_ltac gr in
     Libnames.pr_qualid qid
   | GTacFun (nas, c) ->
     let nas = pr_sequence pr_name nas in