Type of conjecture and subst_entry made uniform.

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

diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml
index 1d43c2cbc3a69e18e18916a354f5ff9040859cd3..213c0457a5d88ab82ee155d5dfcd4cac20214018 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUtils.ml
+++ b/helm/software/components/ng_kernel/nCicUtils.ml
@@ -30,10 +30,10 @@ let lookup_subst n subst =
   with Not_found -> raise (Subst_not_found n)
 ;;
 
-let lookup_meta index metasenv =
+let lookup_meta n metasenv =
   try
-    List.find (fun (index', _, _, _) -> index = index') metasenv
-  with Not_found -> raise (Meta_not_found index)
+    List.assoc n metasenv
+  with Not_found -> raise (Meta_not_found n)
 ;;
 
 let fold g k f acc = function