From b00cb9ccbb02e2aa913294887749fff79b0adad5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 10 Mar 2008 10:22:45 +0000
Subject: Une passe sur l'unification des evars (suite aux commits 10124,
 10125, 10145) - Correction bug des filtres dans define_evar_as_abstraction -
 Nettoyage, documentation et réorganisations diverses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10650 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 9573f54382..154f8481aa 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -69,10 +69,12 @@ let with_check = Flags.with_option check
 (* The Clear tactic: it scans the context for hypotheses to be removed
    (instead of iterating on the list of identifier to be removed, which
    forces the user to give them in order). *)
+
 let clear_hyps sigma ids gl =
   let evdref = ref (Evd.create_goal_evar_defs sigma) in
-  let ngl = Evarutil.clear_hyps_in_evi evdref gl ids in
-    (ngl, evars_of !evdref)
+  let (hyps,concl) =
+    Evarutil.clear_hyps_in_evi evdref gl.evar_hyps gl.evar_concl ids in
+    (mk_goal hyps concl gl.evar_extra, evars_of !evdref)
 
 (* The ClearBody tactic *)
 
-- 
cgit v1.2.3