diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-22 16:45:35 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-22 16:45:35 +0000 |
| commit | 1cc5c0da0b5335c8773efd27e678178ef5e9c5f1 (patch) | |
| tree | 67feba4f2ab227bec5cdbee24f936046d40b1dcf /tactics | |
| parent | 8646837a56962c9319d7fd428a72223b947ac141 (diff) | |
Fix bug# 2994, 2971 about better error messages.
Fix bug# 2956, porting fix from 8.4 branch
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16349 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index a3006e99c..ad8517c32 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -142,11 +142,14 @@ let build_signature evars env m (cstrs : (types * types option) option list) new_cstr_evar evars env (* ~src:(Loc.ghost, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t in - let mk_relty evars env ty obj = + let mk_relty evars newenv ty obj = match obj with | None | Some (_, None) -> let relty = mk_relation ty in - new_evar evars env relty + if closed0 ty then + let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in + new_evar evars env' relty + else new_evar evars newenv relty | Some (x, Some rel) -> evars, rel in let rec aux env evars ty l = @@ -484,7 +487,7 @@ let rec apply_pointwise rel = function | [] -> rel let pointwise_or_dep_relation n t car rel = - if noccurn 1 car then + if noccurn 1 car && noccurn 1 rel then mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |]) else mkApp (Lazy.force forall_relation, |