diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-06 17:21:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:25:30 +0100 |
| commit | e27949240f5b1ee212e7d0fe3326a21a13c4abb0 (patch) | |
| tree | bf076ea31e6ca36cc80e0f978bc63d112e183725 /proofs/clenv.ml | |
| parent | b365304d32db443194b7eaadda63c784814f53f1 (diff) | |
Typing API using EConstr.
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f4ac094b8..c2130a64a 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -29,7 +29,7 @@ open Sigma.Notations (* Abbreviations *) let pf_env = Refiner.pf_env -let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c +let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c) (******************************************************************) (* Clausal environments *) |