match (R.whd context ty) with
(C.MutInd (uri, typeno, exp_named_subst))
| (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
- PrimitiveTactics.apply_tac ~status:(proof, goal)
+ PrimitiveTactics.apply_tac
~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
+ ~status:(proof, goal)
| _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
;;