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

1 files changed, 4 insertions, 2 deletions

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 *)