From 2cbf0f8fe0929d36391a8f12e32873eb3a95d7cd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Aug 2009 12:15:30 +0000
Subject: Fixed incorrect optimization in Prettyp.pr_located_qualid introduced
 in commit r12265. Add a few synonyms back in Libnames/Nameops to maintain
 some minimal compatibility.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12267 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 024f190f2a..1c7cfa9f64 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -362,7 +362,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
 
 let dummy = mkProp
 let vfx = id_of_string"_expanded_fix_"
-let vfun = id_of_string"_elimminator_function_"
+let vfun = id_of_string"_eliminator_function_"
 
 (* Mark every occurrence of substituted vars (associated to a function)
    as a problem variable: an evar that can be instantiated either by
-- 
cgit v1.2.3