From 78a8d59b39dfcb07b94721fdcfd9241d404905d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 15:30:02 +0100
Subject: Introducing contexts parameterized by the inner term type.

This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
---
 proofs/pfedit.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 142fd9a899..09b924c7e6 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -228,7 +228,7 @@ let solve_by_implicit_tactic env sigma evk =
   match (!implicit_tactic, snd (evar_source evk sigma)) with
   | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
       when
-	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
+	Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
       (try
-- 
cgit v1.2.3