From 9ea87248101d774e1b4c4b706d8d99444b2e5907 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 17 Dec 2003 10:47:40 +0000 Subject: [PATCH] * Reindentation * More comments --- helm/ocaml/cic_proof_checking/cicSubstitution.ml | 12 +++++++----- helm/ocaml/cic_proof_checking/cicSubstitution.mli | 4 +++- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 4a938acb9..704a8325a 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -335,13 +335,15 @@ if List.mem uri params then prerr_endline "---- OK2" ; substaux 1 ;; -(* l is the relocation list *) +(* lift_meta [t_1 ; ... ; t_n] t *) +(* returns the term [t] where [Rel i] is substituted with [t_i] *) +(* [t_i] is lifted as usual when it crosses an abstraction *) let lift_meta l t = - let module C = Cic in - if l = [] then t else - let rec aux k = function + let module C = Cic in + if l = [] then t else + let rec aux k = function C.Rel n as t -> - if n <= k then t else + if n <= k then t else (try match List.nth l (n-k-1) with None -> raise RelToHiddenHypothesis diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli index 038b5de3f..203286991 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -42,5 +42,7 @@ val subst : Cic.term -> Cic.term -> Cic.term val subst_vars : Cic.term Cic.explicit_named_substitution -> Cic.term -> Cic.term -(* ?????????? *) +(* lift_meta [t_1 ; ... ; t_n] t *) +(* returns the term [t] where [Rel i] is substituted with [t_i] *) +(* [t_i] is lifted as usual when it crosses an abstraction *) val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term -- 2.39.2