From 8ca2202b7bf9b11b69562502f6dfb168b7efb0e2 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Oct 2004 11:58:20 +0000
Subject: [PATCH] - ported to typed explicit substitutions

---
 .../cic_proof_checking/cicReductionMachine.ml |  2 +-
 .../cic_proof_checking/cicTypeChecker.ml      | 24 +++++++------------
 2 files changed, 9 insertions(+), 17 deletions(-)

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index 4b8099fed..f5684a951 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -544,7 +544,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
           )
      | (k, e, ens, (C.Meta (n,l) as t), s) ->
         (try 
-	   let (_, term) = CicUtil.lookup_subst n subst in
+	   let (_, term,_) = CicUtil.lookup_subst n subst in
            reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
 	 with  CicUtil.Subst_not_found _ ->
            let t' = unwind k e ens t in
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 5715778fb..414d0b976 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1330,19 +1330,9 @@ and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l
              let type_t = type_of_aux' ~subst metasenv context t in
              if not (R.are_convertible ~subst ~metasenv context type_t ct) then
 	       (* debug *)
-	       (
-                 (*
-		 (match type_t with 
-		     Cic.Meta (n,l) ->
-		       try 
-			 let (cc, ecco) = CicUtil.lookup_subst n subst in
-			 prerr_endline (CicPp.ppterm ecco)
-		       with CicUtil.Subst_not_found _ ->
-                         prerr_endline "Non lo trovo"
-		    | _ -> ()); *)
               raise (TypeCheckerFailure (sprintf
                 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
-                (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t))))
+                (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
          | None, _  ->
              raise (TypeCheckerFailure
               "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
@@ -1379,15 +1369,17 @@ and type_of_aux' ?(subst = []) metasenv context t =
        ty
     | C.Meta (n,l) -> 
        (try
-          let (canonical_context, term) = CicUtil.lookup_subst n subst in
+          let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
           check_metasenv_consistency 
 	    ~subst metasenv context canonical_context l;
-          type_of_aux context (CicSubstitution.lift_meta l term)
+          (* assuming subst is well typed !!!!! *)
+          CicSubstitution.lift_meta l ty
+          (* type_of_aux context (CicSubstitution.lift_meta l term) *)
 	with CicUtil.Subst_not_found _ ->
 	  let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
-            check_metasenv_consistency 
-	      ~subst metasenv context canonical_context l;
-            CicSubstitution.lift_meta l ty)
+          check_metasenv_consistency 
+	     ~subst metasenv context canonical_context l;
+          CicSubstitution.lift_meta l ty)
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
-- 
2.39.2