diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-26 14:09:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-26 14:09:38 +0000 |
| commit | 76f02a4751c3eac40d91dfa7bb61de1f985672d3 (patch) | |
| tree | d1baeaf19b47abd61c9e7c1a65def7c4bdfe0632 /tactics | |
| parent | df78c17c0d1545f2ce37b6c2bb3521f0d2fb130b (diff) | |
Report correction bug #1289 dans trunk (r9435 pour branche v8.1)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9463 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 074ccadf9..aeb8b4e50 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -610,6 +610,7 @@ let cut_and_apply c gl = let goal_constr = pf_concl gl in match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> + let c2 = refresh_universes c2 in tclTHENLAST (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())]) (apply_term c [mkMeta (new_meta())]) gl @@ -966,7 +967,7 @@ let true_cut = assert_tac true (**************************) let generalize_goal gl c cl = - let t = pf_type_of gl c in + let t = refresh_universes (pf_type_of gl c) in match kind_of_term c with | Var id -> (* The choice of remembering or not a non dependent name has an impact |