From e6a8ab0f428c26fff2bd7e636126974f167101bf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 20 Nov 2016 01:35:54 +0100
Subject: Tactic_matching API using EConstr.

---
 dev/top_printers.ml           |  2 +-
 intf/pattern.mli              |  4 ++--
 ltac/taccoerce.ml             |  9 +++++----
 ltac/taccoerce.mli            |  4 ++--
 ltac/tacinterp.ml             | 14 +++++++++-----
 ltac/tactic_matching.ml       | 18 ++++++++++--------
 ltac/tactic_matching.mli      |  8 ++++----
 plugins/quote/quote.ml        |  2 +-
 pretyping/constr_matching.ml  | 11 +++++------
 pretyping/constr_matching.mli |  2 +-
 pretyping/detyping.ml         |  1 +
 pretyping/patternops.ml       |  4 +++-
 pretyping/pretyping.ml        |  2 +-
 printing/printer.ml           |  2 +-
 tactics/auto.ml               |  2 +-
 tactics/hipattern.ml          | 11 +++--------
 tactics/tactics.ml            |  1 -
 17 files changed, 50 insertions(+), 47 deletions(-)

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b7736f498..8290ca945 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -109,7 +109,7 @@ let ppididmap = ppidmap (fun _ -> pr_id)
 
 let prconstrunderbindersidmap = pridmap (fun _ (l,c) ->
   hov 1 (str"[" ++  prlist_with_sep spc Id.print l ++ str"]")
-  ++ str "," ++ spc () ++ Termops.print_constr c)
+  ++ str "," ++ spc () ++ Termops.print_constr (EConstr.Unsafe.to_constr c))
 
 let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
 
diff --git a/intf/pattern.mli b/intf/pattern.mli
index 329ae837e..ac84b91e6 100644
--- a/intf/pattern.mli
+++ b/intf/pattern.mli
@@ -43,11 +43,11 @@ open Misctypes
     could be inferred. We also loose the ability of typing ltac
     variables before calling the right-hand-side of ltac matching clauses. *)
 
-type constr_under_binders = Id.t list * constr
+type constr_under_binders = Id.t list * EConstr.constr
 
 (** Types of substitutions with or w/o bound variables *)
 
-type patvar_map = constr Id.Map.t
+type patvar_map = EConstr.constr Id.Map.t
 type extended_patvar_map = constr_under_binders Id.Map.t
 
 (** {5 Patterns} *)
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
index df38a42cb..288e12d0b 100644
--- a/ltac/taccoerce.ml
+++ b/ltac/taccoerce.ml
@@ -17,7 +17,7 @@ open Geninterp
 
 exception CannotCoerceTo of string
 
-let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
+let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_context" in
   let () = register_val0 wit None in
   wit
@@ -64,7 +64,7 @@ let to_constr v =
     Some c
   else if has_type v (topwit wit_constr_under_binders) then
     let vars, c = out_gen (topwit wit_constr_under_binders) v in
-    match vars with [] -> Some c | _ -> None
+    match vars with [] -> Some (EConstr.Unsafe.to_constr c) | _ -> None
   else None
 
 let of_uconstr c = in_gen (topwit wit_uconstr) c
@@ -96,7 +96,7 @@ let is_variable env id =
 
 (* Transforms an id into a constr if possible, or fails with Not_found *)
 let constr_of_id env id =
-  Term.mkVar (let _ = Environ.lookup_named id env in id)
+  EConstr.mkVar (let _ = Environ.lookup_named id env in id)
 
 (* Gives the constr corresponding to a Constr_context tactic_arg *)
 let coerce_to_constr_context v =
@@ -212,7 +212,7 @@ let coerce_to_constr env v =
     | _ -> fail ()
   else if has_type v (topwit wit_constr) then
     let c = out_gen (topwit wit_constr) v in
-    ([], c)
+    ([], EConstr.of_constr c)
   else if has_type v (topwit wit_constr_under_binders) then
     out_gen (topwit wit_constr_under_binders) v
   else if has_type v (topwit wit_var) then
@@ -229,6 +229,7 @@ let coerce_to_uconstr env v =
 
 let coerce_to_closed_constr env v =
   let ids,c = coerce_to_constr env v in
+  let c = EConstr.Unsafe.to_constr c in
   let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
   c
 
diff --git a/ltac/taccoerce.mli b/ltac/taccoerce.mli
index 0b67f8726..3049aff7e 100644
--- a/ltac/taccoerce.mli
+++ b/ltac/taccoerce.mli
@@ -48,7 +48,7 @@ end
 
 (** {5 Coercion functions} *)
 
-val coerce_to_constr_context : Value.t -> constr
+val coerce_to_constr_context : Value.t -> EConstr.constr
 
 val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t
 
@@ -91,6 +91,6 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list
 
 (** {5 Missing generic arguments} *)
 
-val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type
+val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type
 
 val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 553565639..d2fb2614e 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -239,7 +239,7 @@ let pr_value env v =
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
     match env with
-    | Some (env,sigma) -> pr_lconstr_env env sigma c
+    | Some (env,sigma) -> pr_lconstr_env env sigma (EConstr.Unsafe.to_constr c)
     | _ -> str "a term"
   else if has_type v (topwit wit_constr) then
     let c = out_gen (topwit wit_constr) v in
@@ -334,7 +334,7 @@ let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2
 
 let extend_values_with_bindings (ln,lm) lfun =
   let of_cub c = match c with
-  | [], c -> Value.of_constr c
+  | [], c -> Value.of_constr (EConstr.Unsafe.to_constr c)
   | _ -> in_gen (topwit wit_constr_under_binders) c
   in
   (* For compatibility, bound variables are visible only if no other
@@ -790,6 +790,7 @@ let interp_may_eval f ist env sigma = function
       (try
 	let (sigma,ic) = f ist env sigma c in
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
+	let ctxt = EConstr.Unsafe.to_constr ctxt in
 	let evdref = ref sigma in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
 	let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
@@ -860,6 +861,7 @@ let rec message_of_value v =
     end }
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
+    let c = EConstr.Unsafe.to_constr c in
     Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (project gl) c) end }
   else if has_type v (topwit wit_uconstr) then
     let c = out_gen (topwit wit_uconstr) v in
@@ -1464,7 +1466,7 @@ and interp_letin ist llc u =
 and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
   let (>>=) = Ftactic.bind in
   let lctxt = Id.Map.map interp_context context in
-  let hyp_subst = Id.Map.map Value.of_constr terms in
+  let hyp_subst = Id.Map.map (EConstr.Unsafe.to_constr %> Value.of_constr) terms in
   let lfun = extend_values_with_bindings subst (lctxt +++ hyp_subst +++ ist.lfun) in
   let ist = { ist with lfun } in
   val_interp ist lhs >>= fun v ->
@@ -1518,6 +1520,7 @@ and interp_match ist lz constr lmr =
           Proofview.tclZERO ~info e
     end
   end >>= fun constr ->
+  let constr = EConstr.of_constr constr in
   Ftactic.enter { enter = begin fun gl ->
     let sigma = project gl in
     let env = Proofview.Goal.env gl in
@@ -1533,6 +1536,7 @@ and interp_match_goal ist lz lr lmr =
       let hyps = Proofview.Goal.hyps gl in
       let hyps = if lr then List.rev hyps else hyps in
       let concl = Proofview.Goal.concl gl in
+      let concl = EConstr.of_constr concl in
       let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
       interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr)
     end }
@@ -1844,7 +1848,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let c_interp patvars = { Sigma.run = begin fun sigma ->
 	  let lfun' = Id.Map.fold (fun id c lfun ->
-	    Id.Map.add id (Value.of_constr c) lfun) 
+	    Id.Map.add id (Value.of_constr (EConstr.Unsafe.to_constr c)) lfun) 
 	    patvars ist.lfun
 	  in
 	  let sigma = Sigma.to_evar_map sigma in
@@ -1871,7 +1875,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
         let c_interp patvars = { Sigma.run = begin fun sigma ->
           let lfun' = Id.Map.fold (fun id c lfun ->
-            Id.Map.add id (Value.of_constr c) lfun) 
+            Id.Map.add id (Value.of_constr (EConstr.Unsafe.to_constr c)) lfun) 
             patvars ist.lfun
           in
           let ist = { ist with lfun = lfun' } in
diff --git a/ltac/tactic_matching.ml b/ltac/tactic_matching.ml
index 58998c96e..ac64f0bba 100644
--- a/ltac/tactic_matching.ml
+++ b/ltac/tactic_matching.ml
@@ -23,8 +23,8 @@ module NamedDecl = Context.Named.Declaration
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
   subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
-  context : Term.constr Id.Map.t;
-  terms : Term.constr Id.Map.t;
+  context : EConstr.constr Id.Map.t;
+  terms : EConstr.constr Id.Map.t;
   lhs : 'a;
 }
 
@@ -84,7 +84,7 @@ let equal_instances env sigma (ctx',c') (ctx,c) =
   (* How to compare instances? Do we want the terms to be convertible?
      unifiable? Do we want the universe levels to be relevant? 
      (historically, conv_x is used) *)
-  CList.equal Id.equal ctx ctx' && Reductionops.is_conv env sigma (EConstr.of_constr c') (EConstr.of_constr c)
+  CList.equal Id.equal ctx ctx' && Reductionops.is_conv env sigma c' c
 
 
 (** Merges two substitutions. Raises [Not_coherent_metas] when
@@ -233,7 +233,7 @@ module PatternMatching (E:StaticEnvironment) = struct
     | Term p ->
         begin 
           try
-            put_subst (Constr_matching.extended_matches E.env E.sigma p (EConstr.of_constr term)) <*>
+            put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*>
             return lhs
           with Constr_matching.PatternMatchingFailure -> fail
         end
@@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct
             | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
         }
       in
-      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p (EConstr.of_constr term)) imatching_error
+      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
 
 
   (** [rule_match_term term rule] matches the term [term] with the
@@ -284,8 +284,8 @@ module PatternMatching (E:StaticEnvironment) = struct
     pick hyps >>= fun decl ->
     let id = NamedDecl.get_id decl in
     let refresh = is_local_def decl in
-    pattern_match_term refresh pat (NamedDecl.get_type decl) () <*>
-    put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+    pattern_match_term refresh pat (EConstr.of_constr (NamedDecl.get_type decl)) () <*>
+    put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*>
     return id
 
   (** [hyp_match_type hypname bodypat typepat hyps] matches a single
@@ -295,9 +295,11 @@ module PatternMatching (E:StaticEnvironment) = struct
   let hyp_match_body_and_type hypname bodypat typepat hyps =
     pick hyps >>= function
       | LocalDef (id,body,hyp) ->
+          let body = EConstr.of_constr body in
+          let hyp = EConstr.of_constr hyp in
           pattern_match_term false bodypat body () <*>
           pattern_match_term true typepat hyp () <*>
-          put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+          put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*>
           return id
       | LocalAssum (id,hyp) -> fail
 
diff --git a/ltac/tactic_matching.mli b/ltac/tactic_matching.mli
index 090207bcc..d6f67d6c7 100644
--- a/ltac/tactic_matching.mli
+++ b/ltac/tactic_matching.mli
@@ -18,8 +18,8 @@
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
   subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
-  context : Term.constr Names.Id.Map.t;
-  terms : Term.constr Names.Id.Map.t;
+  context : EConstr.constr Names.Id.Map.t;
+  terms : EConstr.constr Names.Id.Map.t;
   lhs : 'a;
 }
 
@@ -31,7 +31,7 @@ type 'a t = {
 val match_term :
   Environ.env ->
   Evd.evar_map ->
-  Term.constr ->
+  EConstr.constr ->
   (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
 
@@ -44,6 +44,6 @@ val match_goal:
   Environ.env ->
   Evd.evar_map ->
   Context.Named.t ->
-  Term.constr ->
+  EConstr.constr ->
   (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 2cc402e28..09e77598a 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -403,7 +403,7 @@ let quote_terms ivs lc =
         | (lhs, rhs)::tail ->
             begin try
               let s1 = Id.Map.bindings (matches (Global.env ()) Evd.empty rhs (EConstr.of_constr c)) in
-              let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1
+              let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux (EConstr.Unsafe.to_constr c_i))) s1
 	      in
               Termops.subst_meta s2 lhs
             with PatternMatchingFailure -> auxl tail
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 4d2500ccd..06daa5116 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -16,6 +16,7 @@ open Nameops
 open Termops
 open Reductionops
 open Term
+open EConstr
 open Vars
 open Pattern
 open Patternops
@@ -61,11 +62,11 @@ let constrain sigma n (ids, m) (names, terms as subst) =
   let open EConstr in
   try
     let (ids', m') = Id.Map.find n terms in
-    if List.equal Id.equal ids ids' && eq_constr sigma m (EConstr.of_constr m') then subst
+    if List.equal Id.equal ids ids' && eq_constr sigma m m' then subst
     else raise PatternMatchingFailure
   with Not_found ->
     let () = if Id.Map.mem n names then warn_meta_collision n in
-    (names, Id.Map.add n (ids, EConstr.Unsafe.to_constr m) terms)
+    (names, Id.Map.add n (ids, m) terms)
 
 let add_binders na1 na2 binding_vars (names, terms as subst) =
   match na1, na2 with
@@ -152,7 +153,6 @@ let merge_binding sigma allow_bound_rels ctx n cT subst =
   | [] -> (* Optimization *)
     ([], cT)
   | _ ->
-    let open EConstr in
     let frels = free_rels sigma cT in
     if allow_bound_rels then
       let vars = extract_bound_vars frels ctx in
@@ -344,7 +344,7 @@ type matching_result =
     { m_sub : bound_ident_map * patvar_map;
       m_ctx : constr; }
 
-let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=EConstr.Unsafe.to_constr c; } , (IStream.thunk n) )
+let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )
 
 let isPMeta = function PMeta _ -> true | _ -> false
 
@@ -362,10 +362,9 @@ let matches_head env sigma pat c =
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
 let authorized_occ env sigma partial_app closed pat c mk_ctx =
-  let open EConstr in
   try
     let subst = matches_core_closed env sigma false partial_app pat c in
-    if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst)
+    if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
     then (fun next -> next ())
     else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
   with PatternMatchingFailure -> (fun next -> next ())
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 32bb48c93..4734c90a8 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -64,7 +64,7 @@ val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
    (whose hole is denoted here with [special_meta]) *)
 type matching_result =
     { m_sub : bound_ident_map * patvar_map;
-      m_ctx : Constr.t }
+      m_ctx : EConstr.t }
 
 (** [match_subterm n pat c] returns the substitution and the context
    corresponding to each **closed** subterm of [c] matching [pat]. *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ec8945e85..c0611dcec 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -745,6 +745,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
         with Not_found -> try
           (* assumes [detype] does not raise [Not_found] exceptions *)
           let (b,c) = Id.Map.find id cl.typed in
+          let c = EConstr.Unsafe.to_constr c in
           (* spiwack: I'm not sure it is the right thing to do,
              but I'm computing the detyping environment like
              [Printer.pr_constr_under_binders_env] does. *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ffd6e73fa..26e23be23 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -224,6 +224,8 @@ let error_instantiate_pattern id l =
     ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
 let instantiate_pattern env sigma lvar c =
+  let open EConstr in
+  let open Vars in
   let rec aux vars = function
   | PVar id as x ->
       (try
@@ -235,7 +237,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  pattern_of_constr env sigma (EConstr.of_constr c)
+	  pattern_of_constr env sigma c
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 11d50926f..c792bf2ca 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -445,7 +445,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
     try
       let (ids,c) = Id.Map.find id lvar.ltac_constrs in
       let subst = List.map (invert_ltac_bound_name lvar env id) ids in
-      let c = substl subst (EConstr.of_constr c) in
+      let c = substl subst c in
 	{ uj_val = c; uj_type = protected_get_type_of env sigma c }
     with Not_found -> try
        let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in
diff --git a/printing/printer.ml b/printing/printer.ml
index ed6ebdc9b..2a30681bf 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -76,7 +76,7 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
   (* we also need to preserve the actual names of the patterns *)
   (* So what to do? *)
   let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
-  pr (Termops.push_rels_assum assums env) sigma c
+  pr (Termops.push_rels_assum assums env) sigma (EConstr.Unsafe.to_constr c)
 
 let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
 let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
diff --git a/tactics/auto.ml b/tactics/auto.ml
index c34f9dd92..21fe9667b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -152,7 +152,7 @@ let conclPattern concl pat tac =
      let open Genarg in
      let open Geninterp in
      let inj c = match val_tag (topwit Stdarg.wit_constr) with
-     | Val.Base tag -> Val.Dyn (tag, c)
+     | Val.Base tag -> Val.Dyn (tag, EConstr.Unsafe.to_constr c)
      | _ -> assert false
      in
      let fold id c accu = Id.Map.add id (inj c) accu in
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 9e78ff323..b92d65908 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -353,8 +353,6 @@ let is_imp_term sigma c = op2bool (match_with_imp_term sigma c)
 let match_with_nottype sigma t =
   try
     let (arg,mind) = match_arrow_pattern sigma t in
-    let arg = EConstr.of_constr arg in
-    let mind = EConstr.of_constr mind in
     if is_empty_type sigma mind then Some (mind,arg) else None
   with PatternMatchingFailure -> None
 
@@ -470,11 +468,11 @@ let match_eq_nf gls eqn (ref, hetero) =
   let n = if hetero then 4 else 3 in
   let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in
   let pat = mkPattern (mkGAppRef ref args) in
-  let pf_whd_all gls c = EConstr.of_constr (pf_whd_all gls (EConstr.of_constr c)) in
+  let pf_whd_all gls c = EConstr.of_constr (pf_whd_all gls c) in
   match Id.Map.bindings (pf_matches gls pat eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
-	(EConstr.of_constr t,pf_whd_all gls x,pf_whd_all gls y)
+	(t,pf_whd_all gls x,pf_whd_all gls y)
     | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
 
 let dest_nf_eq gls eqn =
@@ -502,7 +500,7 @@ let coq_sig_pattern =
 
 let match_sigma sigma t =
   match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with
-    | [(_,a); (_,p)] -> (EConstr.of_constr a,EConstr.of_constr p)
+    | [(_,a); (_,p)] -> (a,p)
     | _ -> anomaly (Pp.str "Unexpected pattern")
 
 let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t
@@ -548,9 +546,6 @@ let match_eqdec sigma t =
         false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in
   match Id.Map.bindings subst with
   | [(_,typ);(_,c1);(_,c2)] ->
-      let typ = EConstr.of_constr typ in
-      let c1 = EConstr.of_constr c1 in
-      let c2 = EConstr.of_constr c2 in
       eqonleft, EConstr.of_constr (Universes.constr_of_global (Lazy.force op)), c1, c2, typ
   | _ -> anomaly (Pp.str "Unexpected pattern")
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c025ca9b5..606eb27b9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -816,7 +816,6 @@ let e_change_in_hyp redfun (id,where) =
 type change_arg = Pattern.patvar_map -> EConstr.constr Sigma.run
 
 let make_change_arg c pats =
-  let pats = Id.Map.map EConstr.of_constr pats in
   { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma }
 
 let check_types env sigma mayneedglobalcheck deep newc origc =
-- 
cgit v1.2.3