diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 47b9b406d..c41b0b0dc 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1023,14 +1023,14 @@ let catchable_exception = function module Goal = struct - type 'a t = { + type t = { env : Environ.env; sigma : Evd.evar_map; concl : EConstr.constr ; self : Evar.t ; (* for compatibility with old-style definitions *) } - let assume (gl : 'a t) = (gl :> [ `NF ] t) + let assume (gl : t) = (gl : t) let env {env} = env let sigma {sigma} = sigma |