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.

---
 pretyping/evarutil.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping/evarutil.ml')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index cfbff80a9d..f02d7623df 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -21,6 +21,8 @@ open Evd
 open Reductionops
 open Pretype_errors
 
+(** Combinators *)
+
 let evd_comb0 f evdref =
   let (evd',x) = f !evdref in
     evdref := evd';
@@ -472,7 +474,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 		ctxt (Array.to_list l) (Id.Map.empty,[]) in
 	    (* Check if some rid to clear in the context of ev has dependencies
 	       in the type of ev and adjust the source of the dependency *)
-	    let nconcl =
+	    let _nconcl =
 	      try
                 let nids = Id.Map.domain rids in
                 check_and_clear_in_constr evdref (EvarTypingBreak ev) nids (evar_concl evi)
-- 
cgit v1.2.3