From c5ecebf6fefbaa673dda506175a2aa4a69d79807 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Sep 2014 00:03:46 +0200
Subject: Revert specific syntax for primitive projections, avoiding ugly
 contortions in internalization/externalization. It uses a fully typed version
 of detyping, requiring the environment, to move from primitive projection
 applications to regular applications of the eta-expanded version. The kernel
 is unchanged, and only constrMatching needs compatibility code now.

---
 tactics/extratactics.ml4 | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e4ba9a7ee5..41f8dc8dec 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -628,9 +628,8 @@ let hResolve id c occ t gl =
   let sigma = project gl in 
   let env = Termops.clear_named_body id (pf_env gl) in
   let env_ids = Termops.ids_of_context env in
-  let env_names = Termops.names_of_rel_context env in
-  let c_raw = Detyping.detype true env_ids env_names sigma c in
-  let t_raw = Detyping.detype true env_ids env_names sigma t in
+  let c_raw = Detyping.detype true env_ids env sigma c in
+  let t_raw = Detyping.detype true env_ids env sigma t in
   let rec resolve_hole t_hole =
     try 
       Pretyping.understand env sigma t_hole
-- 
cgit v1.2.3