From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 May 2008 10:41:53 +0000 (+0000)
Subject: Type of conjecture and subst_entry made uniform.
X-Git-Tag: make_still_working~5227
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e286f733eec5b192c43c9f9f4450bcf6ae42bac;p=helm.git

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 f32f68426..c2e1c53d2 100644
--- 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 efe04de1a..ef1442d4e 100644
--- 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 1d43c2cbc..213c0457a 100644
--- 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