bugfix in discriminate: now works also with inductive types with left parameters

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 97f40205201446fdf82cebd6ad5a67278edec6c7..62f4eb1f30e947e1fb510fb253dfb7af1c6aeb4c 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -281,7 +281,8 @@ let apply_tac_verbose ~term (proof, goal) =
    in
    let metasenv' = metasenv@newmetasenvfragment in
    let termty,_ = 
-     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+   in
    let termty =
      CicSubstitution.subst_vars exp_named_subst_diff termty in
    let goal_arity = count_prods context ty in
@@ -304,7 +305,6 @@ let apply_tac_verbose ~term (proof, goal) =
    in
    let bo' = apply_subst t in
    let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
-(*    prerr_endline ("me: " ^ CicMetaSubst.ppmetasenv newmetasenv'' subst); *)
    let subst_in =
      (* if we just apply the subtitution, the type is irrelevant:
               we may use Implicit, since it will be dropped *)