diff options
| author | Pierre-Marie Pédrot | 2016-11-04 14:48:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:23:49 +0100 |
| commit | d528fdaf12b74419c47698cca7c6f1ec762245a3 (patch) | |
| tree | 2edbaac4e19db595e0ec763de820cbc704897043 /plugins/micromega | |
| parent | 6bd193ff409b01948751525ce0f905916d7a64bd (diff) | |
Retyping API using EConstr.
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 9fb1463db0..a943ef2b01 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1199,7 +1199,7 @@ struct with e when CErrors.noncritical e -> (X(t),env,tg) in let is_prop term = - let sort = Retyping.get_sort_of (Tacmach.pf_env gl) (Tacmach.project gl) term in + let sort = Retyping.get_sort_of (Tacmach.pf_env gl) (Tacmach.project gl) (EConstr.of_constr term) in Term.is_prop_sort sort in let rec xparse_formula env tg term = |