diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index c5d6e3e08..829c96296 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -490,6 +490,7 @@ and mk_arggoals sigma goal goalacc funty allargs = and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in + let ct = EConstr.of_constr ct in let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let indspec = try Tacred.find_hnf_rectype env sigma ct |