7.2 Explicit proof as a term
7.2.1 Exact term
This tactic applies to any goal. It gives directly the exact proof term of the goal. Let T be our goal, let p be a term of type U then Exact p succeeds iff T and U are convertible (see section 4.3).Error messages:
- Not an exact proof
7.2.2 Refine term
This tactic allows to give an exact proof but still with some holes. The holes are noted ``?''.Error messages:
- invalid argument: the tactic Refine doesn't know what to do with the term you gave.
- Refine passed ill-formed term: the term you gave is not a valid proof (not easy to debug in general). This message may also occur in higher-level tactics, which call Refine internally.
- unconstrained isevar: there is a hole in the term you gave which type cannot be inferred. Put a cast around it.
This tactic is currently given as an experiment. An example of use is given in section 8.1.