Type of conjecture and subst_entry made uniform.

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index f32f6842638e196c3a74db75ea1761d0fbfd58e4..c2e1c53d2d36cad3c6ccb022c0118fbb9e5d3871 100644 (file)
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -47,9 +47,9 @@ type hypothesis = string * context_entry
 
 type context = hypothesis list
 
-type conjecture = int * string option * context * term
+type conjecture = string option * context * term
 
-type metasenv = conjecture list
+type metasenv = (int * conjecture) list
 
 type subst_entry = string option * context * term * term
 

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))))

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