Ltac now uses evar-based constrs.

10 files changed, 24 insertions, 29 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 102efe55b..0a980c03b 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -497,10 +497,10 @@ let rec inst_pattern subst = function
 	   args t
 
 let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
-  Termops.print_constr (constr_of_term (term uf i)) ++ str "]"
+  Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
 
 let pr_term t = str "[" ++
-  Termops.print_constr (constr_of_term t) ++ str "]"
+  Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
 
 let rec add_term state t=
   let uf=state.uf in
@@ -615,7 +615,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
@@ -623,7 +623,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a4ed4798a..62892973d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -414,6 +414,7 @@ let build_term_to_complete uf meta pac =
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library Coqlib.logic_module_name;
     let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
     let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
@@ -448,7 +449,7 @@ let cc_tactic depth additionnal_terms =
 		   str "\"congruence with (" ++
 		     prlist_with_sep
 		     (fun () -> str ")" ++ spc () ++ str "(")
-		     (EConstr.Unsafe.to_constr %> Termops.print_constr_env env)
+		     (Termops.print_constr_env env sigma)
 		     terms_to_complete ++
 		     str ")\","
 		 end ++
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index b787e824f..6f6811334 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -18,9 +18,9 @@ DECLARE PLUGIN "cc_plugin"
 TACTIC EXTEND cc
  [ "congruence" ] -> [ congruence_tac 1000 [] ]
  |[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 (List.map EConstr.of_constr l) ]
+ |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
  |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
-   [ congruence_tac n (List.map EConstr.of_constr l) ]
+   [ congruence_tac n l ]
 END
 
 TACTIC EXTEND f_equal
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 59a0bb5a2..93b98263e 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -206,6 +206,8 @@ let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) =
      instr
 
 let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) =
+  let pconstr1 c = pconstr1 (EConstr.of_constr c) in
+  let pconstr2 c = pconstr2 (EConstr.of_constr c) in
   pr_gen_proof_instr
     (fun st -> pr_statement pconstr1 st)
     pconstr2
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index a6f971703..560242bf2 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -58,7 +58,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
     | None -> mt ()
     | Some b ->
       let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
-      spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed (EConstr.Unsafe.to_constr %> prc) (EConstr.Unsafe.to_constr %> prlc) b)
+      spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b)
 
 
 ARGUMENT EXTEND fun_ind_using
@@ -108,8 +108,9 @@ TACTIC EXTEND newfunind
        let c = match cl with
 	 | [] -> assert false
 	 | [c] -> c
-	 | c::cl -> applist(c,cl)
+	 | c::cl -> EConstr.applist(c,cl)
        in
+       let c = EConstr.Unsafe.to_constr c in
        Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ]
 END
 (***** debug only ***)
@@ -119,8 +120,9 @@ TACTIC EXTEND snewfunind
        let c = match cl with
 	 | [] -> assert false
 	 | [c] -> c
-	 | c::cl -> applist(c,cl)
+	 | c::cl -> EConstr.applist(c,cl)
        in
+       let c = EConstr.Unsafe.to_constr c in
        Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ]
 END
 
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 5f906a8da..a6749c347 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -13,5 +13,5 @@ DECLARE PLUGIN "nsatz_plugin"
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute"  constr(lt) ] -> [ Nsatz.nsatz_compute lt ]
+| [ "nsatz_compute"  constr(lt) ] -> [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ]
 END
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 79c429615..40c1028e5 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -23,7 +23,6 @@ let cont = Id.of_string "cont"
 let x = Id.of_string "x"
 
 let make_cont (k : Val.t) (c : EConstr.t) =
-  let c = EConstr.Unsafe.to_constr c in
   let c = Tacinterp.Value.of_constr c in
   let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in
   let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
@@ -33,8 +32,8 @@ TACTIC EXTEND quote
   [ "quote" ident(f) ] -> [ quote f [] ]
 | [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
 | [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] ->
-  [ gen_quote (make_cont k) (EConstr.of_constr c) f [] ]
+  [ gen_quote (make_cont k) c f [] ]
 | [ "quote" ident(f) "[" ne_ident_list(lc) "]"
     "in" constr(c) "using" tactic(k) ] ->
-  [ gen_quote (make_cont k) (EConstr.of_constr c) f lc ]
+  [ gen_quote (make_cont k) c f lc ]
 END
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 13cf8330b..b1882ae8a 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -30,7 +30,7 @@ END
 
 TACTIC EXTEND closed_term
   [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
-    [ closed_term (EConstr.of_constr t) l ]
+    [ closed_term t l ]
 END
 
 open Pptactic
@@ -90,11 +90,7 @@ END
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
-    [
-      let lH = List.map EConstr.of_constr lH in
-      let lrt = List.map EConstr.of_constr lrt in
-      let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t
-    ]
+    [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t ]
 END
 
 let pr_field_mod = function
@@ -129,9 +125,5 @@ END
 
 TACTIC EXTEND field_lookup
 | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
-      [
-        let lH = List.map EConstr.of_constr lH in
-        let lt = List.map EConstr.of_constr lt in
-        let (t,l) = List.sep_last lt in field_lookup f lH l t
-      ]
+      [ let (t,l) = List.sep_last lt in field_lookup f lH l t ]
 END
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index c0eeff8d7..ce2c558ae 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -183,7 +183,7 @@ let dummy_goal env sigma =
   {Evd.it = gl; Evd.sigma = sigma}
 
 let constr_of v = match Value.to_constr v with
-  | Some c -> c
+  | Some c -> EConstr.Unsafe.to_constr c
   | None -> failwith "Ring.exec_tactic: anomaly"
 
 let tactic_res = ref [||]
@@ -203,7 +203,6 @@ let get_res =
 
 let exec_tactic env evd n f args =
   let fold arg (i, vars, lfun) =
-    let arg = EConstr.Unsafe.to_constr arg in
     let id = Id.of_string ("x" ^ string_of_int i) in
     let x = Reference (ArgVar (Loc.ghost, id)) in
     (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun)
@@ -730,7 +729,7 @@ let make_term_list env evd carrier rl =
     (plapp evd coq_nil [|carrier|])
   in Typing.e_solve_evars env evd l
 
-let carg = Tacinterp.Value.of_constr
+let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
 let tacarg expr =
   Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 9798fa11c..9dcc6c4cc 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1030,7 +1030,7 @@ let interp_constr = interp_wit wit_constr
 let interp_open_constr ist gl gc =
   interp_wit wit_open_constr ist gl gc
 let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
-let interp_term ist gl (_, c) = (interp_open_constr ist gl c)
+let interp_term ist gl (_, c) = on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c)
 let pr_ssrterm _ _ _ = pr_term
 let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with
   | Tok.KEYWORD "(" -> '('