diff options
| author | Pierre-Marie Pédrot | 2016-11-25 14:54:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:39 +0100 |
| commit | a5499688bd76def8de3d8e1089a49c7a08430903 (patch) | |
| tree | 8aed5c5f9a372b90a97af706043a618e78d69d2c /proofs | |
| parent | 778e863b77bcafc8ed339dd02226e85e5fee2532 (diff) | |
Funind API using EConstr.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 5 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 7499bc251b..410e738de7 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -49,7 +49,7 @@ module V82 = struct (* Access to ".evar_concl" *) let concl evars gl = let evi = Evd.find evars gl in - evi.Evd.evar_concl + EConstr.of_constr evi.Evd.evar_concl (* Access to ".evar_extra" *) let extra evars gl = @@ -146,6 +146,7 @@ module V82 = struct (* Goal represented as a type, doesn't take into account section variables *) let abstract_type sigma gl = + let open EConstr in let (gl,sigma) = nf_evar sigma gl in let env = env sigma gl in let genv = Global.env () in @@ -159,6 +160,4 @@ module V82 = struct t ) ~init:(concl sigma gl) env - let concl sigma gl = EConstr.of_constr (concl sigma gl) - end diff --git a/proofs/goal.mli b/proofs/goal.mli index ca6584e76d..a2fa34c05e 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -75,6 +75,6 @@ module V82 : sig val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map (* Goal represented as a type, doesn't take into account section variables *) - val abstract_type : Evd.evar_map -> goal -> Term.types + val abstract_type : Evd.evar_map -> goal -> EConstr.types end |