2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 exception RefineFailure of (Stdpp.location * string) Lazy.t;;
15 exception Uncertain of (Stdpp.location * string) Lazy.t;;
16 exception AssertFailure of string Lazy.t;;
18 type 'a expected_type = [ `XTNone (* unknown *)
19 | `XTSome of 'a (* the given term *)
20 | `XTSort (* any sort *)
21 | `XTInd (* any (co)inductive type *)
24 #NCicCoercion.status ->
25 ?localise:(NCic.term -> Stdpp.location) ->
26 NCic.metasenv -> NCic.substitution -> NCic.context ->
27 NCic.term -> NCic.term expected_type -> (* term, expected type *)
28 NCic.metasenv * NCic.substitution * NCic.term * NCic.term
29 (* menv, subst,refined term, type *)
32 #NCicCoercion.status ->
33 ?localise:(NCic.term -> Stdpp.location) ->