Type of conjecture and subst_entry made uniform.

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index efe04de1a7553d3b43d44b7a1c0c069447a33485..ef1442d4efabf202b24de3f005eca80b533518e4 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -365,7 +365,7 @@ let rec typeof ~subst ~metasenv context term =
         try
          let _,c,_,ty = U.lookup_subst n subst in c,ty
         with U.Subst_not_found _ -> try
-         let _,_,c,ty = U.lookup_meta n metasenv in c,ty
+         let _,c,ty = U.lookup_meta n metasenv in c,ty
         with U.Meta_not_found _ ->
          raise (AssertFailure (lazy (Printf.sprintf
           "%s not found" (PP.ppterm ~subst ~metasenv ~context t))))