diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-20 22:16:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:34 +0100 |
| commit | e09f3b44bb381854b647a6d9debdeddbfc49177e (patch) | |
| tree | e7ba5807fa369b912cb36fe50bba97d33f7af5b5 /proofs/tacmach.ml | |
| parent | d4b344acb23f19b089098b7788f37ea22bc07b81 (diff) | |
Proofview.Goal primitive now return EConstrs.
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index aa54e4f9b..f3f19e854 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -220,7 +220,7 @@ module New = struct let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = project gl in - nf_evar sigma concl + EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr concl)) let pf_whd_all gl t = pf_apply whd_all gl t @@ -229,13 +229,13 @@ module New = struct let pf_reduce_to_quantified_ind gl t = pf_apply reduce_to_quantified_ind gl t - let pf_hnf_constr gl t = pf_apply hnf_constr gl t + let pf_hnf_constr gl t = EConstr.of_constr (pf_apply hnf_constr gl t) let pf_hnf_type_of gl t = - pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)) + EConstr.of_constr (pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t + let pf_whd_all gl t = EConstr.of_constr (pf_apply whd_all gl t) let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t |