positivity check fixed, a MutInd not applied (but with an exp-named-subst)

[helm.git] / helm / software / components / tactics / universe.ml

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index 6a0a3156664b6106b965260ac6227a07a1c1fa27..c4e439efe34ca8ffa579b4e94a95e7ebd0066a70 100644 (file)
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -120,7 +120,7 @@ let keys context ty =
     [head true ty; head true (unfold context ty)]
   with ProofEngineTypes.Fail _ -> [head true ty]
 
-let key term = head false term
+let key term = head false term;;
 
 let index_term_and_unfolded_term univ context t ty =
   let key = head true ty in