let ok_types ty menv =
List.for_all (fun (_, _, mt) -> mt = ty) menv
in
+ let rec has_vars = function
+ | C.Meta _ | C.Rel _ | C.Const _ -> false
+ | C.Var _ -> true
+ | C.Appl l -> List.exists has_vars l
+ | C.Prod (_, s, t) -> (has_vars s) || (has_vars t)
+ | _ -> assert false
+ in
let rec aux newmeta = function
| [] -> [], newmeta
| (uri, term, termty)::tl ->
(CicPp.ppterm term) (CicPp.ppterm termty)));
let res, newmeta =
match termty with
- | C.Prod (name, s, t) ->
+ | C.Prod (name, s, t) when not (has_vars termty) ->
let head, newmetas, args, newmeta =
ProofEngineHelpers.saturate_term newmeta [] context termty 0
in
Some e, (newmeta+1)
| _ -> None, newmeta
)
- | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when iseq uri && not (has_vars termty) ->
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in