diff options
| author | Pierre-Marie Pédrot | 2016-11-08 19:02:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:27:26 +0100 |
| commit | 85ab3e298aa1d7333787c1fa44d25df189ac255c (patch) | |
| tree | 32f661f4ccd3fb36657bb9ac8104a08df9cd1d87 /plugins | |
| parent | 67dc22d8389234d0c9b329944ff579e7056b7250 (diff) | |
Pretyping API using EConstr.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 65d273fafb..ddf0137354 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -173,7 +173,7 @@ let get_eq_typ info env = typ let interp_constr_in_type typ env sigma c = - fst (understand env sigma (fst c) ~expected_type:(OfType typ))(*FIXME*) + fst (understand env sigma (fst c) ~expected_type:(OfType (EConstr.of_constr typ)))(*FIXME*) let interp_statement interp_it env sigma st = {st_label=st.st_label; diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e587fd52ce..5e16d2da0e 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1330,7 +1330,7 @@ let understand_my_constr env sigma c concl = | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None) | rc -> map_glob_constr frob rc in - Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc) + Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType (EConstr.of_constr concl)) (frob rawc) let my_refine c gls = let oc = { run = begin fun sigma -> |