diff options
| author | Hugo Herbelin | 2015-05-15 11:37:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-15 11:39:49 +0200 |
| commit | 5d015ae0d90fd7fd3d440acee6ccd501d8b63ba0 (patch) | |
| tree | e73fb685fea3bd4aa5a9eecde1df69c518acccf0 /plugins/setoid_ring | |
| parent | 76c3b40482978fffca50f6f59e8bcae455680aba (diff) | |
| parent | 3fb81febe8efc34860688cac88a2267cfe298cf7 (diff) | |
Merge v8.5 into trunk
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 7844a36c16..f73a15dba0 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -152,7 +152,7 @@ let ic_unsafe c = (*FIXME remove *) let env = Global.env() and sigma = Evd.empty in fst (Constrintern.interp_constr env sigma c) -let ty c = Typing.type_of (Global.env()) Evd.empty c +let ty c = Typing.unsafe_type_of (Global.env()) Evd.empty c let decl_constant na ctx c = let vars = Universes.universes_of_constr c in |