diff options
| author | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
| commit | 4bb062f4a66c4ae5a1742e7d99fdc335de0d57a9 (patch) | |
| tree | af8ead1cdc5af3842e683f602177ab4fa2dec9b5 /tactics | |
| parent | 1be9c4da4d814c29d4ba45b121fda924adc1130e (diff) | |
| parent | 29ba692f0fd25ce87392bbb7494cb62e3b97dc07 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 9289c6d663..ac8b4923e5 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -283,7 +283,7 @@ end) = struct (app_poly env evd arrow [| a; b |]), unfold_impl (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) - (app_poly env evd coq_all [| a; mkLambda (Anonymous, a, b) |]), unfold_forall + (app_poly env evd coq_all [| a; mkLambda (Anonymous, a, lift 1 b) |]), unfold_forall else (* None in Prop, use arrow *) (app_poly env evd arrow [| a; b |]), unfold_impl @@ -1444,7 +1444,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let newt = Evarutil.nf_evar evars' res.rew_to in let evars = (* Keep only original evars (potentially instantiated) and goal evars, the rest has been defined and substituted already. *) - Evar.Set.fold (fun ev acc -> Evd.remove acc ev) cstrs evars' + Evar.Set.fold + (fun ev acc -> + if not (Evd.is_defined acc ev) then + errorlabstrm "rewrite" + (str "Unsolved constraint remaining: " ++ spc () ++ + Evd.pr_evar_info (Evd.find acc ev)) + else Evd.remove acc ev) + cstrs evars' in let res = match res.rew_prf with | RewCast c -> None |