implemented normalize (used in new_metasenv_for_apply)

[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 3ff3e4570ed894a2cb6ffd3ef2f793e53e2e4fe8..5f35c54b9d172bad15052cc423e07237f31cd408 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -497,3 +497,4 @@ let subst_meta l t =
  in
   aux 0 t          
 ;;
+