let module C = Cic in
let module R = CicReduction in
let (_,metasenv,_,_) = proof in
let module C = Cic in
let module R = CicReduction in
let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
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
~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
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
~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
-
-let exists_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let split_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let left_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let right_tac ~status =
- constructor_tac ~n:2 ~status
-;;
+let exists_tac status = constructor_tac ~n:1 status ;;
+let split_tac status = constructor_tac ~n:1 status ;;
+let left_tac status = constructor_tac ~n:1 status ;;
+let right_tac status = constructor_tac ~n:2 status ;;