From 9e286f733eec5b192c43c9f9f4450bcf6ae42bac Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 13 May 2008 10:41:53 +0000 Subject: [PATCH] Type of conjecture and subst_entry made uniform. --- helm/software/components/ng_kernel/nCic.ml | 4 ++-- helm/software/components/ng_kernel/nCicTypeChecker.ml | 2 +- helm/software/components/ng_kernel/nCicUtils.ml | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) 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 -- 2.39.2